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); }
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
static Z3_sort Z3_mk_datatype(Z3_context a0, IntPtr a1, uint a2, [In, Out] Z3_constructor[] a3)
Constructors are used for datatype sorts.
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)
Symbols are used to name several term and type constructors.
static Z3_func_decl Z3_get_datatype_sort_constructor_accessor(Z3_context a0, Z3_sort a1, uint a2, uint a3)