Z3 |

Data Structures | Public Member Functions | Friends
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 ()
| operator Z3_model () const
model & | operator= (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)
context & | ctx () 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
context * | m_ctx

## Detailed Description

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

## Constructor & Destructor Documentation

## ◆ model() [1/4]

model | ( | context & | c | ) |
| inline

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

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

## ◆ model() [2/4]

model | ( | context & | c,
|  | Z3_model | m
| ) |  |
| inline

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

2441:object(c) { init(m); }

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(), FuncInterp::translate(), and ModelRef::translate().

## ◆ model() [3/4]

model | ( | model const & | s | ) |
| inline

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

2442:object(s) { init(s.m_model); }

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(), FuncInterp::translate(), and ModelRef::translate().

## ◆ model() [4/4]

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

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

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

## ◆ ~model()

~model | ( |  | ) |
| inline

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

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

2503 {
2504 Z3_add_const_interp(ctx(), m_model, f, value);
2505 check_error();
2506 }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
Z3_add_const_interp
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 2497 of file z3++.h.

2497 {
2498 Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
2499 check_error();
2500 return func_interp(ctx(), r);
2501 }
Z3_add_func_interp
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 2454 of file z3++.h.

2454 {
2455 check_context(*this, n);
2456 Z3_ast r = 0;
2457 bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
2458 check_error();
2459 if (status == false && ctx().enable_exceptions())
2460 Z3_THROW(exception("failed to evaluate expression"));
2461 return expr(ctx(), r);
2462 }
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:426
Z3_THROW
#define Z3_THROW(x)
Definition: z3++.h:100
Z3_model_eval
Z3_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.

Referenced by ModelRef::evaluate().

## ◆ get_const_decl()

func_decl get_const_decl | ( | unsigned | i | ) | const
| inline

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

2466{ Z3_func_decl r = Z3_model_get_const_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }
Z3_model_get_const_decl
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 2477 of file z3++.h.

2477 {
2478 check_context(*this, c);
2479 Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
2480 check_error();
2481 return expr(ctx(), r);
2482 }
Z3_model_get_const_interp
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 2467 of file z3++.h.

2467{ Z3_func_decl r = Z3_model_get_func_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }
Z3_model_get_func_decl
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 2483 of file z3++.h.

2483 {
2484 check_context(*this, f);
2485 Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
2486 check_error();
2487 return func_interp(ctx(), r);
2488 }
Z3_model_get_func_interp
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 2492 of file z3++.h.

2492 {
2493 check_context(*this, f);
2494 return Z3_model_has_interp(ctx(), m_model, f);
2495 }
Z3_model_has_interp
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 2464 of file z3++.h.

2464{ return Z3_model_get_num_consts(ctx(), m_model); }
Z3_model_get_num_consts
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 2465 of file z3++.h.

2465{ return Z3_model_get_num_funcs(ctx(), m_model); }
Z3_model_get_num_funcs
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 2445 of file z3++.h.

2445{ return m_model; }

## ◆ operator=()

model & operator= | ( | model const & | s | ) |
| inline

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

2446 {
2447 Z3_model_inc_ref(s.ctx(), s.m_model);
2448 Z3_model_dec_ref(ctx(), m_model);
2449 object::operator=(s);
2450 m_model = s.m_model;
2451 return *this;
2452 }
Z3_model_inc_ref
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 2469 of file z3++.h.

2469 {
2470 assert(0 <= i);
2471 return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
2472 }
z3::model::num_consts
unsigned num_consts() const
Definition: z3++.h:2464
z3::model::get_func_decl
func_decl get_func_decl(unsigned i) const
Definition: z3++.h:2467
z3::model::get_const_decl
func_decl get_const_decl(unsigned i) const
Definition: z3++.h:2466

## ◆ size()

unsigned size | ( |  | ) | const
| inline

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

2468{ return num_consts() + num_funcs(); }
z3::model::num_funcs
unsigned num_funcs() const
Definition: z3++.h:2465

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

## ◆ to_string()

std::string to_string | ( |  | ) | const
| inline

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

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

## Friends And Related Function Documentation

## ◆ operator<<

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

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

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