21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
49 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
50 IntPtr constructor = IntPtr.Zero;
51 IntPtr tester = IntPtr.Zero;
52 IntPtr[] accessors =
new IntPtr[n];
65 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
66 IntPtr constructor = IntPtr.Zero;
67 IntPtr tester = IntPtr.Zero;
68 IntPtr[] accessors =
new IntPtr[n];
81 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
82 IntPtr constructor = IntPtr.Zero;
83 IntPtr tester = IntPtr.Zero;
84 IntPtr[] accessors =
new IntPtr[n];
87 for (uint i = 0; i < n; i++)
105 Sort[] sorts, uint[] sortRefs)
108 Contract.Requires(ctx != null);
109 Contract.Requires(name != null);
110 Contract.Requires(recognizer != null);
112 n =
AST.ArrayLength(fieldNames);
114 if (n !=
AST.ArrayLength(sorts))
115 throw new Z3Exception(
"Number of field names does not match number of sorts");
116 if (sortRefs != null && sortRefs.Length != n)
117 throw new Z3Exception(
"Number of field names does not match number of sort refs");
119 if (sortRefs == null) sortRefs =
new uint[n];
123 Symbol.ArrayToNative(fieldNames),
124 Sort.ArrayToNative(sorts),
Constructors are used for datatype sorts.
static void Z3_query_constructor(Z3_context a0, Z3_constructor a1, uint a2, [In, Out] ref Z3_func_decl a3, [In, Out] ref Z3_func_decl a4, [Out] Z3_func_decl[] a5)
static Z3_constructor Z3_mk_constructor(Z3_context a0, IntPtr a1, IntPtr a2, uint a3, [In] IntPtr[] a4, [In] Z3_sort[] a5, [In] uint[] a6)
The main interaction with Z3 happens via the Context.
The Sort class implements type information for ASTs.
The exception base class for error reporting from Z3
The abstract syntax tree (AST) class.
static void Z3_del_constructor(Z3_context a0, Z3_constructor a1)
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Symbols are used to name several term and type constructors.