34 public uint NumConstructors
36 get {
return Native.Z3_get_datatype_sort_num_constructors(
Context.nCtx, NativeObject); }
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++)
90 tmp[j] =
new FuncDecl(
Context, Native.Z3_get_datatype_sort_constructor_accessor(
Context.nCtx, NativeObject, i, 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
Constructors are used for datatype sorts.
The main interaction with Z3 happens via the Context.
The Sort class implements type information for ASTs.
Symbols are used to name several term and type constructors.