49 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
50 IntPtr constructor = IntPtr.Zero;
51 IntPtr tester = IntPtr.Zero;
52 IntPtr[] accessors =
new IntPtr[n];
53 Native.Z3_query_constructor(
Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
65 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
66 IntPtr constructor = IntPtr.Zero;
67 IntPtr tester = IntPtr.Zero;
68 IntPtr[] accessors =
new IntPtr[n];
69 Native.Z3_query_constructor(
Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
81 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
82 IntPtr constructor = IntPtr.Zero;
83 IntPtr tester = IntPtr.Zero;
84 IntPtr[] accessors =
new IntPtr[n];
85 Native.Z3_query_constructor(
Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
87 for (uint i = 0; i < n; i++)
98 Native.Z3_del_constructor(
Context.nCtx, NativeObject);
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.
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.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Symbols are used to name several term and type constructors.