Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/classz3_1_1constructors.html below:

Z3: constructors Class Reference

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

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

(

con : cons)

void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr)

Reclaim memory allocated to constructor.

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

array<unsigned> sort_refs(n);

array<Z3_sort> sorts(n);

array<Z3_symbol> _names(n);

(

i = 0; i < n; ++i) sorts[i] = fields[i], _names[i] = names[i];

cons.push_back(

(ctx, name, rec, n, _names.ptr(), sorts.ptr(), sort_refs.ptr()));

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.

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

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

array<Z3_func_decl> accessors(num_fields[i]);

constructor = func_decl(ctx, _constructor);

test = func_decl(ctx, _test);

(

j = 0; j < num_fields[i]; ++j)

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.

System.IntPtr Z3_func_decl

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4