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 |
func_interp | ( | context & | c, |
Z3_func_interp | e | ||
) | [inline] |
func_interp | ( | func_interp const & | s | ) | [inline] |
~func_interp | ( | ) | [inline] |
Definition at line 1141 of file z3++.h.
{ Z3_func_interp_dec_ref(ctx(), m_interp); }
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] |
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; }