smt_solver_baset::uf_ackermann_entry Struct Reference

One recorded uninterpreted-function application in the Ackermannisation fallback: the argument asts, the fresh result ast, and the context level at which it was created (so it can be pruned on the matching pop, since pop_ctx deletes the asts made since the push). More...

#include <smt_solver.h>

Public Attributes
std::vector< smt_astt >	args
smt_astt	result
unsigned int	level

Detailed Description

One recorded uninterpreted-function application in the Ackermannisation fallback: the argument asts, the fresh result ast, and the context level at which it was created (so it can be pruned on the matching pop, since pop_ctx deletes the asts made since the push).

Member Data Documentation

args

std::vector<smt_astt> smt_solver_baset::uf_ackermann_entry::args

level

unsigned int smt_solver_baset::uf_ackermann_entry::level

result

smt_astt smt_solver_baset::uf_ackermann_entry::result

---

The documentation for this struct was generated from the following file:

• src/solvers/smt/smt_solver.h