Z3
Public Member Functions | Friends
constructors Class Reference

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
 

Detailed Description

Definition at line 3492 of file z3++.h.

Constructor & Destructor Documentation

constructors ( context ctx)
inline

Definition at line 3498 of file z3++.h.

3498 : ctx(ctx) {}
~constructors ( )
inline

Definition at line 3500 of file z3++.h.

3500  {
3501  for (auto con : cons)
3502  Z3_del_constructor(ctx, con);
3503  }
void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr)
Reclaim memory allocated to constructor.

Member Function Documentation

void add ( symbol const &  name,
symbol const &  rec,
unsigned  n,
symbol const *  names,
sort const *  fields 
)
inline

Definition at line 3505 of file z3++.h.

3505  {
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);
3512  }
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 3514 of file z3++.h.

3514 { return cons[i]; }
void query ( unsigned  i,
func_decl constructor,
func_decl test,
func_decl_vector accs 
)
inline

Definition at line 3518 of file z3++.h.

3518  {
3519  Z3_func_decl _constructor;
3520  Z3_func_decl _test;
3521  array<Z3_func_decl> accessors(num_fields[i]);
3522  accs.resize(0);
3524  cons[i],
3525  num_fields[i],
3526  &_constructor,
3527  &_test,
3528  accessors.ptr());
3529  constructor = func_decl(ctx, _constructor);
3530 
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]));
3534  }
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.
unsigned size ( ) const
inline

Definition at line 3516 of file z3++.h.

Referenced by constructor_list::constructor_list(), and context::datatype().

3516 { return (unsigned)cons.size(); }

Friends And Related Function Documentation

friend class constructor_list
friend

Definition at line 3493 of file z3++.h.