Public Member Functions | |
model (context &c, Z3_model m) | |
model (model const &s) | |
~model () | |
operator Z3_model () const | |
model & | operator= (model const &s) |
expr | eval (expr const &n, bool model_completion=false) const |
unsigned | num_consts () const |
unsigned | num_funcs () const |
func_decl | get_const_decl (unsigned i) const |
func_decl | get_func_decl (unsigned i) const |
unsigned | size () const |
func_decl | operator[] (int i) const |
expr | get_const_interp (func_decl c) const |
func_interp | get_func_interp (func_decl f) const |
Friends | |
std::ostream & | operator<< (std::ostream &out, model const &m) |
~model | ( | ) | [inline] |
Definition at line 1164 of file z3++.h.
{ Z3_model_dec_ref(ctx(), m_model); }
Definition at line 1174 of file z3++.h.
{ check_context(*this, n); Z3_ast r; Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r); check_error(); if (status == Z3_FALSE) throw exception("failed to evaluate expression"); return expr(ctx(), r); }
func_decl get_const_decl | ( | unsigned | i | ) | const [inline] |
Definition at line 1186 of file z3++.h.
Referenced by model::operator[]().
{ Z3_func_decl r = Z3_model_get_const_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }
expr get_const_interp | ( | func_decl | c | ) | const [inline] |
Definition at line 1194 of file z3++.h.
{ check_context(*this, c); Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c); check_error(); return expr(ctx(), r); }
func_decl get_func_decl | ( | unsigned | i | ) | const [inline] |
Definition at line 1187 of file z3++.h.
Referenced by model::operator[]().
{ Z3_func_decl r = Z3_model_get_func_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }
func_interp get_func_interp | ( | func_decl | f | ) | const [inline] |
Definition at line 1200 of file z3++.h.
{ check_context(*this, f); Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f); check_error(); return func_interp(ctx(), r); }
unsigned num_consts | ( | ) | const [inline] |
Definition at line 1184 of file z3++.h.
Referenced by model::operator[](), and model::size().
{ return Z3_model_get_num_consts(ctx(), m_model); }
unsigned num_funcs | ( | ) | const [inline] |
Definition at line 1185 of file z3++.h.
Referenced by model::size().
{ return Z3_model_get_num_funcs(ctx(), m_model); }
Definition at line 1166 of file z3++.h.
{ Z3_model_inc_ref(s.ctx(), s.m_model); Z3_model_dec_ref(ctx(), m_model); m_ctx = s.m_ctx; m_model = s.m_model; return *this; }
func_decl operator[] | ( | int | i | ) | const [inline] |
Definition at line 1189 of file z3++.h.
{ assert(0 <= i); return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts()); }
unsigned size | ( | ) | const [inline] |
Definition at line 1188 of file z3++.h.
{ return num_consts() + num_funcs(); }
std::ostream& operator<< | ( | std::ostream & | out, |
model const & | m | ||
) | [friend] |
Definition at line 1207 of file z3++.h.
{ out << Z3_model_to_string(m.ctx(), m); return out; }