#include <z3++.h>
Definition at line 2604 of file z3++.h.
◆ model() [1/4]
◆ model() [2/4]
Definition at line 2613 of file z3++.h.
2613:object(c) { init(m); }
◆ model() [3/4]
Definition at line 2614 of file z3++.h.
2614:object(s) { init(s.m_model); }
◆ 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.
◆ ~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.
2675 {
2677 check_error();
2678 }
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.
2669 {
2671 check_error();
2672 return func_interp(ctx(), r);
2673 }
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...
◆ eval()
expr eval |
( |
expr const & | n, |
|
|
bool | model_completion = false ) const |
|
inline |
Definition at line 2626 of file z3++.h.
2626 {
2628 Z3_ast r = 0;
2629 bool status =
Z3_model_eval(ctx(), m_model, n, model_completion, &r);
2630 check_error();
2631 if (status == false && ctx().enable_exceptions())
2632 Z3_THROW(exception(
"failed to evaluate expression"));
2633 return expr(ctx(), r);
2634 }
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 check_context(object const &a, object const &b)
◆ get_const_decl()
Definition 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.
Referenced by operator[]().
◆ get_const_interp()
Definition at line 2649 of file z3++.h.
2649 {
2652 check_error();
2653 return expr(ctx(), r);
2654 }
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.
2639{ Z3_func_decl r =
Z3_model_get_func_decl(ctx(), m_model, i); check_error();
return func_decl(ctx(), r); }
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 operator[]().
◆ get_func_interp()
Definition at line 2655 of file z3++.h.
2655 {
2658 check_error();
2659 return func_interp(ctx(), r);
2660 }
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.
2664 {
2667 }
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 |
|
inline |
Definition 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 operator[](), and size().
◆ num_funcs()
unsigned num_funcs |
( |
| ) |
const |
|
inline |
Definition 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 size().
◆ operator Z3_model()
operator Z3_model |
( |
| ) |
const |
|
inline |
◆ operator=()
Definition at line 2618 of file z3++.h.
2618 {
2621 object::operator=(s);
2622 m_model = s.m_model;
2623 return *this;
2624 }
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.
2641 {
2642 assert(0 <= i);
2643 return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
2644 }
◆ size()
Definition at line 2640 of file z3++.h.
2640{ return num_consts() + num_funcs(); }
◆ to_string()
std::string to_string |
( |
| ) |
const |
|
inline |
Definition 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.
Referenced by operator<<.
◆ operator<<
std::ostream & operator<< |
( |
std::ostream & | out, |
|
|
model const & | m ) |
|
friend |
Definition at line 2684 of file z3++.h.
2684{ return out << m.to_string(); }