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 () 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.
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 2756 of file z3++.h.

Constructor & Destructor Documentation

model() [1/4]

model ( context &  c )

inline

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

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

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::project(), ModelRef::project_with_witness(), ModelRef::sexpr(), ModelRef::translate(), and ModelRef::update_value().

model() [2/4]

model ( context &  c, Z3_model  m  )

inline

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

: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::project(), ModelRef::project_with_witness(), ModelRef::sexpr(), ModelRef::translate(), and ModelRef::update_value().

model() [3/4]

model ( model const &  s )

inline

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

: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::project(), ModelRef::project_with_witness(), ModelRef::sexpr(), ModelRef::translate(), and ModelRef::update_value().

model() [4/4]

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

inline

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

: object(dst) { init(Z3_model_translate(src.ctx(), src, 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::project(), ModelRef::project_with_witness(), ModelRef::sexpr(), ModelRef::translate(), and ModelRef::update_value().

~model()

~model ( )

inlineoverride

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

{ Z3_model_dec_ref(ctx(), m_model); }

Member Function Documentation

add_const_interp()

void add_const_interp ( func_decl &  f, expr &  value  )

inline

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

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

add_func_interp()

func_interp add_func_interp ( func_decl &  f, expr &  else_val  )

inline

Definition at line 2821 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);
        }

eval()

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

inline

Definition at line 2778 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);
        }

Referenced by ModelRef::evaluate().

get_const_decl()

func_decl get_const_decl ( unsigned  i ) const

inline

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

{ Z3_func_decl r = Z3_model_get_const_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }

Referenced by model::operator[]().

get_const_interp()

expr get_const_interp ( func_decl  c ) const

inline

Definition at line 2801 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);
        }

get_func_decl()

func_decl get_func_decl ( unsigned  i ) const

inline

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

{ Z3_func_decl r = Z3_model_get_func_decl(ctx(), m_model, i); check_error(); return func_decl(ctx(), r); }

Referenced by model::operator[]().

get_func_interp()

func_interp get_func_interp ( func_decl  f ) const

inline

Definition at line 2807 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);
        }

get_sort()

sort get_sort ( unsigned  i ) const

inline

Return the uninterpreted sort at position i.

Precondition

i < num_sorts()

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

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

Referenced by ModelRef::sorts().

has_interp()

bool has_interp ( func_decl  f ) const

inline

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

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

num_consts()

unsigned num_consts ( ) const

inline

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

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

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

num_funcs()

unsigned num_funcs ( ) const

inline

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

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

Referenced by model::size().

num_sorts()

unsigned num_sorts ( ) const

inline

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

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

Referenced by ModelRef::get_sort(), and ModelRef::sorts().

operator Z3_model()

operator Z3_model ( ) const

inline

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

{ return m_model; }

operator=()

model & operator= ( model const &  s )

inline

Definition at line 2770 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;
        }

operator[]()

func_decl operator[] ( int  i ) const

inline

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

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

size()

unsigned size ( ) const

inline

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

{ return num_consts() + num_funcs(); }

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

sort_universe()

expr_vector sort_universe ( sort const &  s ) const

inline

Definition at line 2848 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);
        }

to_string()

std::string to_string ( ) const

inline

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

{ return m_model ? std::string(Z3_model_to_string(ctx(), m_model)) : "null"; }

Friends And Related Symbol Documentation

operator<<

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

friend

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

{ return out << m.to_string(); }