18 package com.microsoft.z3;
45 long[] accessors =
new long[n];
47 return new FuncDecl(getContext(), constructor.value);
59 long[] accessors =
new long[n];
61 return new FuncDecl(getContext(), tester.value);
73 long[] accessors =
new long[n];
76 for (
int i = 0; i < n; i++)
77 t[i] =
new FuncDecl(getContext(), accessors[i]);
93 Symbol[] fieldNames,
Sort[] sorts,
int[] sortRefs)
98 n =
AST.arrayLength(fieldNames);
100 if (n !=
AST.arrayLength(sorts))
102 "Number of field names does not match number of sorts");
103 if (sortRefs != null && sortRefs.length != n)
105 "Number of field names does not match number of sort refs");
107 if (sortRefs == null)
108 sortRefs =
new int[n];
111 recognizer.getNativeObject(), n,
Symbol.arrayToNative(fieldNames),
112 Sort.arrayToNative(sorts), sortRefs));
FuncDecl[] getAccessorDecls()
FuncDecl ConstructorDecl()
static void queryConstructor(long a0, long a1, int a2, LongPtr a3, LongPtr a4, long[] a5)
static void delConstructor(long a0, long a1)
static long mkConstructor(long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6)