21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
34 public uint NumConstructors
46 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
48 uint n = NumConstructors;
50 for (uint i = 0; i < n; i++)
63 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
65 uint n = NumConstructors;
67 for (uint i = 0; i < n; i++)
80 Contract.Ensures(Contract.Result<
FuncDecl[][]>() != null);
82 uint n = NumConstructors;
84 for (uint i = 0; i < n; i++)
89 for (uint j = 0; j < ds; j++)
98 internal DatatypeSort(
Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
100 internal DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
101 : base(ctx, Native.
Z3_mk_datatype(ctx.nCtx, name.NativeObject, (uint)constructors.Length, ArrayToNative(constructors)))
103 Contract.Requires(ctx != null);
104 Contract.Requires(name != null);
105 Contract.Requires(constructors != null);
uint DomainSize
The size of the domain of the function declaration Arity
Z3_sort Z3_API Z3_mk_datatype(__in Z3_context c, __in Z3_symbol name, __in unsigned num_constructors, __inout_ecount(num_constructors) Z3_constructor constructors[])
Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.
static Z3_func_decl Z3_get_datatype_sort_recognizer(Z3_context a0, Z3_sort a1, uint a2)
The main interaction with Z3 happens via the Context.
The Sort class implements type information for ASTs.
static uint Z3_get_datatype_sort_num_constructors(Z3_context a0, Z3_sort a1)
static Z3_func_decl Z3_get_datatype_sort_constructor(Z3_context a0, Z3_sort a1, uint a2)
static Z3_func_decl Z3_get_datatype_sort_constructor_accessor(Z3_context a0, Z3_sort a1, uint a2, uint a3)