38 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
39 uint n = Native.Z3_get_datatype_sort_num_constructors(
Context.nCtx, NativeObject);
41 for (uint i = 0; i < n; i++)
64 Contract.Ensures(Contract.Result<
Expr[]>() != null);
67 for (uint i = 0; i < t.Length; i++)
90 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
91 uint n = Native.Z3_get_datatype_sort_num_constructors(
Context.nCtx, NativeObject);
93 for (uint i = 0; i < n; i++)
111 : base(ctx, IntPtr.Zero)
113 Contract.Requires(ctx != null);
114 Contract.Requires(name != null);
115 Contract.Requires(enumNames != null);
117 int n = enumNames.Length;
118 IntPtr[] n_constdecls =
new IntPtr[n];
119 IntPtr[] n_testers =
new IntPtr[n];
120 NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
121 Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
FuncDecl ConstDecl(uint inx)
Retrieves the inx'th constant declaration in the enumeration.
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Expr Const(uint inx)
Retrieves the inx'th constant in the enumeration.
def EnumSort(name, values, ctx=None)
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.
FuncDecl TesterDecl(uint inx)
Retrieves the inx'th tester/recognizer declaration in the enumeration.