Z3
 
Loading...
Searching...
No Matches
constructors Class Reference

#include <z3++.h>

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 3543 of file z3++.h.

Constructor & Destructor Documentation

◆ constructors()

constructors ( context & ctx)
inline

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

3549: ctx(ctx) {}

Referenced by Datatype::__deepcopy__(), Datatype::__repr__(), and Datatype::declare_core().

◆ ~constructors()

~constructors ( )
inline

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

3551 {
3552 for (auto con : cons)
3553 Z3_del_constructor(ctx, con);
3554 }
void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr)
Reclaim memory allocated to constructor.

Member Function Documentation

◆ add()

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

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

3556 {
3557 array<unsigned> sort_refs(n);
3558 array<Z3_sort> sorts(n);
3559 array<Z3_symbol> _names(n);
3560 for (unsigned i = 0; i < n; ++i) sorts[i] = fields[i], _names[i] = names[i];
3561 cons.push_back(Z3_mk_constructor(ctx, name, rec, n, _names.ptr(), sorts.ptr(), sort_refs.ptr()));
3562 num_fields.push_back(n);
3563 }
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.

Referenced by Solver::__iadd__().

◆ operator[]()

Z3_constructor operator[] ( unsigned i) const
inline

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

3565{ return cons[i]; }

◆ query()

void query ( unsigned i,
func_decl & constructor,
func_decl & test,
func_decl_vector & accs )
inline

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

3569 {
3570 Z3_func_decl _constructor;
3571 Z3_func_decl _test;
3572 array<Z3_func_decl> accessors(num_fields[i]);
3573 accs.resize(0);
3575 cons[i],
3576 num_fields[i],
3577 &_constructor,
3578 &_test,
3579 accessors.ptr());
3580 constructor = func_decl(ctx, _constructor);
3581
3582 test = func_decl(ctx, _test);
3583 for (unsigned j = 0; j < num_fields[i]; ++j)
3584 accs.push_back(func_decl(ctx, accessors[j]));
3585 }
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.

◆ size()

unsigned size ( ) const
inline

Friends And Related Symbol Documentation

◆ constructor_list

friend class constructor_list
friend

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