Public Member Functions | |
func_interp (context &c, Z3_func_interp e) | |
func_interp (func_interp const &s) | |
~func_interp () override | |
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) | |
virtual | ~object ()=default |
context & | ctx () const |
Z3_error_code | check_error () const |
Additional Inherited Members | |
Protected Attributes inherited from object | |
context * | m_ctx |
|
inline |
|
inline |
|
inlineoverride |
|
inline |
|
inline |
Definition at line 2591 of file z3++.h.
Referenced by FuncInterp::as_list().
|
inline |
Definition at line 2593 of file z3++.h.
Referenced by FuncEntry::__deepcopy__(), FuncEntry::__del__(), FuncEntry::arg_value(), FuncInterp::as_list(), FuncEntry::num_args(), and FuncEntry::value().
|
inline |
Definition at line 2592 of file z3++.h.
Referenced by FuncInterp::as_list(), and FuncInterp::entry().
|
inline |
|
inline |