18 package com.microsoft.z3;
27 super(ctx, nativeObj);
51 long[] accessors =
new long[n];
53 return new FuncDecl(getContext(), constructor.value);
65 long[] accessors =
new long[n];
67 return new FuncDecl(getContext(), tester.value);
79 long[] accessors =
new long[n];
82 for (
int i = 0; i < n; i++)
83 t[i] =
new FuncDecl(getContext(), accessors[i]);
93 void addToReferenceQueue() {
98 Symbol[] fieldNames,
Sort[] sorts,
int[] sortRefs) {
99 int n =
AST.arrayLength(fieldNames);
101 if (n !=
AST.arrayLength(sorts))
103 "Number of field names does not match number of sorts");
104 if (sortRefs != null && sortRefs.length != n)
106 "Number of field names does not match number of sort refs");
108 if (sortRefs == null)
109 sortRefs =
new int[n];
112 recognizer.getNativeObject(), n,
Symbol.arrayToNative(fieldNames),
113 Sort.arrayToNative(sorts), sortRefs);
FuncDecl [] getAccessorDecls()
FuncDecl ConstructorDecl()
void storeReference(Context ctx, T obj)
static void queryConstructor(long a0, long a1, int a2, LongPtr a3, LongPtr a4, long[] a5)
IDecRefQueue< Constructor > getConstructorDRQ()
static long mkConstructor(long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6)