Z3
 
Loading...
Searching...
No Matches
model Class Reference

#include <z3++.h>

+ Inheritance diagram for model:

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
 
modeloperator= (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
 
contextctx () 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
contextm_ctx
 

Detailed Description

Definition at line 2604 of file z3++.h.

Constructor & Destructor Documentation

◆ model() [1/4]

model ( context & c)
inline

Definition at line 2612 of file z3++.h.

2612:object(c) { init(Z3_mk_model(c)); }
object(context &c)
Definition z3++.h:472
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(), ModelRef::translate(), and ModelRef::update_value().

◆ model() [2/4]

◆ model() [3/4]

◆ model() [4/4]

model ( model & src,
context & dst,
translate  )
inline

Definition at line 2615 of file z3++.h.

2615: object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); }
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(), ModelRef::translate(), and ModelRef::update_value().

◆ ~model()

~model ( )
inlineoverride

Definition at line 2616 of file z3++.h.

2616{ Z3_model_dec_ref(ctx(), m_model); }
context & ctx() const
Definition z3++.h:474
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.

Member Function Documentation

◆ add_const_interp()

void add_const_interp ( func_decl & f,
expr & value )
inline

Definition at line 2675 of file z3++.h.

2675 {
2676 Z3_add_const_interp(ctx(), m_model, f, value);
2677 check_error();
2678 }
Z3_error_code check_error() const
Definition z3++.h:475
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()

func_interp add_func_interp ( func_decl & f,
expr & else_val )
inline

Definition at line 2669 of file z3++.h.

2669 {
2670 Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
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 {
2627 check_context(*this, n);
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 }
friend void check_context(object const &a, object const &b)
Definition z3++.h:478
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.
#define Z3_THROW(x)
Definition z3++.h:103

Referenced by ModelRef::evaluate().

◆ get_const_decl()

func_decl get_const_decl ( unsigned i) const
inline

Definition at line 2638 of file z3++.h.

2638{ Z3_func_decl r = Z3_model_get_const_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }
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 model::operator[]().

◆ get_const_interp()

expr get_const_interp ( func_decl c) const
inline

Definition at line 2649 of file z3++.h.

2649 {
2650 check_context(*this, c);
2651 Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
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()

func_decl get_func_decl ( unsigned i) const
inline

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 model::operator[]().

◆ get_func_interp()

func_interp get_func_interp ( func_decl f) const
inline

Definition at line 2655 of file z3++.h.

2655 {
2656 check_context(*this, f);
2657 Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
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()

bool has_interp ( func_decl f) const
inline

Definition at line 2664 of file z3++.h.

2664 {
2665 check_context(*this, f);
2666 return Z3_model_has_interp(ctx(), m_model, f);
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.

2636{ return Z3_model_get_num_consts(ctx(), m_model); }
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
inline

Definition at line 2637 of file z3++.h.

2637{ return Z3_model_get_num_funcs(ctx(), m_model); }
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

Definition at line 2617 of file z3++.h.

2617{ return m_model; }

◆ operator=()

model & operator= ( model const & s)
inline

Definition at line 2618 of file z3++.h.

2618 {
2619 Z3_model_inc_ref(s.ctx(), s.m_model);
2620 Z3_model_dec_ref(ctx(), m_model);
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[]()

func_decl operator[] ( int i) const
inline

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 }
unsigned num_consts() const
Definition z3++.h:2636
func_decl get_func_decl(unsigned i) const
Definition z3++.h:2639
func_decl get_const_decl(unsigned i) const
Definition z3++.h:2638

◆ size()

unsigned size ( ) const
inline

Definition at line 2640 of file z3++.h.

2640{ return num_consts() + num_funcs(); }
unsigned num_funcs() const
Definition z3++.h:2637

Referenced by Goal::__len__(), ParamDescrsRef::__len__(), BitVecNumRef::as_signed_long(), and BitVecSortRef::subsort().

◆ to_string()

std::string to_string ( ) const
inline

Definition at line 2682 of file z3++.h.

2682{ return m_model ? std::string(Z3_model_to_string(ctx(), m_model)) : "null"; }
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.

Friends And Related Symbol Documentation

◆ 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(); }