21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
38 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
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);
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];
121 Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
FuncDecl ConstDecl(uint inx)
Retrieves the inx'th constant declaration in the enumeration.
static Z3_sort Z3_mk_enumeration_sort(Z3_context a0, IntPtr a1, uint a2, [In] IntPtr[] a3, [Out] Z3_func_decl[] a4, [Out] Z3_func_decl[] a5)
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)
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.
FuncDecl TesterDecl(uint inx)
Retrieves the inx'th tester/recognizer declaration in the enumeration.