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
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
Friends
std::ostream &	operator<< (std::ostream &out, model const &m)

---

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.

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

model

(

model const &

s

)

[inline]

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

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

~model

(

)

[inline]

Definition at line 1164 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 1174 of file z3++.h.

                                                                     {
            check_context(*this, n);
            Z3_ast r;
            Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r);
            check_error();
            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 1186 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 1194 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 1187 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 1200 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);
        }

unsigned num_consts

(

)

const [inline]

Definition at line 1184 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 1185 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 1165 of file z3++.h.

{ return m_model; }

model& operator=

(

model const &

s

)

[inline]

Definition at line 1166 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[]

(

int

i

)

const [inline]

Definition at line 1189 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 1188 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 1207 of file z3++.h.

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