21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
38 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
59 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
63 for (uint i = 0; i < n; i++)
71 : base(ctx, IntPtr.Zero)
73 Contract.Requires(ctx != null);
74 Contract.Requires(name != null);
76 IntPtr t = IntPtr.Zero;
77 IntPtr[] f =
new IntPtr[numFields];
79 Symbol.ArrayToNative(fieldNames),
AST.ArrayToNative(fieldSorts),
static Z3_sort Z3_mk_tuple_sort(Z3_context a0, IntPtr a1, uint a2, [In] IntPtr[] a3, [In] Z3_sort[] a4, [In, Out] ref Z3_func_decl a5, [Out] Z3_func_decl[] a6)
static Z3_func_decl Z3_get_tuple_sort_mk_decl(Z3_context a0, Z3_sort a1)
static Z3_func_decl Z3_get_tuple_sort_field_decl(Z3_context a0, Z3_sort a1, uint a2)
static uint Z3_get_tuple_sort_num_fields(Z3_context a0, Z3_sort a1)
The main interaction with Z3 happens via the Context.
The Sort class implements type information for ASTs.
The abstract syntax tree (AST) class.
Symbols are used to name several term and type constructors.