18 package com.microsoft.z3;
42 long[] accessors =
new long[n];
44 return new FuncDecl(getContext(), constructor.value);
55 long[] accessors =
new long[n];
57 return new FuncDecl(getContext(), tester.value);
68 long[] accessors =
new long[n];
71 for (
int i = 0; i < n; i++)
72 t[i] =
new FuncDecl(getContext(), accessors[i]);
87 Symbol[] fieldNames,
Sort[] sorts,
int[] sortRefs)
92 n =
AST.arrayLength(fieldNames);
94 if (n !=
AST.arrayLength(sorts))
96 "Number of field names does not match number of sorts");
97 if (sortRefs != null && sortRefs.length != n)
99 "Number of field names does not match number of sort refs");
101 if (sortRefs == null)
102 sortRefs =
new int[n];
105 recognizer.getNativeObject(), n,
Symbol.arrayToNative(fieldNames),
106 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)