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++)
104 internal Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
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];
121 NativeObject = Native.Z3_mk_constructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
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)
The main interaction with Z3 happens via the Context.
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.