Z3
Data Structures | Public Member Functions | Friends
model Class Reference
+ 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 ()
 
 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)
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
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 1814 of file z3++.h.

Constructor & Destructor Documentation

◆ model() [1/4]

model ( context c)
inline

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

1822 :object(c) { init(Z3_mk_model(c)); }
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
object(context &c)
Definition: z3++.h:371

◆ model() [2/4]

model ( context c,
Z3_model  m 
)
inline

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

1823 :object(c) { init(m); }
object(context &c)
Definition: z3++.h:371

◆ model() [3/4]

model ( model const &  s)
inline

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

1824 :object(s) { init(s.m_model); }
object(context &c)
Definition: z3++.h:371

◆ model() [4/4]

model ( model src,
context dst,
translate   
)
inline

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

1825 : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); }
object(context &c)
Definition: z3++.h:371
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()

~model ( )
inline

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

1826 { Z3_model_dec_ref(ctx(), m_model); }
context & ctx() const
Definition: z3++.h:373
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 1885 of file z3++.h.

1885  {
1886  Z3_add_const_interp(ctx(), m_model, f, value);
1887  check_error();
1888  }
Z3_error_code check_error() const
Definition: z3++.h:374
void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a)
Add a constant interpretation.
context & ctx() const
Definition: z3++.h:373

◆ add_func_interp()

func_interp add_func_interp ( func_decl f,
expr else_val 
)
inline

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

1879  {
1880  Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
1881  check_error();
1882  return func_interp(ctx(), r);
1883  }
Z3_error_code check_error() const
Definition: z3++.h:374
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...
context & ctx() const
Definition: z3++.h:373

◆ eval()

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

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

1836  {
1837  check_context(*this, n);
1838  Z3_ast r = 0;
1839  Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
1840  check_error();
1841  if (status == Z3_FALSE && ctx().enable_exceptions())
1842  Z3_THROW(exception("failed to evaluate expression"));
1843  return expr(ctx(), r);
1844  }
Z3_error_code check_error() const
Definition: z3++.h:374
#define Z3_THROW(x)
Definition: z3++.h:93
bool Z3_bool
Z3 Boolean type. It is just an alias for bool.
Definition: z3_api.h:77
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377
Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v...
#define Z3_FALSE
False value. It is just an alias for 0.
Definition: z3_api.h:93

◆ get_const_decl()

func_decl get_const_decl ( unsigned  i) const
inline

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

Referenced by model::operator[]().

1848 { Z3_func_decl r = Z3_model_get_const_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:374
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.
context & ctx() const
Definition: z3++.h:373

◆ get_const_interp()

expr get_const_interp ( func_decl  c) const
inline

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

1859  {
1860  check_context(*this, c);
1861  Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
1862  check_error();
1863  return expr(ctx(), r);
1864  }
Z3_error_code check_error() const
Definition: z3++.h:374
context & ctx() const
Definition: z3++.h:373
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...
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377

◆ get_func_decl()

func_decl get_func_decl ( unsigned  i) const
inline

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

Referenced by model::operator[]().

1849 { Z3_func_decl r = Z3_model_get_func_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }
Z3_error_code check_error() const
Definition: z3++.h:374
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.
context & ctx() const
Definition: z3++.h:373

◆ get_func_interp()

func_interp get_func_interp ( func_decl  f) const
inline

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

1865  {
1866  check_context(*this, f);
1867  Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
1868  check_error();
1869  return func_interp(ctx(), r);
1870  }
Z3_error_code check_error() const
Definition: z3++.h:374
context & ctx() const
Definition: z3++.h:373
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...
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377

◆ has_interp()

bool has_interp ( func_decl  f) const
inline

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

1874  {
1875  check_context(*this, f);
1876  return 0 != Z3_model_has_interp(ctx(), m_model, f);
1877  }
context & ctx() const
Definition: z3++.h:373
friend void check_context(object const &a, object const &b)
Definition: z3++.h:377
Z3_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 1846 of file z3++.h.

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

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

◆ num_funcs()

unsigned num_funcs ( ) const
inline

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

Referenced by model::size().

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

◆ operator Z3_model()

operator Z3_model ( ) const
inline

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

1827 { return m_model; }

◆ operator=()

model& operator= ( model const &  s)
inline

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

1828  {
1829  Z3_model_inc_ref(s.ctx(), s.m_model);
1830  Z3_model_dec_ref(ctx(), m_model);
1831  m_ctx = s.m_ctx;
1832  m_model = s.m_model;
1833  return *this;
1834  }
context & ctx() const
Definition: z3++.h:373
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
context * m_ctx
Definition: z3++.h:369

◆ operator[]()

func_decl operator[] ( int  i) const
inline

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

1851  {
1852  assert(0 <= i);
1853  return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
1854  }
func_decl get_const_decl(unsigned i) const
Definition: z3++.h:1848
func_decl get_func_decl(unsigned i) const
Definition: z3++.h:1849
unsigned num_consts() const
Definition: z3++.h:1846

◆ size()

unsigned size ( ) const
inline

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

1850 { return num_consts() + num_funcs(); }
unsigned num_consts() const
Definition: z3++.h:1846
unsigned num_funcs() const
Definition: z3++.h:1847

Friends And Related Function Documentation

◆ operator<<

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

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

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