func_interp Class Reference

Inheritance diagram for func_interp:

Public Member Functions
	func_interp (context &c, Z3_func_interp e)
	func_interp (func_interp const &s)
	~func_interp ()
	operator Z3_func_interp () const
func_interp &	operator= (func_interp const &s)
expr	else_value () const
unsigned	num_entries () const
func_entry	entry (unsigned i) const
void	add_entry (expr_vector const &args, expr &value)
void	set_else (expr &value)
Public Member Functions inherited from object
	object (context &c)
context &	ctx () const
Z3_error_code	check_error () const

Additional Inherited Members
Protected Attributes inherited from object
context *	m_ctx

Detailed Description

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

Constructor & Destructor Documentation

func_interp() [1/2]

func_interp ( context &  c, Z3_func_interp  e  )

inline

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

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

func_interp() [2/2]

func_interp ( func_interp const &  s )

inline

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

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

~func_interp()

~func_interp ( )

inline

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

{ Z3_func_interp_dec_ref(ctx(), m_interp); }

Member Function Documentation

add_entry()

void add_entry ( expr_vector const &  args, expr &  value  )

inline

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

                                                             {
            Z3_func_interp_add_entry(ctx(), m_interp, args, value);
            check_error();
        }

else_value()

expr else_value ( ) const

inline

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

{ Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), r); }

Referenced by FuncInterp::as_list().

entry()

func_entry entry ( unsigned  i ) const

inline

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

{ Z3_func_entry e = Z3_func_interp_get_entry(ctx(), m_interp, i); check_error(); return func_entry(ctx(), e); }

Referenced by FuncEntry::__deepcopy__(), FuncEntry::__del__(), FuncEntry::arg_value(), FuncInterp::as_list(), FuncEntry::num_args(), and FuncEntry::value().

num_entries()

unsigned num_entries ( ) const

inline

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

{ unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; }

Referenced by FuncInterp::as_list(), and FuncInterp::entry().

operator Z3_func_interp()

operator Z3_func_interp ( ) const

inline

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

{ return m_interp; }

operator=()

func_interp& operator= ( func_interp const &  s )

inline

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

                                                       {
            Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
            Z3_func_interp_dec_ref(ctx(), m_interp);
            object::operator=(s);
            m_interp = s.m_interp;
            return *this;
        }

set_else()

void set_else ( expr &  value )

inline

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

                                   {
            Z3_func_interp_set_else(ctx(), m_interp, value);
            check_error();
        }