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

Constructor & Destructor Documentation

constructors()

constructors ( context &  ctx )

inline

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

: ctx(ctx) {}

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

~constructors()

~constructors ( )

inline

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

                        {
            for (auto con : cons)
                Z3_del_constructor(ctx, con);           
        }

Member Function Documentation

add()

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

inline

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

                                                                                                             {
            array<unsigned> sort_refs(n);
            array<Z3_sort> sorts(n);
            array<Z3_symbol> _names(n);            
            for (unsigned i = 0; i < n; ++i) sorts[i] = fields[i], _names[i] = names[i];
            cons.push_back(Z3_mk_constructor(ctx, name, rec, n, _names.ptr(), sorts.ptr(), sort_refs.ptr()));
            num_fields.push_back(n);
        }

Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().

operator[]()

Z3_constructor operator[] ( unsigned  i ) const

inline

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

{ return cons[i]; }

query()

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

inline

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

                                                                                                {
            Z3_func_decl _constructor;
            Z3_func_decl _test;
            array<Z3_func_decl> accessors(num_fields[i]);
            accs.resize(0);
            Z3_query_constructor(ctx,
                                 cons[i],
                                 num_fields[i],
                                 &_constructor,
                                 &_test,
                                 accessors.ptr());
            constructor = func_decl(ctx, _constructor);
 
            test = func_decl(ctx, _test);
            for (unsigned j = 0; j < num_fields[i]; ++j)
                accs.push_back(func_decl(ctx, accessors[j]));
        }

size()

unsigned size ( ) const

inline

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

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

Referenced by ParamDescrsRef::__len__(), Goal::__len__(), BitVecNumRef::as_signed_long(), constructor_list::constructor_list(), context::datatype(), and BitVecSortRef::subsort().

Friends And Related Function Documentation

constructor_list

friend class constructor_list

friend

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