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 |
func_entry | ( | context & | c, |
Z3_func_entry | e | ||
) | [inline] |
func_entry | ( | func_entry const & | s | ) | [inline] |
~func_entry | ( | ) | [inline] |
Definition at line 1118 of file z3++.h.
{ Z3_func_entry_dec_ref(ctx(), m_entry); }
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] |
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; }
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); }