Definition at line 2604 of file z3++.h.
◆ model() [1/4]Definition at line 2612 of file z3++.h.
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
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().
◆ model() [2/4]Definition at line 2613 of file z3++.h.
2613:
object(c) { init(m); }
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().
◆ model() [3/4]Definition at line 2614 of file z3++.h.
2614:
object(s) { init(s.m_model); }
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().
◆ model() [4/4]Definition at line 2615 of file z3++.h.
Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)
translate model from context c to context dst.
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().
◆ ~model()Definition at line 2616 of file z3++.h.
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
◆ add_const_interp()Definition at line 2675 of file z3++.h.
Z3_error_code check_error() const
void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a)
Add a constant interpretation.
◆ add_func_interp()Definition at line 2669 of file z3++.h.
2672 returnfunc_interp(
ctx(), r);
Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value)
Create a fresh func_interp object, add it to a model for a specified function. It has reference count...
System.IntPtr Z3_func_interp
◆ eval() expr eval ( expr const & n, bool model_completion =false ) const inline
Definition at line 2626 of file z3++.h.
2631 if(status ==
false&&
ctx().enable_exceptions())
2632 Z3_THROW(exception(
"failed to evaluate expression"));
2633 returnexpr(
ctx(), r);
friend void check_context(object const &a, object const &b)
bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return true if succeeded, and store the result in v.
Referenced by ModelRef::evaluate().
◆ get_const_decl() func_decl get_const_decl ( unsigned i ) const inlineDefinition at line 2638 of file z3++.h.
Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)
Return the i-th constant in the given model.
System.IntPtr Z3_func_decl
Referenced by model::operator[]().
◆ get_const_interp()Definition at line 2649 of file z3++.h.
2653 returnexpr(
ctx(), r);
Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL,...
◆ get_func_decl()Definition at line 2639 of file z3++.h.
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i)
Return the declaration of the i-th function in the given model.
Referenced by model::operator[]().
◆ get_func_interp()Definition at line 2655 of file z3++.h.
2659 returnfunc_interp(
ctx(), r);
Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
◆ has_interp()Definition at line 2664 of file z3++.h.
bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Test if there exists an interpretation (i.e., assignment) for a in the model m.
◆ num_consts() unsigned num_consts ( ) const inlineDefinition at line 2636 of file z3++.h.
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
Referenced by model::operator[](), and model::size().
◆ num_funcs() unsigned num_funcs ( ) const inlineDefinition at line 2637 of file z3++.h.
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
Referenced by model::size().
◆ operator Z3_model() operator Z3_model ( ) const inline ◆ operator=()Definition at line 2618 of file z3++.h.
2621object::operator=(s);
2622m_model = s.m_model;
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
◆ operator[]()Definition at line 2641 of file z3++.h.
unsigned num_consts() const
func_decl get_func_decl(unsigned i) const
func_decl get_const_decl(unsigned i) const
◆ size() ◆ to_string() std::string to_string ( ) const inlineDefinition at line 2682 of file z3++.h.
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
◆ operator<< std::ostream& operator<< ( std::ostream & out, model const & m ) friendDefinition at line 2684 of file z3++.h.
2684{
returnout << m.to_string(); }
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4