18 package com.microsoft.z3;
32 for (
int i = 0; i < n; i++)
44 for (
int i = 0; i < t.length; i++)
45 t[i] = getContext().
mkApp(cds[i]);
56 for (
int i = 0; i < n; i++)
65 int n = enumNames.length;
66 long[] n_constdecls =
new long[n];
67 long[] n_testers =
new long[n];
69 name.getNativeObject(), (int) n,
Symbol.arrayToNative(enumNames),
70 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)
static long mkEnumerationSort(long a0, long a1, int a2, long[] a3, long[] a4, long[] a5)
FuncDecl[] getTesterDecls()