func_entry Class Reference

Inheritance diagram for func_entry:

Public Member Functions
	func_entry (context &c, Z3_func_entry e)
	func_entry (func_entry const &s)
	~func_entry ()
	operator Z3_func_entry () const
func_entry &	operator= (func_entry const &s)
expr	value () const
unsigned	num_args () const
expr	arg (unsigned i) const

---

Detailed Description

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

---

Constructor & Destructor Documentation

func_entry	(	context &	c,
		Z3_func_entry	e
	)		[inline]

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

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

func_entry

(

func_entry const &

s

)

[inline]

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

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

~func_entry

(

)

[inline]

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

{ Z3_func_entry_dec_ref(ctx(), m_entry); }

---

Member Function Documentation

expr arg

(

unsigned

i

)

const [inline]

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

Referenced by ExprRef::children().

{ Z3_ast r = Z3_func_entry_get_arg(ctx(), m_entry, i); check_error(); return expr(ctx(), r); }

unsigned num_args

(

)

const [inline]

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

Referenced by ExprRef::arg(), and ExprRef::children().

{ unsigned r = Z3_func_entry_get_num_args(ctx(), m_entry); check_error(); return r; }

operator Z3_func_entry

(

)

const [inline]

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

{ return m_entry; }

func_entry& operator=

(

func_entry const &

s

)

[inline]

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

                                                     {
            Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
            Z3_func_entry_dec_ref(ctx(), m_entry);
            m_ctx = s.m_ctx; 
            m_entry = s.m_entry;
            return *this; 
        }

expr value

(

)

const [inline]

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

{ Z3_ast r = Z3_func_entry_get_value(ctx(), m_entry); check_error(); return expr(ctx(), r); }