Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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[] (int 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 1155 of file z3++.h.

Constructor & Destructor Documentation

model ( context c,
Z3_model  m 
)
inline

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

1162 :object(c) { init(m); }
object(context &c)
Definition: z3++.h:270
model ( model const &  s)
inline

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

1163 :object(s) { init(s.m_model); }
object(context &c)
Definition: z3++.h:270
~model ( )
inline

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

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

Member Function Documentation

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

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

1174  {
1175  check_context(*this, n);
1176  Z3_ast r;
1177  Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
1178  check_error();
1179  if (status == Z3_FALSE)
1180  throw exception("failed to evaluate expression");
1181  return expr(ctx(), r);
1182  }
int Z3_bool
Z3 Boolean type. It is just an alias for int.
Definition: z3_api.h:102
Z3_bool Z3_API Z3_model_eval(__in Z3_context c, __in Z3_model m, __in Z3_ast t, __in Z3_bool model_completion, __out Z3_ast *v)
Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v...
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
#define Z3_FALSE
False value. It is just an alias for 0.
Definition: z3_api.h:127
func_decl get_const_decl ( unsigned  i) const
inline

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

Referenced by model::operator[]().

1186 { Z3_func_decl r = Z3_model_get_const_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_func_decl Z3_API Z3_model_get_const_decl(__in Z3_context c, __in Z3_model m, __in unsigned i)
Return the i-th constant in the given model.
expr get_const_interp ( func_decl  c) const
inline

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

1194  {
1195  check_context(*this, c);
1196  Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
1197  check_error();
1198  return expr(ctx(), r);
1199  }
Z3_ast Z3_API Z3_model_get_const_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL...
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
func_decl get_func_decl ( unsigned  i) const
inline

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

Referenced by model::operator[]().

1187 { 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(__in Z3_context c, __in Z3_model m, __in unsigned i)
Return the declaration of the i-th function in the given model.
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
func_interp get_func_interp ( func_decl  f) const
inline

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

1200  {
1201  check_context(*this, f);
1202  Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
1203  check_error();
1204  return func_interp(ctx(), r);
1205  }
Z3_func_interp Z3_API Z3_model_get_func_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
unsigned num_consts ( ) const
inline

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

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

1184 { return Z3_model_get_num_consts(ctx(), m_model); }
context & ctx() const
Definition: z3++.h:272
unsigned Z3_API Z3_model_get_num_consts(__in Z3_context c, __in Z3_model m)
Return the number of constants assigned by the given model.
unsigned num_funcs ( ) const
inline

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

Referenced by model::size().

1185 { return Z3_model_get_num_funcs(ctx(), m_model); }
context & ctx() const
Definition: z3++.h:272
unsigned Z3_API Z3_model_get_num_funcs(__in Z3_context c, __in Z3_model m)
Return the number of function interpretations in the given model.
operator Z3_model ( ) const
inline

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

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

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

1166  {
1167  Z3_model_inc_ref(s.ctx(), s.m_model);
1168  Z3_model_dec_ref(ctx(), m_model);
1169  m_ctx = s.m_ctx;
1170  m_model = s.m_model;
1171  return *this;
1172  }
void Z3_API Z3_model_inc_ref(__in Z3_context c, __in Z3_model m)
Increment the reference counter of the given model.
void Z3_API Z3_model_dec_ref(__in Z3_context c, __in Z3_model m)
Decrement the reference counter of the given model.
context & ctx() const
Definition: z3++.h:272
context * m_ctx
Definition: z3++.h:268
func_decl operator[] ( int  i) const
inline

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

1189  {
1190  assert(0 <= i);
1191  return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
1192  }
func_decl get_const_decl(unsigned i) const
Definition: z3++.h:1186
func_decl get_func_decl(unsigned i) const
Definition: z3++.h:1187
unsigned num_consts() const
Definition: z3++.h:1184
unsigned size ( ) const
inline

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

1188 { return num_consts() + num_funcs(); }
unsigned num_consts() const
Definition: z3++.h:1184
unsigned num_funcs() const
Definition: z3++.h:1185

Friends And Related Function Documentation

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

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

1207 { out << Z3_model_to_string(m.ctx(), m); return out; }
Z3_string Z3_API Z3_model_to_string(__in Z3_context c, __in Z3_model m)
Convert the given model into a string.