18package com.microsoft.z3;
27 super(ctx, nativeObj);
49 Native.LongPtr constructor =
new Native.LongPtr();
50 Native.LongPtr tester =
new Native.LongPtr();
51 long[] accessors =
new long[n];
52 Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
53 return new FuncDecl<>(getContext(), constructor.value);
63 Native.LongPtr constructor =
new Native.LongPtr();
64 Native.LongPtr tester =
new Native.LongPtr();
65 long[] accessors =
new long[n];
66 Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
67 return new FuncDecl<>(getContext(), tester.value);
77 Native.LongPtr constructor =
new Native.LongPtr();
78 Native.LongPtr tester =
new Native.LongPtr();
79 long[] accessors =
new long[n];
80 Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
82 for (
int i = 0; i < n; i++)
83 t[i] =
new FuncDecl<>(getContext(), accessors[i]);
93 void addToReferenceQueue() {
97 static <R> Constructor<R> of(Context ctx, Symbol name, Symbol recognizer,
98 Symbol[] fieldNames, Sort[] sorts,
int[] sortRefs) {
99 int n = AST.arrayLength(fieldNames);
101 if (n != AST.arrayLength(sorts))
102 throw new Z3Exception(
103 "Number of field names does not match number of sorts");
104 if (sortRefs !=
null && sortRefs.length != n)
105 throw new Z3Exception(
106 "Number of field names does not match number of sort refs");
108 if (sortRefs ==
null)
109 sortRefs =
new int[n];
111 long nativeObj = Native.mkConstructor(ctx.nCtx(), name.getNativeObject(),
112 recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames),
113 Sort.arrayToNative(sorts), sortRefs);
114 return new Constructor<>(ctx, n, nativeObj);
FuncDecl<?>[] getAccessorDecls()
FuncDecl< DatatypeSort< R > > ConstructorDecl()
FuncDecl< BoolSort > getTesterDecl()
IDecRefQueue< Constructor<?> > getConstructorDRQ()
void storeReference(Context ctx, T obj)