20using System.Diagnostics;
48 IntPtr constructor = IntPtr.Zero;
49 IntPtr tester = IntPtr.Zero;
50 IntPtr[] accessors =
new IntPtr[n];
51 Native.Z3_query_constructor(
Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
63 IntPtr constructor = IntPtr.Zero;
64 IntPtr tester = IntPtr.Zero;
65 IntPtr[] accessors =
new IntPtr[n];
66 Native.Z3_query_constructor(
Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
78 IntPtr constructor = IntPtr.Zero;
79 IntPtr tester = IntPtr.Zero;
80 IntPtr[] accessors =
new IntPtr[n];
81 Native.Z3_query_constructor(
Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
83 for (uint i = 0; i < n; i++)
94 Native.Z3_del_constructor(
Context.nCtx, NativeObject);
100 internal Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
101 Sort[] sorts, uint[] sortRefs)
104 Debug.Assert(ctx !=
null);
105 Debug.Assert(name !=
null);
106 Debug.Assert(recognizer !=
null);
108 n = AST.ArrayLength(fieldNames);
110 if (n != AST.ArrayLength(sorts))
111 throw new Z3Exception(
"Number of field names does not match number of sorts");
112 if (sortRefs !=
null && sortRefs.Length != n)
113 throw new Z3Exception(
"Number of field names does not match number of sort refs");
115 if (sortRefs ==
null) sortRefs =
new uint[n];
117 NativeObject = Native.Z3_mk_constructor(ctx.nCtx, name.NativeObject, recognizer.NativeObject,
119 Symbol.ArrayToNative(fieldNames),
120 Sort.ArrayToNative(sorts),
Constructors are used for datatype sorts.
FuncDecl[] AccessorDecls
The function declarations of the accessors
uint NumFields
The number of fields of the constructor.
FuncDecl ConstructorDecl
The function declaration of the constructor.
FuncDecl TesterDecl
The function declaration of the tester.
The main interaction with Z3 happens via the Context.
Internal base class for interfacing with native Z3 objects. Should not be used externally.