Data Structures | |
struct | translate |
Public Member Functions | |
model (context &c) | |
model (context &c, Z3_model m) | |
model (model const &s) | |
model (model &src, context &dst, translate) | |
~model () override | |
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 |
bool | has_interp (func_decl f) const |
func_interp | add_func_interp (func_decl &f, expr &else_val) |
void | add_const_interp (func_decl &f, expr &value) |
std::string | to_string () const |
Public Member Functions inherited from object | |
object (context &c) | |
virtual | ~object ()=default |
context & | ctx () const |
Z3_error_code | check_error () const |
Friends | |
std::ostream & | operator<< (std::ostream &out, model const &m) |
Additional Inherited Members | |
Protected Attributes inherited from object | |
context * | m_ctx |
Definition at line 2612 of file z3++.h.
Referenced by ModelRef::__del__(), ModelRef::__getitem__(), ModelRef::__len__(), ModelRef::decls(), ModelRef::eval(), ModelRef::get_interp(), ModelRef::get_sort(), ModelRef::get_universe(), ModelRef::num_sorts(), ModelRef::sexpr(), FuncInterp::translate(), ModelRef::translate(), and ModelRef::update_value().
Definition at line 2613 of file z3++.h.
Referenced by ModelRef::__del__(), ModelRef::__getitem__(), ModelRef::__len__(), ModelRef::decls(), ModelRef::eval(), ModelRef::get_interp(), ModelRef::get_sort(), ModelRef::get_universe(), ModelRef::num_sorts(), ModelRef::sexpr(), FuncInterp::translate(), ModelRef::translate(), and ModelRef::update_value().
Definition at line 2614 of file z3++.h.
Referenced by ModelRef::__del__(), ModelRef::__getitem__(), ModelRef::__len__(), ModelRef::decls(), ModelRef::eval(), ModelRef::get_interp(), ModelRef::get_sort(), ModelRef::get_universe(), ModelRef::num_sorts(), ModelRef::sexpr(), FuncInterp::translate(), ModelRef::translate(), and ModelRef::update_value().
Definition at line 2615 of file z3++.h.
Referenced by ModelRef::__del__(), ModelRef::__getitem__(), ModelRef::__len__(), ModelRef::decls(), ModelRef::eval(), ModelRef::get_interp(), ModelRef::get_sort(), ModelRef::get_universe(), ModelRef::num_sorts(), ModelRef::sexpr(), FuncInterp::translate(), ModelRef::translate(), and ModelRef::update_value().
|
inlineoverride |
|
inline |
Definition at line 2626 of file z3++.h.
Referenced by ModelRef::evaluate().
|
inline |
Definition at line 2638 of file z3++.h.
Referenced by model::operator[]().
|
inline |
Definition at line 2639 of file z3++.h.
Referenced by model::operator[]().
|
inline |
|
inline |
|
inline |
Definition at line 2636 of file z3++.h.
Referenced by model::operator[](), and model::size().
|
inline |
Definition at line 2637 of file z3++.h.
Referenced by model::size().
|
inline |
Definition at line 2641 of file z3++.h.
|
inline |
Definition at line 2640 of file z3++.h.
Referenced by ParamDescrsRef::__len__(), Goal::__len__(), BitVecNumRef::as_signed_long(), and BitVecSortRef::subsort().
|
inline |