18 package com.microsoft.z3;
33 for (
int i = 0; i < n; i++)
56 for (
int i = 0; i < t.length; i++)
57 t[i] = getContext().
mkApp(cds[i]);
79 for (
int i = 0; i < n; i++)
97 int n = enumNames.length;
98 long[] n_constdecls =
new long[n];
99 long[] n_testers =
new long[n];
101 name.getNativeObject(), (int) n,
Symbol.arrayToNative(enumNames),
102 n_constdecls, n_testers));
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
static long getDatatypeSortConstructor(long a0, long a1, int a2)
FuncDecl[] getConstDecls()
Expr mkApp(FuncDecl f, Expr...args)
static int getDatatypeSortNumConstructors(long a0, long a1)
FuncDecl getTesterDecl(int inx)
static long mkEnumerationSort(long a0, long a1, int a2, long[] a3, long[] a4, long[] a5)
FuncDecl getConstDecl(int inx)
FuncDecl[] getTesterDecls()