Public Member Functions | |
constructors (context &ctx) | |
~constructors () | |
void | add (symbol const &name, symbol const &rec, unsigned n, symbol const *names, sort const *fields) |
Z3_constructor | operator[] (unsigned i) const |
unsigned | size () const |
void | query (unsigned i, func_decl &constructor, func_decl &test, func_decl_vector &accs) |
Friends | |
class | constructor_list |
|
inline |
Definition at line 3549 of file z3++.h.
Referenced by Datatype::__deepcopy__(), Datatype::__repr__(), and Datatype::declare_core().
|
inline |
|
inline |
Definition at line 3556 of file z3++.h.
Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().
|
inline |
|
inline |
|
inline |
Definition at line 3567 of file z3++.h.
Referenced by ParamDescrsRef::__len__(), Goal::__len__(), BitVecNumRef::as_signed_long(), constructor_list::constructor_list(), context::datatype(), and BitVecSortRef::subsort().
|
friend |