Definition at line 2225 of file z3++.h.
◆ model() [1/4]
◆ model() [2/4]
◆ model() [3/4]
◆ model() [4/4]
◆ ~model()
◆ add_const_interp()
◆ add_func_interp()
Definition at line 2290 of file z3++.h.
2293 return func_interp(
ctx(), r);
◆ eval()
expr eval |
( |
expr const & |
n, |
|
|
bool |
model_completion = false |
|
) |
| const |
|
inline |
Definition at line 2247 of file z3++.h.
2252 if (status ==
false &&
ctx().enable_exceptions())
2253 Z3_THROW(exception(
"failed to evaluate expression"));
2254 return expr(
ctx(), r);
◆ get_const_decl()
◆ get_const_interp()
Definition at line 2270 of file z3++.h.
2274 return expr(
ctx(), r);
◆ get_func_decl()
◆ get_func_interp()
Definition at line 2276 of file z3++.h.
2280 return func_interp(
ctx(), r);
◆ has_interp()
◆ num_consts()
unsigned num_consts |
( |
| ) |
const |
|
inline |
◆ num_funcs()
unsigned num_funcs |
( |
| ) |
const |
|
inline |
◆ operator Z3_model()
operator Z3_model |
( |
| ) |
const |
|
inline |
◆ operator=()
Definition at line 2239 of file z3++.h.
2243 m_model = s.m_model;
◆ operator[]()
◆ size()
◆ operator<<
std::ostream& operator<< |
( |
std::ostream & |
out, |
|
|
model const & |
m |
|
) |
| |
|
friend |
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...
Z3_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.
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)
translate model from context c to context dst.
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.
func_decl get_const_decl(unsigned i) const
func_decl get_func_decl(unsigned i) const
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.
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
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...
void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a)
Add a constant interpretation.
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,...
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
friend void check_context(object const &a, object const &b)
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.
unsigned num_consts() const
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
Z3_error_code check_error() const
unsigned num_funcs() const