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

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)

unsigned	num_sorts () const

sort	get_sort (unsigned i) const
	Return the uninterpreted sort at position `i`. More...

expr_vector	sort_universe (sort const &s) const

std::string	to_string () const

Public Member Functions inherited from object
	object (context &c)

virtual	~object ()=default

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 2712 of file z3++.h.

Constructor & Destructor Documentation

model ( context & c )

inline

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

2720 :object(c) { init(Z3_mk_model(c)); }

Z3_mk_model

Z3_model Z3_API Z3_mk_model(Z3_context c)

Create a fresh model object. It has reference count 0.

z3::object::object

object(context &c)

Definition: z3++.h:538

model	(	context &	c,
		Z3_model	m
	)

inline

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

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

z3::object::object

object(context &c)

Definition: z3++.h:538

model ( model const & s )

inline

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

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

z3::object::object

object(context &c)

Definition: z3++.h:538

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

inline

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

2723 : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); }

z3::object::object

object(context &c)

Definition: z3++.h:538

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.

~model ( )

inlineoverride

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

2724 { Z3_model_dec_ref(ctx(), m_model); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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

void add_const_interp	(	func_decl &	f,
		expr &	value
	)

inline

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

                                                          {
             Z3_add_const_interp(ctx(), m_model, f, value);
             check_error();
         }

func_interp add_func_interp	(	func_decl &	f,
		expr &	else_val
	)

inline

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

                                                                   {
             Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val);
             check_error();
             return func_interp(ctx(), r);
         }

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

inline

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

                                                                      {
             check_context(*this, n);
             Z3_ast r = 0;
             bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
             check_error();
             if (status == false && ctx().enable_exceptions())
                 Z3_THROW(exception("failed to evaluate expression"));
             return expr(ctx(), r);
         }

func_decl get_const_decl ( unsigned i ) const

inline

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

Referenced by model::operator[]().

2746 { 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.

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

expr get_const_interp ( func_decl c ) const

inline

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

                                                  {
             check_context(*this, c);
             Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c);
             check_error();
             return expr(ctx(), r);
         }

func_decl get_func_decl ( unsigned i ) const

inline

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

Referenced by model::operator[]().

2747 { 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.

z3::object::check_error

Z3_error_code check_error() const

Definition: z3++.h:541

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

func_interp get_func_interp ( func_decl f ) const

inline

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

                                                        {
             check_context(*this, f);
             Z3_func_interp r = Z3_model_get_func_interp(ctx(), m_model, f);
             check_error();
             return func_interp(ctx(), r);
         }

sort get_sort ( unsigned i ) const

inline

Return the uninterpreted sort at position i.

Precondition: i < num_sorts()

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

                                         {
             Z3_sort s = Z3_model_get_sort(ctx(), m_model, i);
             check_error();
             return sort(ctx(), s);
         }

bool has_interp ( func_decl f ) const

inline

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

                                            {
             check_context(*this, f);
             return Z3_model_has_interp(ctx(), m_model, f);
         }

unsigned num_consts ( ) const

inline

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

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

2744 { return Z3_model_get_num_consts(ctx(), m_model); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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.

unsigned num_funcs ( ) const

inline

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

Referenced by model::size().

2745 { return Z3_model_get_num_funcs(ctx(), m_model); }

z3::object::ctx

context & ctx() const

Definition: z3++.h:540

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.

unsigned num_sorts ( ) const

inline

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

                                    {
             unsigned r = Z3_model_get_num_sorts(ctx(), m_model);
             check_error();
             return r;
         }

operator Z3_model ( ) const

inline

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

2725 { return m_model; }

model& operator= ( model const & s )

inline

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

                                            {
             Z3_model_inc_ref(s.ctx(), s.m_model);
             Z3_model_dec_ref(ctx(), m_model);
             object::operator=(s);
             m_model = s.m_model;
             return *this;
         }

func_decl operator[] ( int i ) const

inline

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

                                           {
             assert(0 <= i);
             return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
         }

unsigned size ( ) const

inline

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

2748 { return num_consts() + num_funcs(); }

z3::model::num_consts

unsigned num_consts() const

Definition: z3++.h:2744

z3::model::num_funcs

unsigned num_funcs() const

Definition: z3++.h:2745

expr_vector sort_universe ( sort const & s ) const

inline

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

                                                        {
             check_context(*this, s);
             Z3_ast_vector r = Z3_model_get_sort_universe(ctx(), m_model, s);
             check_error();
             return expr_vector(ctx(), r);
         }