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

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

Z3: EnumSort Class Reference

Enumeration sorts. More...

Enumeration sorts.

Definition at line 28 of file EnumSort.cs.

Retrieves the inx'th constant in the enumeration.

Parameters

Returns

Definition at line 75 of file EnumSort.cs.

Expr MkApp(FuncDecl f, params Expr[] args)

Create a new function application.

FuncDecl ConstDecl(uint inx)

Retrieves the inx'th constant declaration in the enumeration.

Context Context

Access Context object

Retrieves the inx'th constant declaration in the enumeration.

Parameters

Returns

Definition at line 50 of file EnumSort.cs.

FuncDecl(

, Native.Z3_get_datatype_sort_constructor(

.nCtx, NativeObject, inx));

Referenced by EnumSort.Const().

Retrieves the inx'th tester/recognizer declaration in the enumeration.

Parameters

Returns

Definition at line 101 of file EnumSort.cs.

FuncDecl(

, Native.Z3_get_datatype_sort_recognizer(

.nCtx, NativeObject, inx));

The function declarations of the constants in the enumeration.

Definition at line 33 of file EnumSort.cs.

uint n = Native.Z3_get_datatype_sort_num_constructors(

.nCtx, NativeObject);

FuncDecl[] t =

FuncDecl[n];

(uint i = 0; i < n; i++)

t[i] =

FuncDecl(

, Native.Z3_get_datatype_sort_constructor(

.nCtx, NativeObject, i));

The constants in the enumeration.

Definition at line 58 of file EnumSort.cs.

Expr[] t =

Expr[cds.Length];

(uint i = 0; i < t.Length; i++)

FuncDecl[] ConstDecls

The function declarations of the constants in the enumeration.

The test predicates (recognizers) for the constants in the enumeration.

Definition at line 84 of file EnumSort.cs.

uint n = Native.Z3_get_datatype_sort_num_constructors(

.nCtx, NativeObject);

FuncDecl[] t =

FuncDecl[n];

(uint i = 0; i < n; i++)

t[i] =

FuncDecl(

, Native.Z3_get_datatype_sort_recognizer(

.nCtx, NativeObject, i));

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