#include <z3++.h>
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 |
Definition at line 2580 of file z3++.h.
Referenced by func_interp(), and operator=().
|
inline |
|
inlineoverride |
Definition at line 2582 of file z3++.h.
|
inline |
Definition at line 2594 of file z3++.h.
|
inline |
|
inline |
Definition at line 2593 of file z3++.h.
|
inline |
|
inline |
|
inline |
Definition at line 2584 of file z3++.h.
|
inline |
Definition at line 2598 of file z3++.h.