20using System.Diagnostics;
35 get {
return Native.Z3_get_datatype_sort_num_constructors(
Context.nCtx, NativeObject); }
48 for (uint i = 0; i < n; i++)
64 for (uint i = 0; i < n; i++)
80 for (uint i = 0; i < n; i++)
85 for (uint j = 0; j < ds; j++)
86 tmp[j] =
new FuncDecl(
Context, Native.Z3_get_datatype_sort_constructor_accessor(
Context.nCtx, NativeObject, i, j));
94 internal DatatypeSort(
Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx !=
null); }
96 internal DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
97 : base(ctx, Native.
Z3_mk_datatype(ctx.nCtx, name.NativeObject, (uint)constructors.
Length, ArrayToNative(constructors)))
99 Debug.Assert(ctx !=
null);
100 Debug.Assert(name !=
null);
101 Debug.Assert(constructors !=
null);
The main interaction with Z3 happens via the Context.
FuncDecl[] Constructors
The constructors.
uint NumConstructors
The number of constructors of the datatype sort.
FuncDecl[][] Accessors
The constructor accessors.
FuncDecl[] Recognizers
The recognizers.
uint DomainSize
The size of the domain of the function declaration Arity
The Sort class implements type information for ASTs.
Z3_sort Z3_API Z3_mk_datatype(Z3_context c, Z3_symbol name, unsigned num_constructors, Z3_constructor constructors[])
Create datatype, such as lists, trees, records, enumerations or unions of records....