Definition at line 3492 of file z3++.h.
Definition at line 3500 of file z3++.h.
3501 for (
auto con : cons)
void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr)
Reclaim memory allocated to constructor.
Definition at line 3505 of file z3++.h.
3506 array<unsigned> sort_refs(n);
3507 array<Z3_sort> sorts(n);
3508 array<Z3_symbol> _names(n);
3509 for (
unsigned i = 0; i < n; ++i) sorts[i] = fields[i], _names[i] = names[i];
3510 cons.push_back(
Z3_mk_constructor(ctx, name, rec, n, _names.ptr(), sorts.ptr(), sort_refs.ptr()));
3511 num_fields.push_back(n);
Z3_constructor Z3_API Z3_mk_constructor(Z3_context c, Z3_symbol name, Z3_symbol recognizer, unsigned num_fields, Z3_symbol const field_names[], Z3_sort_opt const sorts[], unsigned sort_refs[])
Create a constructor.
Z3_constructor operator[] |
( |
unsigned |
i | ) |
const |
|
inline |
Definition at line 3518 of file z3++.h.
3519 Z3_func_decl _constructor;
3521 array<Z3_func_decl> accessors(num_fields[i]);
3529 constructor = func_decl(ctx, _constructor);
3531 test = func_decl(ctx, _test);
3532 for (
unsigned j = 0; j < num_fields[i]; ++j)
3533 accs.push_back(func_decl(ctx, accessors[j]));
void Z3_API Z3_query_constructor(Z3_context c, Z3_constructor constr, unsigned num_fields, Z3_func_decl *constructor, Z3_func_decl *tester, Z3_func_decl accessors[])
Query constructor for declared functions.