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

---

Detailed Description

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

---

Constructor & Destructor Documentation

func_interp	(	context &	c,
		Z3_func_interp	e
	)		[inline]

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

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

func_interp

(

func_interp const &

s

)

[inline]

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

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

~func_interp

(

)

[inline]

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

{ Z3_func_interp_dec_ref(ctx(), m_interp); }

---

Member Function Documentation

expr else_value

(

)

const [inline]

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

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

func_entry entry

(

unsigned

i

)

const [inline]

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

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

unsigned num_entries

(

)

const [inline]

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

Referenced by FuncInterp::entry().

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

operator Z3_func_interp

(

)

const [inline]

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

{ return m_interp; }

func_interp& operator=

(

func_interp const &

s

)

[inline]

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

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