Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions | Friends
model Class Reference
+ Inheritance diagram for model:

Public Member Functions

 model (context &c, Z3_model m)
 
 model (model const &s)
 
 ~model ()
 
 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[] (unsigned i) const
 
expr get_const_interp (func_decl c) const
 
func_interp get_func_interp (func_decl f) const
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void 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 1054 of file z3++.h.

Constructor & Destructor Documentation

model ( context c,
Z3_model  m 
)
inline

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

:object(c) { init(m); }
model ( model const &  s)
inline

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

:object(s) { init(s.m_model); }
~model ( )
inline

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

{ Z3_model_dec_ref(ctx(), m_model); }

Member Function Documentation

expr eval ( expr const &  n,
bool  model_completion = false 
) const
inline

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

{
check_context(*this, n);
Z3_ast r;
Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
if (status == Z3_FALSE)
throw exception("failed to evaluate expression");
return expr(ctx(), r);
}
func_decl get_const_decl ( unsigned  i) const
inline

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

Referenced by model::operator[]().

{ Z3_func_decl r = Z3_model_get_const_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }
expr get_const_interp ( func_decl  c) const
inline

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

{
check_context(*this, c);
Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
return expr(ctx(), r);
}
func_decl get_func_decl ( unsigned  i) const
inline

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

Referenced by model::operator[]().

{ Z3_func_decl r = Z3_model_get_func_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }
func_interp get_func_interp ( func_decl  f) const
inline

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

{
check_context(*this, f);
return func_interp(ctx(), r);
}
unsigned num_consts ( ) const
inline

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

Referenced by model::operator[](), and model::size().

{ return Z3_model_get_num_consts(ctx(), m_model); }
unsigned num_funcs ( ) const
inline

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

Referenced by model::size().

{ return Z3_model_get_num_funcs(ctx(), m_model); }
operator Z3_model ( ) const
inline

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

{ return m_model; }
model& operator= ( model const &  s)
inline

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

{
Z3_model_inc_ref(s.ctx(), s.m_model);
Z3_model_dec_ref(ctx(), m_model);
m_ctx = s.m_ctx;
m_model = s.m_model;
return *this;
}
func_decl operator[] ( unsigned  i) const
inline

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

{ return i < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts()); }
unsigned size ( ) const
inline

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

{ return num_consts() + num_funcs(); }

Friends And Related Function Documentation

std::ostream& operator<< ( std::ostream &  out,
model const &  m 
)
friend

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

{ out << Z3_model_to_string(m.ctx(), m); return out; }