2 package com.microsoft.z3;
5 public static class IntPtr {
public int value; }
6 public static class LongPtr {
public long value; }
7 public static class StringPtr {
public String value; }
8 public static class ObjArrayPtr {
public long[] value; }
9 public static class UIntArrayPtr {
public int[] value; }
13 try {
System.load(
"/usr/lib64/z3/z3java.so"); }
14 catch (UnsatisfiedLinkError ex) {
System.load(
"/usr/lib64/z3/libz3java.so"); }
54 protected static native
long INTERNALmkTupleSort(
long a0,
long a1,
int a2,
long[] a3,
long[] a4, LongPtr a5,
long[] a6);
56 protected static native
long INTERNALmkListSort(
long a0,
long a1,
long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8);
57 protected static native
long INTERNALmkConstructor(
long a0,
long a1,
long a2,
int a3,
long[] a4,
long[] a5,
int[] a6);
62 protected static native
void INTERNALmkDatatypes(
long a0,
int a1,
long[] a2,
long[] a3,
long[] a4);
64 protected static native
long INTERNALmkFuncDecl(
long a0,
long a1,
int a2,
long[] a3,
long a4);
65 protected static native
long INTERNALmkApp(
long a0,
long a1,
int a2,
long[] a3);
66 protected static native
long INTERNALmkConst(
long a0,
long a1,
long a2);
71 protected static native
long INTERNALmkEq(
long a0,
long a1,
long a2);
74 protected static native
long INTERNALmkIte(
long a0,
long a1,
long a2,
long a3);
75 protected static native
long INTERNALmkIff(
long a0,
long a1,
long a2);
77 protected static native
long INTERNALmkXor(
long a0,
long a1,
long a2);
78 protected static native
long INTERNALmkAnd(
long a0,
int a1,
long[] a2);
79 protected static native
long INTERNALmkOr(
long a0,
int a1,
long[] a2);
80 protected static native
long INTERNALmkAdd(
long a0,
int a1,
long[] a2);
81 protected static native
long INTERNALmkMul(
long a0,
int a1,
long[] a2);
82 protected static native
long INTERNALmkSub(
long a0,
int a1,
long[] a2);
84 protected static native
long INTERNALmkDiv(
long a0,
long a1,
long a2);
85 protected static native
long INTERNALmkMod(
long a0,
long a1,
long a2);
86 protected static native
long INTERNALmkRem(
long a0,
long a1,
long a2);
87 protected static native
long INTERNALmkPower(
long a0,
long a1,
long a2);
88 protected static native
long INTERNALmkLt(
long a0,
long a1,
long a2);
89 protected static native
long INTERNALmkLe(
long a0,
long a1,
long a2);
90 protected static native
long INTERNALmkGt(
long a0,
long a1,
long a2);
91 protected static native
long INTERNALmkGe(
long a0,
long a1,
long a2);
98 protected static native
long INTERNALmkBvand(
long a0,
long a1,
long a2);
99 protected static native
long INTERNALmkBvor(
long a0,
long a1,
long a2);
100 protected static native
long INTERNALmkBvxor(
long a0,
long a1,
long a2);
102 protected static native
long INTERNALmkBvnor(
long a0,
long a1,
long a2);
105 protected static native
long INTERNALmkBvadd(
long a0,
long a1,
long a2);
106 protected static native
long INTERNALmkBvsub(
long a0,
long a1,
long a2);
107 protected static native
long INTERNALmkBvmul(
long a0,
long a1,
long a2);
113 protected static native
long INTERNALmkBvult(
long a0,
long a1,
long a2);
114 protected static native
long INTERNALmkBvslt(
long a0,
long a1,
long a2);
115 protected static native
long INTERNALmkBvule(
long a0,
long a1,
long a2);
116 protected static native
long INTERNALmkBvsle(
long a0,
long a1,
long a2);
117 protected static native
long INTERNALmkBvuge(
long a0,
long a1,
long a2);
118 protected static native
long INTERNALmkBvsge(
long a0,
long a1,
long a2);
119 protected static native
long INTERNALmkBvugt(
long a0,
long a1,
long a2);
120 protected static native
long INTERNALmkBvsgt(
long a0,
long a1,
long a2);
122 protected static native
long INTERNALmkExtract(
long a0,
int a1,
int a2,
long a3);
126 protected static native
long INTERNALmkBvshl(
long a0,
long a1,
long a2);
134 protected static native
long INTERNALmkBv2int(
long a0,
long a1,
boolean a2);
144 protected static native
long INTERNALmkStore(
long a0,
long a1,
long a2,
long a3);
146 protected static native
long INTERNALmkMap(
long a0,
long a1,
int a2,
long[] a3);
160 protected static native
long INTERNALmkReal(
long a0,
int a1,
int a2);
161 protected static native
long INTERNALmkInt(
long a0,
int a1,
long a2);
163 protected static native
long INTERNALmkInt64(
long a0,
long a1,
long a2);
166 protected static native
long INTERNALmkBound(
long a0,
int a1,
long a2);
167 protected static native
long INTERNALmkForall(
long a0,
int a1,
int a2,
long[] a3,
int a4,
long[] a5,
long[] a6,
long a7);
168 protected static native
long INTERNALmkExists(
long a0,
int a1,
int a2,
long[] a3,
int a4,
long[] a5,
long[] a6,
long a7);
169 protected static native
long INTERNALmkQuantifier(
long a0,
boolean a1,
int a2,
int a3,
long[] a4,
int a5,
long[] a6,
long[] a7,
long a8);
170 protected static native
long INTERNALmkQuantifierEx(
long a0,
boolean a1,
int a2,
long a3,
long a4,
int a5,
long[] a6,
int a7,
long[] a8,
int a9,
long[] a10,
long[] a11,
long a12);
171 protected static native
long INTERNALmkForallConst(
long a0,
int a1,
int a2,
long[] a3,
int a4,
long[] a5,
long a6);
172 protected static native
long INTERNALmkExistsConst(
long a0,
int a1,
int a2,
long[] a3,
int a4,
long[] a5,
long a6);
173 protected static native
long INTERNALmkQuantifierConst(
long a0,
boolean a1,
int a2,
int a3,
long[] a4,
int a5,
long[] a6,
long a7);
174 protected static native
long INTERNALmkQuantifierConstEx(
long a0,
boolean a1,
int a2,
long a3,
long a4,
int a5,
long[] a6,
int a7,
long[] a8,
int a9,
long[] a10,
long a11);
181 protected static native
boolean INTERNALisEqSort(
long a0,
long a1,
long a2);
197 protected static native
long INTERNALmkAtmost(
long a0,
int a1,
long[] a2,
int a3);
198 protected static native
long INTERNALmkPble(
long a0,
int a1,
long[] a2,
int[] a3,
int a4);
221 protected static native
boolean INTERNALisEqAst(
long a0,
long a1,
long a2);
228 protected static native
boolean INTERNALisApp(
long a0,
long a1);
231 protected static native
long INTERNALtoApp(
long a0,
long a1);
264 protected static native
long INTERNALsubstitute(
long a0,
long a1,
int a2,
long[] a3,
long[] a4);
269 protected static native
boolean INTERNALmodelEval(
long a0,
long a1,
long a2,
boolean a3, LongPtr a4);
304 protected static native
long INTERNALparseSmtlib2String(
long a0, String a1,
int a2,
long[] a3,
long[] a4,
int a5,
long[] a6,
long[] a7);
305 protected static native
long INTERNALparseSmtlib2File(
long a0, String a1,
int a2,
long[] a3,
long[] a4,
int a5,
long[] a6,
long[] a7);
306 protected static native
void INTERNALparseSmtlibString(
long a0, String a1,
int a2,
long[] a3,
long[] a4,
int a5,
long[] a6,
long[] a7);
307 protected static native
void INTERNALparseSmtlibFile(
long a0, String a1,
int a2,
long[] a3,
long[] a4,
int a5,
long[] a6,
long[] a7);
321 protected static native
void INTERNALgetVersion(IntPtr a0, IntPtr a1, IntPtr a2, IntPtr a3);
393 protected static native
long INTERNALmkGoal(
long a0,
boolean a1,
boolean a2,
boolean a3);
428 protected static native
long INTERNALprobeLt(
long a0,
long a1,
long a2);
429 protected static native
long INTERNALprobeGt(
long a0,
long a1,
long a2);
430 protected static native
long INTERNALprobeLe(
long a0,
long a1,
long a2);
431 protected static native
long INTERNALprobeGe(
long a0,
long a1,
long a2);
432 protected static native
long INTERNALprobeEq(
long a0,
long a1,
long a2);
434 protected static native
long INTERNALprobeOr(
long a0,
long a1,
long a2);
489 protected static native
void INTERNALpop(
long a0,
int a1);
495 protected static native
int INTERNALcheckAssumptions(
long a0,
int a1,
long[] a2, LongPtr a3, LongPtr a4, IntPtr a5,
long[] a6);
500 protected static native
long INTERNALmkLabel(
long a0,
long a1,
boolean a2,
long a3);
516 protected static native
void INTERNALgetArrayValue(
long a0,
long a1,
long a2,
int a3,
long[] a4,
long[] a5, LongPtr a6);
522 protected static native
boolean INTERNALeval(
long a0,
long a1,
long a2, LongPtr a3);
523 protected static native
boolean INTERNALevalDecl(
long a0,
long a1,
long a2,
int a3,
long[] a4, LongPtr a5);
553 protected static native
int INTERNALrcfMkRoots(
long a0,
int a1,
long[] a2,
long[] a3);
554 protected static native
long INTERNALrcfAdd(
long a0,
long a1,
long a2);
555 protected static native
long INTERNALrcfSub(
long a0,
long a1,
long a2);
556 protected static native
long INTERNALrcfMul(
long a0,
long a1,
long a2);
557 protected static native
long INTERNALrcfDiv(
long a0,
long a1,
long a2);
561 protected static native
boolean INTERNALrcfLt(
long a0,
long a1,
long a2);
562 protected static native
boolean INTERNALrcfGt(
long a0,
long a1,
long a2);
563 protected static native
boolean INTERNALrcfLe(
long a0,
long a1,
long a2);
564 protected static native
boolean INTERNALrcfGe(
long a0,
long a1,
long a2);
565 protected static native
boolean INTERNALrcfEq(
long a0,
long a1,
long a2);
566 protected static native
boolean INTERNALrcfNeq(
long a0,
long a1,
long a2);
575 protected static native
int INTERNALreadInterpolationProblem(
long a0, IntPtr a1, ObjArrayPtr a2, UIntArrayPtr a3, String a4, StringPtr a5, IntPtr a6, ObjArrayPtr a7);
576 protected static native
int INTERNALcheckInterpolant(
long a0,
int a1,
long[] a2,
int[] a3,
long[] a4, StringPtr a5,
int a6,
long[] a7);
599 protected static native
long INTERNALmkFpaInf(
long a0,
long a1,
boolean a2);
601 protected static native
long INTERNALmkFpaFp(
long a0,
long a1,
long a2,
long a3);
609 protected static native
long INTERNALmkFpaAdd(
long a0,
long a1,
long a2,
long a3);
610 protected static native
long INTERNALmkFpaSub(
long a0,
long a1,
long a2,
long a3);
611 protected static native
long INTERNALmkFpaMul(
long a0,
long a1,
long a2,
long a3);
612 protected static native
long INTERNALmkFpaDiv(
long a0,
long a1,
long a2,
long a3);
613 protected static native
long INTERNALmkFpaFma(
long a0,
long a1,
long a2,
long a3,
long a4);
620 protected static native
long INTERNALmkFpaLt(
long a0,
long a1,
long a2);
622 protected static native
long INTERNALmkFpaGt(
long a0,
long a1,
long a2);
623 protected static native
long INTERNALmkFpaEq(
long a0,
long a1,
long a2);
686 throw new Z3Exception(
"Object allocation failed.");
694 throw new Z3Exception(
"Object allocation failed.");
960 public static long mkListSort(
long a0,
long a1,
long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8)
throws Z3Exception 1955 public static long mkForall(
long a0,
int a1,
int a2,
long[] a3,
int a4,
long[] a5,
long[] a6,
long a7)
throws Z3Exception 1964 public static long mkExists(
long a0,
int a1,
int a2,
long[] a3,
int a4,
long[] a5,
long[] a6,
long a7)
throws Z3Exception 1973 public static long mkQuantifier(
long a0,
boolean a1,
int a2,
int a3,
long[] a4,
int a5,
long[] a6,
long[] a7,
long a8)
throws Z3Exception 1982 public static long mkQuantifierEx(
long a0,
boolean a1,
int a2,
long a3,
long a4,
int a5,
long[] a6,
int a7,
long[] a8,
int a9,
long[] a10,
long[] a11,
long a12)
throws Z3Exception 1984 long res =
INTERNALmkQuantifierEx(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12);
2018 public static long mkQuantifierConstEx(
long a0,
boolean a1,
int a2,
long a3,
long a4,
int a5,
long[] a6,
int a7,
long[] a8,
int a9,
long[] a10,
long a11)
throws Z3Exception 2020 long res =
INTERNALmkQuantifierConstEx(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11);
3310 public static void getVersion(IntPtr a0, IntPtr a1, IntPtr a2, IntPtr a3)
static native boolean INTERNALgetNumeralUint(long a0, long a1, IntPtr a2)
static int statsSize(long a0, long a1)
static long mkFpaFp(long a0, long a1, long a2, long a3)
static void solverDecRef(long a0, long a1)
static native long INTERNALmkBvslt(long a0, long a1, long a2)
static long mkFpaToFpSigned(long a0, long a1, long a2, long a3)
static void fixedpointUpdateRule(long a0, long a1, long a2, long a3)
static native void INTERNALoptimizeIncRef(long a0, long a1)
static long tacticRepeat(long a0, long a1, int a2)
static native long INTERNALgetSmtlibFormula(long a0, int a1)
static native void INTERNALassertCnstr(long a0, long a1)
static native boolean INTERNALisEqAst(long a0, long a1, long a2)
static native long INTERNALmkFpaToSbv(long a0, long a1, long a2, int a3)
static boolean algebraicEq(long a0, long a1, long a2)
static native long INTERNALgetArraySortDomain(long a0, long a1)
static boolean getNumeralUint(long a0, long a1, IntPtr a2)
static long getQuantifierPatternAst(long a0, long a1, int a2)
static long mkBvule(long a0, long a1, long a2)
static native long INTERNALgetGuessedLiterals(long a0)
static long mkSolver(long a0)
static long mkFpaToFpUnsigned(long a0, long a1, long a2, long a3)
static native long INTERNALmkBvxor(long a0, long a1, long a2)
static native long INTERNALmkBvnand(long a0, long a1, long a2)
static native long INTERNALmkFpaToFpIntReal(long a0, long a1, long a2, long a3, long a4)
static native long INTERNALfuncInterpGetEntry(long a0, long a1, int a2)
static native long INTERNALfuncDeclToAst(long a0, long a1)
static native long INTERNALgetArraySortRange(long a0, long a1)
static native long INTERNALmkRealSort(long a0)
static native long INTERNALmkGoal(long a0, boolean a1, boolean a2, boolean a3)
static native void INTERNALdelConstructor(long a0, long a1)
static native long INTERNALrcfPower(long a0, long a1, int a2)
static native int INTERNALgetNumTactics(long a0)
static native String INTERNALgetErrorMsg(int a0)
static int getQuantifierNumPatterns(long a0, long a1)
static native int INTERNALoptimizeMinimize(long a0, long a1, long a2)
static long mkExtract(long a0, int a1, int a2, long a3)
static void interrupt(long a0)
static long funcInterpGetElse(long a0, long a1)
static long getSmtlibSort(long a0, int a1)
static String astMapToString(long a0, long a1)
static native long INTERNALsolverGetAssertions(long a0, long a1)
static long mkForallConst(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6)
static native int INTERNALmodelGetNumFuncs(long a0, long a1)
static native int INTERNALfixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
static void paramsSetDouble(long a0, long a1, long a2, double a3)
static int applyResultGetNumSubgoals(long a0, long a1)
static native long INTERNALmkMul(long a0, int a1, long[] a2)
static native String INTERNALoptimizeToString(long a0, long a1)
static native long INTERNALsolverGetModel(long a0, long a1)
static native long INTERNALfixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
static int getBoolValue(long a0, long a1)
static long mkMod(long a0, long a1, long a2)
static native long INTERNALmkApp(long a0, long a1, int a2, long[] a3)
static native long INTERNALmkSetSubset(long a0, long a1, long a2)
static native long INTERNALmkProbe(long a0, String a1)
static native void INTERNALupdateParamValue(long a0, String a1, String a2)
static long mkBvugt(long a0, long a1, long a2)
static int fpaGetEbits(long a0, long a1)
static long algebraicDiv(long a0, long a1, long a2)
static native boolean INTERNALalgebraicIsNeg(long a0, long a1)
static native long INTERNALmkFpaToReal(long a0, long a1)
static long optimizeGetUpper(long a0, long a1, int a2)
static native boolean INTERNALrcfLt(long a0, long a1, long a2)
static void delConfig(long a0)
static int getSmtlibNumSorts(long a0)
static long mkBvredor(long a0, long a1)
static native void INTERNALfixedpointPop(long a0, long a1)
static String tacticGetHelp(long a0, long a1)
static native long INTERNALtoApp(long a0, long a1)
static native long INTERNALtacticApplyEx(long a0, long a1, long a2, long a3)
static long tacticOrElse(long a0, long a1, long a2)
static void paramDescrsDecRef(long a0, long a1)
static int getModelFuncEntryNumArgs(long a0, long a1, int a2, int a3)
static long getDeclFuncDeclParameter(long a0, long a1, int a2)
static void push(long a0)
static int getNumLiterals(long a0, long a1)
static long rcfMkE(long a0)
static void globalParamResetAll()
static native void INTERNALresetMemory()
static native long INTERNALgetDatatypeSortRecognizer(long a0, long a1, int a2)
static native long INTERNALgetModelFuncEntryValue(long a0, long a1, int a2, int a3)
static native long INTERNALmkInjectiveFunction(long a0, long a1, int a2, long[] a3, long a4)
static long mkFpaNeg(long a0, long a1)
static native long INTERNALgetQuantifierBody(long a0, long a1)
static void applyResultIncRef(long a0, long a1)
static long getModelFuncEntryArg(long a0, long a1, int a2, int a3, int a4)
static int getNumProbes(long a0)
static native long INTERNALmodelGetSort(long a0, long a1, int a2)
static native long INTERNALmkFpaToUbv(long a0, long a1, long a2, int a3)
static long mkFuncDecl(long a0, long a1, int a2, long[] a3, long a4)
static boolean getNumeralRationalInt64(long a0, long a1, LongPtr a2, LongPtr a3)
static native long INTERNALfuncEntryGetArg(long a0, long a1, int a2)
static native long INTERNALmkSetIntersect(long a0, int a1, long[] a2)
static native long INTERNALmkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
static void parseSmtlibFile(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static long mkNumeral(long a0, String a1, long a2)
static native long INTERNALmkAdd(long a0, int a1, long[] a2)
static native boolean INTERNALrcfLe(long a0, long a1, long a2)
static native String INTERNALastMapToString(long a0, long a1)
static void optimizePop(long a0, long a1)
static native long INTERNALprobeEq(long a0, long a1, long a2)
static native long INTERNALoptimizeGetStatistics(long a0, long a1)
static long mkFpaDiv(long a0, long a1, long a2, long a3)
static void updateParamValue(long a0, String a1, String a2)
static void toggleWarningMessages(boolean a0)
static String getSymbolString(long a0, long a1)
static native long INTERNALmkFpaMin(long a0, long a1, long a2)
static boolean algebraicNeq(long a0, long a1, long a2)
static native void INTERNALfixedpointDecRef(long a0, long a1)
static void astMapErase(long a0, long a1, long a2)
static long mkFreshConst(long a0, String a1, long a2)
static void paramsSetSymbol(long a0, long a1, long a2, long a3)
static native int INTERNALgetModelNumFuncs(long a0, long a1)
static long algebraicMul(long a0, long a1, long a2)
static String solverGetReasonUnknown(long a0, long a1)
static native long INTERNALgetDenominator(long a0, long a1)
static native double INTERNALgetDeclDoubleParameter(long a0, long a1, int a2)
static native long INTERNALmkFalse(long a0)
static native String INTERNALgetNumeralDecimalString(long a0, long a1, int a2)
static void persistAst(long a0, long a1, int a2)
static long mkTactic(long a0, String a1)
static native long INTERNALmkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
static long getArraySortRange(long a0, long a1)
static native int INTERNALmodelGetNumConsts(long a0, long a1)
static native void INTERNALoptimizePush(long a0, long a1)
static native boolean INTERNALglobalParamGet(String a0, StringPtr a1)
static native int INTERNALgetDatatypeSortNumConstructors(long a0, long a1)
static native long INTERNALparseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static native int INTERNALgetImpliedEqualities(long a0, long a1, int a2, long[] a3, int[] a4)
static native int INTERNALstatsSize(long a0, long a1)
static boolean algebraicIsZero(long a0, long a1)
static native boolean INTERNALisAsArray(long a0, long a1)
static native boolean INTERNALgetNumeralSmall(long a0, long a1, LongPtr a2, LongPtr a3)
static long mkProbe(long a0, String a1)
static native String INTERNALsimplifyGetHelp(long a0)
static native void INTERNALoptimizeAssert(long a0, long a1, long a2)
static native long INTERNALmkFpaIsNegative(long a0, long a1)
static native void INTERNALstatsDecRef(long a0, long a1)
static long modelGetSort(long a0, long a1, int a2)
static long mkDatatype(long a0, long a1, int a2, long[] a3)
static native void INTERNALfuncEntryDecRef(long a0, long a1)
static native long INTERNALtacticFailIf(long a0, long a1)
static native long INTERNALgetRelevantLabels(long a0)
static native long INTERNALmkFpaSortHalf(long a0)
static native String INTERNALfpaGetNumeralSignificandString(long a0, long a1)
static native long INTERNALmkNot(long a0, long a1)
static long mkFpaIsNegative(long a0, long a1)
static native long INTERNALfuncEntryGetValue(long a0, long a1)
static native long INTERNALgetDomain(long a0, long a1, int a2)
static long mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
static native long INTERNALmkBvsub(long a0, long a1, long a2)
static int paramDescrsGetKind(long a0, long a1, long a2)
static native boolean INTERNALgoalIsDecidedUnsat(long a0, long a1)
static long mkFpaRne(long a0)
static void optimizeSetParams(long a0, long a1, long a2)
static native void INTERNALrcfDel(long a0, long a1)
static String statsGetKey(long a0, long a1, int a2)
static native void INTERNALtoggleWarningMessages(boolean a0)
static void goalReset(long a0, long a1)
static native long INTERNALgetDeclAstParameter(long a0, long a1, int a2)
static void appendLog(String a0)
static long mkContext(long a0)
static boolean getNumeralUint64(long a0, long a1, LongPtr a2)
static native long INTERNALmkBvsgt(long a0, long a1, long a2)
static native String INTERNALastToString(long a0, long a1)
static native long INTERNALmkMap(long a0, long a1, int a2, long[] a3)
static native long INTERNALmkDiv(long a0, long a1, long a2)
static native long INTERNALmkFpaSub(long a0, long a1, long a2, long a3)
static native long INTERNALgetRelationColumn(long a0, long a1, int a2)
static native void INTERNALapplyResultDecRef(long a0, long a1)
static native long INTERNALmkFpaZero(long a0, long a1, boolean a2)
static long mkApp(long a0, long a1, int a2, long[] a3)
static long getTupleSortFieldDecl(long a0, long a1, int a2)
static void incRef(long a0, long a1)
static native long INTERNALmkDatatype(long a0, long a1, int a2, long[] a3)
static int check(long a0)
static native int INTERNALgetModelNumConstants(long a0, long a1)
static native boolean INTERNALisArrayValue(long a0, long a1, long a2, IntPtr a3)
static native void INTERNALrcfGetNumeratorDenominator(long a0, long a1, LongPtr a2, LongPtr a3)
static native boolean INTERNALfpaGetNumeralExponentInt64(long a0, long a1, LongPtr a2)
static long mkOr(long a0, int a1, long[] a2)
static native void INTERNALastVectorDecRef(long a0, long a1)
static int funcInterpGetNumEntries(long a0, long a1)
static native void INTERNALgoalReset(long a0, long a1)
static long rcfAdd(long a0, long a1, long a2)
static long solverGetParamDescrs(long a0, long a1)
static native long INTERNALmkBvsmod(long a0, long a1, long a2)
static native String INTERNALsolverToString(long a0, long a1)
static int optimizeAssertSoft(long a0, long a1, long a2, String a3, long a4)
static native String INTERNALgetDeclRationalParameter(long a0, long a1, int a2)
static void optimizePush(long a0, long a1)
static native void INTERNALsolverReset(long a0, long a1)
static native long INTERNALmkRepeat(long a0, int a1, long a2)
static native long INTERNALgetDeclFuncDeclParameter(long a0, long a1, int a2)
static native long INTERNALtacticTryFor(long a0, long a1, int a2)
static int getRelationArity(long a0, long a1)
static native int INTERNALgetSmtlibNumDecls(long a0)
static boolean goalIsDecidedUnsat(long a0, long a1)
static void resetMemory()
static native int INTERNALgetQuantifierNumBound(long a0, long a1)
static long funcEntryGetValue(long a0, long a1)
static native long INTERNALrcfMkE(long a0)
static native void INTERNALparamDescrsIncRef(long a0, long a1)
static native long INTERNALgetSmtlibSort(long a0, int a1)
static long mkSub(long a0, int a1, long[] a2)
static long tacticFailIf(long a0, long a1)
static native void INTERNALsolverPush(long a0, long a1)
static long mkExtRotateLeft(long a0, long a1, long a2)
static native long INTERNALmkFpaNan(long a0, long a1)
static long funcDeclToAst(long a0, long a1)
static native long INTERNALdatatypeUpdateField(long a0, long a1, long a2, long a3)
static long solverGetStatistics(long a0, long a1)
static native long INTERNALmkIntSort(long a0)
static long mkFpaIsPositive(long a0, long a1)
static long mkFpaSort16(long a0)
static native void INTERNALsolverDecRef(long a0, long a1)
static native long INTERNALmkBvand(long a0, long a1, long a2)
static long mkLabel(long a0, long a1, boolean a2, long a3)
static native long INTERNALgetQuantifierNoPatternAst(long a0, long a1, int a2)
static native void INTERNALfixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4)
static native int INTERNALoptimizeCheck(long a0, long a1)
static native int INTERNALgetBvSortSize(long a0, long a1)
static native long INTERNALmkBvredor(long a0, long a1)
static native long INTERNALoptimizeGetUpper(long a0, long a1, int a2)
static void fixedpointAddRule(long a0, long a1, long a2, long a3)
static native long INTERNALtacticParAndThen(long a0, long a1, long a2)
static long mkAstVector(long a0)
static long mkFpaSqrt(long a0, long a1, long a2)
static native int INTERNALgetSearchFailure(long a0)
static boolean statsIsUint(long a0, long a1, int a2)
static native long INTERNALmkFpaRtn(long a0)
static native int INTERNALcheckInterpolant(long a0, int a1, long[] a2, int[] a3, long[] a4, StringPtr a5, int a6, long[] a7)
static long mkBvlshr(long a0, long a1, long a2)
static native long INTERNALprobeLt(long a0, long a1, long a2)
static native void INTERNALmodelDecRef(long a0, long a1)
static boolean getNumeralSmall(long a0, long a1, LongPtr a2, LongPtr a3)
static native boolean INTERNALisAlgebraicNumber(long a0, long a1)
static native long INTERNALmkPattern(long a0, int a1, long[] a2)
static native boolean INTERNALstatsIsUint(long a0, long a1, int a2)
static long mkArraySort(long a0, long a1, long a2)
static void probeDecRef(long a0, long a1)
static long optimizeGetStatistics(long a0, long a1)
static long algebraicRoot(long a0, long a1, int a2)
static native boolean INTERNALalgebraicIsValue(long a0, long a1)
static native long INTERNALmkFpaIsSubnormal(long a0, long a1)
static native boolean INTERNALisEqFuncDecl(long a0, long a1, long a2)
static long getQuantifierBoundName(long a0, long a1, int a2)
static long getDenominator(long a0, long a1)
static long getDatatypeSortRecognizer(long a0, long a1, int a2)
static long getModelConstant(long a0, long a1, int a2)
static native long INTERNALmkBvugt(long a0, long a1, long a2)
static String probeGetDescr(long a0, String a1)
static long mkBvuge(long a0, long a1, long a2)
static long mkSolverForLogic(long a0, long a1)
static long getSmtlibDecl(long a0, int a1)
static native void INTERNALsolverIncRef(long a0, long a1)
static void solverReset(long a0, long a1)
static String getDeclRationalParameter(long a0, long a1, int a2)
static native int INTERNALfpaGetSbits(long a0, long a1)
static int modelGetNumSorts(long a0, long a1)
static native void INTERNALparamsDecRef(long a0, long a1)
static long mkFpaAdd(long a0, long a1, long a2, long a3)
static long getModelFuncDecl(long a0, long a1, int a2)
static long simplifyGetParamDescrs(long a0)
static void fixedpointAssert(long a0, long a1, long a2)
static long tacticApplyEx(long a0, long a1, long a2, long a3)
static native long INTERNALmkBvlshr(long a0, long a1, long a2)
static native void INTERNALdelLiterals(long a0, long a1)
static int openLog(String a0)
static native long INTERNALmkUninterpretedSort(long a0, long a1)
static long mkLe(long a0, long a1, long a2)
static long mkSetIntersect(long a0, int a1, long[] a2)
static long rcfMkInfinitesimal(long a0)
static native long INTERNALmkFpaFp(long a0, long a1, long a2, long a3)
static long mkFpaRem(long a0, long a1, long a2)
static long rcfPower(long a0, long a1, int a2)
static native void INTERNALgoalDecRef(long a0, long a1)
static long getRelevantLabels(long a0)
static int modelGetNumConsts(long a0, long a1)
static native int INTERNALgoalSize(long a0, long a1)
static native long INTERNALmkExistsConst(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6)
static long mkConcat(long a0, long a1, long a2)
static native boolean INTERNALalgebraicLe(long a0, long a1, long a2)
static long mkSelect(long a0, long a1, long a2)
static native void INTERNALdisableLiteral(long a0, long a1, int a2)
static long mkBvnand(long a0, long a1, long a2)
static long mkFpaRoundTowardNegative(long a0)
static native long INTERNALmkConstructorList(long a0, int a1, long[] a2)
static native long INTERNALmkFpaIsNan(long a0, long a1)
static native long INTERNALmkFpaToFpFloat(long a0, long a1, long a2, long a3)
static void fixedpointDecRef(long a0, long a1)
static long mkFpaToReal(long a0, long a1)
static int fixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
static native int INTERNALoptimizeMaximize(long a0, long a1, long a2)
static native long INTERNALmkBoolSort(long a0)
static int getNumScopes(long a0)
static double probeApply(long a0, long a1, long a2)
static int readInterpolationProblem(long a0, IntPtr a1, ObjArrayPtr a2, UIntArrayPtr a3, String a4, StringPtr a5, IntPtr a6, ObjArrayPtr a7)
static long getPattern(long a0, long a1, int a2)
static native void INTERNALtacticIncRef(long a0, long a1)
static native long INTERNALmkBvsge(long a0, long a1, long a2)
static String optimizeGetReasonUnknown(long a0, long a1)
static long probeEq(long a0, long a1, long a2)
static long getAsArrayFuncDecl(long a0, long a1)
static native void INTERNALgetVersion(IntPtr a0, IntPtr a1, IntPtr a2, IntPtr a3)
static native void INTERNALdelContext(long a0)
static native void INTERNALpop(long a0, int a1)
static native String INTERNALsortToString(long a0, long a1)
static long mkGe(long a0, long a1, long a2)
static native long INTERNALtacticWhen(long a0, long a1, long a2)
static long mkXor(long a0, long a1, long a2)
static native long INTERNALmkBound(long a0, int a1, long a2)
static native String INTERNALapplyResultToString(long a0, long a1)
static native int INTERNALfuncEntryGetNumArgs(long a0, long a1)
static native void INTERNALparamsSetSymbol(long a0, long a1, long a2, long a3)
static long getDomain(long a0, long a1, int a2)
static long mkBvslt(long a0, long a1, long a2)
static void enableTrace(String a0)
static native String INTERNALrcfNumToDecimalString(long a0, long a1, int a2)
static void goalAssert(long a0, long a1, long a2)
static native long INTERNALmkIte(long a0, long a1, long a2, long a3)
static boolean goalInconsistent(long a0, long a1)
static void getVersion(IntPtr a0, IntPtr a1, IntPtr a2, IntPtr a3)
static String interpolationProfile(long a0)
static long getGuessedLiterals(long a0)
static int getErrorCode(long a0)
static long mkFpaEq(long a0, long a1, long a2)
static long mkAdd(long a0, int a1, long[] a2)
static native String INTERNALfixedpointGetReasonUnknown(long a0, long a1)
static int getSmtlibNumFormulas(long a0)
static int getSearchFailure(long a0)
static native String INTERNALmodelToString(long a0, long a1)
static long mkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
static native void INTERNALastMapReset(long a0, long a1)
static native boolean INTERNALgetNumeralUint64(long a0, long a1, LongPtr a2)
static native void INTERNALparamsSetBool(long a0, long a1, long a2, boolean a3)
static void fixedpointSetParams(long a0, long a1, long a2)
static boolean astMapContains(long a0, long a1, long a2)
static long fixedpointGetAnswer(long a0, long a1)
static long optimizeGetModel(long a0, long a1)
static long toApp(long a0, long a1)
static native long INTERNALtacticFail(long a0)
static void astVectorIncRef(long a0, long a1)
static long probeOr(long a0, long a1, long a2)
static int getSortKind(long a0, long a1)
static String fpaGetNumeralExponentString(long a0, long a1)
static native long INTERNALmkLe(long a0, long a1, long a2)
static void optimizeAssert(long a0, long a1, long a2)
static native String INTERNALparamsToString(long a0, long a1)
static native long INTERNALmkFpaToFpSigned(long a0, long a1, long a2, long a3)
static native long INTERNALmodelGetConstDecl(long a0, long a1, int a2)
static native boolean INTERNALalgebraicEq(long a0, long a1, long a2)
static native boolean INTERNALrcfEq(long a0, long a1, long a2)
static native boolean INTERNALrcfGe(long a0, long a1, long a2)
static int optimizeMinimize(long a0, long a1, long a2)
static native int INTERNALoptimizeAssertSoft(long a0, long a1, long a2, String a3, long a4)
static native void INTERNALdisableTrace(String a0)
static native void INTERNALprobeIncRef(long a0, long a1)
static native long INTERNALparseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static void tacticIncRef(long a0, long a1)
static long mkExists(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7)
static native String INTERNALcontextToString(long a0)
static void goalIncRef(long a0, long a1)
static int getDeclNumParameters(long a0, long a1)
static native long INTERNALmkForall(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7)
static int getAppNumArgs(long a0, long a1)
static native void INTERNALfixedpointAssert(long a0, long a1, long a2)
static native void INTERNALoptimizeDecRef(long a0, long a1)
static native void INTERNALblockLiterals(long a0, long a1)
static native long INTERNALmkContextRc(long a0)
static int getDomainSize(long a0, long a1)
static int getModelNumFuncs(long a0, long a1)
static long getArraySortDomain(long a0, long a1)
static native long INTERNALmkConcat(long a0, long a1, long a2)
static native boolean INTERNALgetNumeralInt64(long a0, long a1, LongPtr a2)
static long probeNot(long a0, long a1)
static native String INTERNALfpaGetNumeralExponentString(long a0, long a1)
static void paramsValidate(long a0, long a1, long a2)
static long mkSignExt(long a0, int a1, long a2)
static native void INTERNALsetParamValue(long a0, String a1, String a2)
static native long INTERNALmkBvSort(long a0, int a1)
static native int INTERNALgetSortKind(long a0, long a1)
static native long INTERNALmkFpaGt(long a0, long a1, long a2)
static boolean algebraicLe(long a0, long a1, long a2)
static String getErrorMsg(int a0)
static long mkBvsmod(long a0, long a1, long a2)
static long mkBvaddNoUnderflow(long a0, long a1, long a2)
static long getLiteral(long a0, long a1, int a2)
static native long INTERNALmkConstructor(long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6)
static long mkSetComplement(long a0, long a1)
static native void INTERNALsolverSetParams(long a0, long a1, long a2)
static long solverGetProof(long a0, long a1)
static long mkInt(long a0, int a1, long a2)
static native long INTERNALmkTactic(long a0, String a1)
static native String INTERNALgetTacticName(long a0, int a1)
static native long INTERNALmkExtract(long a0, int a1, int a2, long a3)
static void paramsSetUint(long a0, long a1, long a2, int a3)
static native int INTERNALfixedpointQuery(long a0, long a1, long a2)
static long getQuantifierBoundSort(long a0, long a1, int a2)
static native void INTERNALparamsSetDouble(long a0, long a1, long a2, double a3)
static long fixedpointFromString(long a0, long a1, String a2)
static long probeConst(long a0, double a1)
static native String INTERNALastVectorToString(long a0, long a1)
static long mkSetAdd(long a0, long a1, long a2)
static native void INTERNALsetAstPrintMode(long a0, int a1)
static void solverIncRef(long a0, long a1)
static long mkFpaNumeralInt(long a0, int a1, long a2)
static long getLabelSymbol(long a0, long a1, int a2)
static long mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
static native long INTERNALsolverGetProof(long a0, long a1)
static long mkBvneg(long a0, long a1)
static native long INTERNALmkFpaEq(long a0, long a1, long a2)
static long mkInt64(long a0, long a1, long a2)
static boolean eval(long a0, long a1, long a2, LongPtr a3)
static native long INTERNALmkInt2real(long a0, long a1)
static native long INTERNALmkFpaSort64(long a0)
static native long INTERNALgetModelConstant(long a0, long a1, int a2)
static long mkFpaSort(long a0, int a1, int a2)
static long mkBvsdiv(long a0, long a1, long a2)
static long mkMap(long a0, long a1, int a2, long[] a3)
static int statsGetUintValue(long a0, long a1, int a2)
static native void INTERNALoptimizePop(long a0, long a1)
static native long INTERNALgoalFormula(long a0, long a1, int a2)
static String astVectorToString(long a0, long a1)
static int getNumTactics(long a0)
static long mkAtmost(long a0, int a1, long[] a2, int a3)
static native long INTERNALmkBvult(long a0, long a1, long a2)
static native int INTERNALgetDeclNumParameters(long a0, long a1)
static long substitute(long a0, long a1, int a2, long[] a3, long[] a4)
static long mkZeroExt(long a0, int a1, long a2)
static long mkBvnot(long a0, long a1)
static long mkFpaRna(long a0)
static native long INTERNALmkAtmost(long a0, int a1, long[] a2, int a3)
static long mkDistinct(long a0, int a1, long[] a2)
static void optimizeDecRef(long a0, long a1)
static native long INTERNALgetDeclSortParameter(long a0, long a1, int a2)
static long mkUnaryMinus(long a0, long a1)
static native long INTERNALmkFpaFma(long a0, long a1, long a2, long a3, long a4)
static native void INTERNALgoalAssert(long a0, long a1, long a2)
static native String INTERNALsolverGetReasonUnknown(long a0, long a1)
static boolean evalDecl(long a0, long a1, long a2, int a3, long[] a4, LongPtr a5)
static long mkSetDifference(long a0, long a1, long a2)
static double statsGetDoubleValue(long a0, long a1, int a2)
static native int INTERNALstatsGetUintValue(long a0, long a1, int a2)
static long mkBvsgt(long a0, long a1, long a2)
static long mkRealSort(long a0)
static native int INTERNALalgebraicEval(long a0, long a1, int a2, long[] a3)
static long mkSetDel(long a0, long a1, long a2)
static int goalPrecision(long a0, long a1)
static long mkRotateRight(long a0, int a1, long a2)
static native long INTERNALmodelGetFuncDecl(long a0, long a1, int a2)
static long toFuncDecl(long a0, long a1)
static long mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
static long mkStore(long a0, long a1, long a2, long a3)
static native int INTERNALgetAstHash(long a0, long a1)
static long mkForall(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7)
static long mkStringSymbol(long a0, String a1)
static native int INTERNALgetDomainSize(long a0, long a1)
static long fixedpointGetParamDescrs(long a0, long a1)
static String getNumeralDecimalString(long a0, long a1, int a2)
static long getQuantifierBody(long a0, long a1)
static native long INTERNALmkOr(long a0, int a1, long[] a2)
static long mkSolverFromTactic(long a0, long a1)
static long mkBvadd(long a0, long a1, long a2)
static void astMapIncRef(long a0, long a1)
static native long INTERNALmkBvsdiv(long a0, long a1, long a2)
static native void INTERNALsolverPop(long a0, long a1, int a2)
static long mkAstMap(long a0)
static native boolean INTERNALevalDecl(long a0, long a1, long a2, int a3, long[] a4, LongPtr a5)
static long fixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
static void delContext(long a0)
static native long INTERNALmkSelect(long a0, long a1, long a2)
static long getDeclSymbolParameter(long a0, long a1, int a2)
static long mkBvsle(long a0, long a1, long a2)
static String patternToString(long a0, long a1)
static native boolean INTERNALalgebraicIsPos(long a0, long a1)
static native long INTERNALmkStringSymbol(long a0, String a1)
static native long INTERNALmkFixedpoint(long a0)
static native long INTERNALmkFpaNumeralInt(long a0, int a1, long a2)
static native long INTERNALalgebraicMul(long a0, long a1, long a2)
static native int INTERNALgetArity(long a0, long a1)
static void paramsSetBool(long a0, long a1, long a2, boolean a3)
static void softCheckCancel(long a0)
static native long INTERNALmkPower(long a0, long a1, long a2)
static boolean rcfLe(long a0, long a1, long a2)
static native long INTERNALmkBvuge(long a0, long a1, long a2)
static int getAstId(long a0, long a1)
static native String INTERNALgetNumeralString(long a0, long a1)
static native String INTERNALgetSymbolString(long a0, long a1)
static native void INTERNALglobalParamResetAll()
static native int INTERNALgetBoolValue(long a0, long a1)
static native int INTERNALapplyResultGetNumSubgoals(long a0, long a1)
static native long INTERNALgetDatatypeSortConstructor(long a0, long a1, int a2)
static long mkFpaGeq(long a0, long a1, long a2)
static void statsIncRef(long a0, long a1)
static native long INTERNALmkPble(long a0, int a1, long[] a2, int[] a3, int a4)
static long mkFpaGt(long a0, long a1, long a2)
static native int INTERNALgetFuncDeclId(long a0, long a1)
static boolean isAsArray(long a0, long a1)
static native void INTERNALfixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4)
static long mkFpaToFpBv(long a0, long a1, long a2)
static native long INTERNALmkFpaIsPositive(long a0, long a1)
static native void INTERNALdecRef(long a0, long a1)
static native long INTERNALgetSortName(long a0, long a1)
static native int INTERNALgetAppNumArgs(long a0, long a1)
static String optimizeGetHelp(long a0, long a1)
static long updateTerm(long a0, long a1, int a2, long[] a3)
static boolean isWellSorted(long a0, long a1)
static void delModel(long a0, long a1)
static native long INTERNALgetPattern(long a0, long a1, int a2)
static void getArrayValue(long a0, long a1, long a2, int a3, long[] a4, long[] a5, LongPtr a6)
static native int INTERNALsolverCheck(long a0, long a1)
static long getContextAssignment(long a0)
static native long INTERNALmkFreshFuncDecl(long a0, String a1, int a2, long[] a3, long a4)
static void statsDecRef(long a0, long a1)
static boolean evalFuncDecl(long a0, long a1, long a2, LongPtr a3)
static long mkQuantifier(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8)
static native boolean INTERNALisQuantifierForall(long a0, long a1)
static native int INTERNALastVectorSize(long a0, long a1)
static native long INTERNALmkZeroExt(long a0, int a1, long a2)
static void disableTrace(String a0)
static native void INTERNALgetArrayValue(long a0, long a1, long a2, int a3, long[] a4, long[] a5, LongPtr a6)
static native void INTERNALastVectorSet(long a0, long a1, int a2, long a3)
static void setAstPrintMode(long a0, int a1)
static native int INTERNALmodelGetNumSorts(long a0, long a1)
static native void INTERNALsolverAssertAndTrack(long a0, long a1, long a2, long a3)
static long mkInterpolant(long a0, long a1)
static native long INTERNALapplyResultConvertModel(long a0, long a1, int a2, long a3)
static long algebraicRoots(long a0, long a1, int a2, long[] a3)
static native boolean INTERNALevalFuncDecl(long a0, long a1, long a2, LongPtr a3)
static int getQuantifierNumNoPatterns(long a0, long a1)
static long fixedpointGetRules(long a0, long a1)
static String contextToString(long a0)
static void queryConstructor(long a0, long a1, int a2, LongPtr a3, LongPtr a4, long[] a5)
static native long INTERNALfixedpointGetRules(long a0, long a1)
static native void INTERNALfixedpointUpdateRule(long a0, long a1, long a2, long a3)
static boolean getNumeralInt(long a0, long a1, IntPtr a2)
static native void INTERNALcloseLog()
static native long INTERNALmkBv2int(long a0, long a1, boolean a2)
static boolean rcfGe(long a0, long a1, long a2)
static native long INTERNALmkFpaInf(long a0, long a1, boolean a2)
static long goalTranslate(long a0, long a1, long a2)
static native long INTERNALprobeAnd(long a0, long a1, long a2)
static native long INTERNALgetContextAssignment(long a0)
static native int INTERNALgetQuantifierNumPatterns(long a0, long a1)
static native long INTERNALtacticCond(long a0, long a1, long a2, long a3)
static native boolean INTERNALgoalIsDecidedSat(long a0, long a1)
static native long INTERNALmkBvmulNoUnderflow(long a0, long a1, long a2)
static native void INTERNALglobalParamSet(String a0, String a1)
static native long INTERNALmkSolver(long a0)
static native long INTERNALgetInterpolant(long a0, long a1, long a2, long a3)
static long astVectorTranslate(long a0, long a1, long a2)
static native long INTERNALmkFpaRoundNearestTiesToEven(long a0)
static long mkTupleSort(long a0, long a1, int a2, long[] a3, long[] a4, LongPtr a5, long[] a6)
static long mkDiv(long a0, long a1, long a2)
static long goalFormula(long a0, long a1, int a2)
static native void INTERNALsoftCheckCancel(long a0)
static int checkAndGetModel(long a0, LongPtr a1)
static native long INTERNALgetAsArrayFuncDecl(long a0, long a1)
static native long INTERNALrcfSub(long a0, long a1, long a2)
static native void INTERNALparamsValidate(long a0, long a1, long a2)
static long mkQuantifierConst(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7)
static long mkIte(long a0, long a1, long a2, long a3)
static native long INTERNALprobeOr(long a0, long a1, long a2)
static void funcInterpIncRef(long a0, long a1)
static native int INTERNALcomputeInterpolant(long a0, long a1, long a2, LongPtr a3, LongPtr a4)
static long mkFpaToSbv(long a0, long a1, long a2, int a3)
static void fixedpointRegisterRelation(long a0, long a1, long a2)
static String tacticGetDescr(long a0, String a1)
static native void INTERNALmkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
static int getPatternNumTerms(long a0, long a1)
static long tacticFailIfNotDecided(long a0)
static native long INTERNALmkBvsdivNoOverflow(long a0, long a1, long a2)
static native String INTERNALstatsGetKey(long a0, long a1, int a2)
static native int INTERNALgetSymbolInt(long a0, long a1)
static native long INTERNALmkBvaddNoUnderflow(long a0, long a1, long a2)
static native long INTERNALmkParams(long a0)
static String optimizeToString(long a0, long a1)
static native long INTERNALmkExtRotateRight(long a0, long a1, long a2)
static native long INTERNALmkForallConst(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6)
static native long INTERNALtacticAndThen(long a0, long a1, long a2)
static native long INTERNALmkEnumerationSort(long a0, long a1, int a2, long[] a3, long[] a4, long[] a5)
static boolean modelHasInterp(long a0, long a1, long a2)
static long getSortName(long a0, long a1)
static native long INTERNALalgebraicRoot(long a0, long a1, int a2)
static native long INTERNALupdateTerm(long a0, long a1, int a2, long[] a3)
static long mkSimpleSolver(long a0)
static native long INTERNALmkQuantifierConstEx(long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long a11)
static native long INTERNALsimplifyEx(long a0, long a1, long a2)
static long getQuantifierNoPatternAst(long a0, long a1, int a2)
static native int INTERNALgoalPrecision(long a0, long a1)
static native String INTERNALstatsToString(long a0, long a1)
static native long INTERNALmkFpaIsInfinite(long a0, long a1)
static boolean rcfNeq(long a0, long a1, long a2)
static String funcDeclToString(long a0, long a1)
static void probeIncRef(long a0, long a1)
static long mkSetMember(long a0, long a1, long a2)
static void funcEntryDecRef(long a0, long a1)
static String getNumeralString(long a0, long a1)
static native long INTERNALsolverGetStatistics(long a0, long a1)
static int computeInterpolant(long a0, long a1, long a2, LongPtr a3, LongPtr a4)
static native long INTERNALprobeGe(long a0, long a1, long a2)
static native void INTERNALfixedpointPush(long a0, long a1)
static long mkFpaSortDouble(long a0)
static int optimizeMaximize(long a0, long a1, long a2)
static long getDatatypeSortConstructor(long a0, long a1, int a2)
static native void INTERNALparamsIncRef(long a0, long a1)
static long mkFpaSort64(long a0)
static native long INTERNALmkConstArray(long a0, long a1, long a2)
static native String INTERNALinterpolationProfile(long a0)
static long rcfMul(long a0, long a1, long a2)
static int rcfMkRoots(long a0, int a1, long[] a2, long[] a3)
static long mkFreshFuncDecl(long a0, String a1, int a2, long[] a3, long a4)
static native long INTERNALmkFpaNumeralDouble(long a0, double a1, long a2)
static native void INTERNALparamsSetUint(long a0, long a1, long a2, int a3)
static native boolean INTERNALastMapContains(long a0, long a1, long a2)
static native int INTERNALalgebraicSign(long a0, long a1)
static native long INTERNALrcfMkSmallInt(long a0, int a1)
static native long INTERNALmkFullSet(long a0, long a1)
static native long INTERNALfixedpointGetAssertions(long a0, long a1)
static void astMapReset(long a0, long a1)
static native long INTERNALgetSmtlibDecl(long a0, int a1)
static native void INTERNALenableTrace(String a0)
static boolean isNumeralAst(long a0, long a1)
static native long INTERNALsubstituteVars(long a0, long a1, int a2, long[] a3)
static native long INTERNALmkFpaNeg(long a0, long a1)
static native long INTERNALmkFpaSortDouble(long a0)
static native long INTERNALmkConst(long a0, long a1, long a2)
static boolean algebraicIsValue(long a0, long a1)
static native void INTERNALfixedpointAddCover(long a0, long a1, int a2, long a3, long a4)
static native boolean INTERNALrcfGt(long a0, long a1, long a2)
static long tacticParOr(long a0, int a1, long[] a2)
static long tacticSkip(long a0)
static int getSmtlibNumDecls(long a0)
static native long INTERNALtacticFailIfNotDecided(long a0)
static native long INTERNALmkSetUnion(long a0, int a1, long[] a2)
static int solverGetNumScopes(long a0, long a1)
static long mkBvurem(long a0, long a1, long a2)
static native String INTERNALgetSmtlibError(long a0)
static long mkSetSubset(long a0, long a1, long a2)
static long mkImplies(long a0, long a1, long a2)
static long funcEntryGetArg(long a0, long a1, int a2)
static int getIndexValue(long a0, long a1)
static int algebraicSign(long a0, long a1)
static native boolean INTERNALmodelEval(long a0, long a1, long a2, boolean a3, LongPtr a4)
static native long INTERNALmkTupleSort(long a0, long a1, int a2, long[] a3, long[] a4, LongPtr a5, long[] a6)
static int getTupleSortNumFields(long a0, long a1)
static long probeGt(long a0, long a1, long a2)
static long fixedpointFromFile(long a0, long a1, String a2)
static long mkFpaAbs(long a0, long a1)
static long mkFpaIsNan(long a0, long a1)
static boolean fpaGetNumeralExponentInt64(long a0, long a1, LongPtr a2)
static native void INTERNALstatsIncRef(long a0, long a1)
static native long INTERNALastMapKeys(long a0, long a1)
static native long INTERNALrcfMkInfinitesimal(long a0)
static long getSmtlibAssumption(long a0, int a1)
static String rcfNumToString(long a0, long a1, boolean a2, boolean a3)
static native long INTERNALparamDescrsGetName(long a0, long a1, int a2)
static native long INTERNALmkBvsle(long a0, long a1, long a2)
static native void INTERNALpush(long a0)
static native long INTERNALgetAlgebraicNumberUpper(long a0, long a1, int a2)
static int astVectorSize(long a0, long a1)
static native long INTERNALmkSetDel(long a0, long a1, long a2)
static native void INTERNALdelConfig(long a0)
static native String INTERNALsolverGetHelp(long a0, long a1)
static long getModelFuncEntryValue(long a0, long a1, int a2, int a3)
static native long INTERNALprobeNot(long a0, long a1)
static native long INTERNALpolynomialSubresultants(long a0, long a1, long a2, long a3)
static long rcfNeg(long a0, long a1)
static int checkAssumptions(long a0, int a1, long[] a2, LongPtr a3, LongPtr a4, IntPtr a5, long[] a6)
static native String INTERNALfixedpointToString(long a0, long a1, int a2, long[] a3)
static long mkFpaSortSingle(long a0)
static int funcInterpGetArity(long a0, long a1)
static long mkEq(long a0, long a1, long a2)
static native int INTERNALgoalDepth(long a0, long a1)
static boolean modelEval(long a0, long a1, long a2, boolean a3, LongPtr a4)
static native long INTERNALgetAlgebraicNumberLower(long a0, long a1, int a2)
static int getDeclKind(long a0, long a1)
static native long INTERNALapplyResultGetSubgoal(long a0, long a1, int a2)
static String applyResultToString(long a0, long a1)
static native void INTERNALastVectorPush(long a0, long a1, long a2)
static long mkRem(long a0, long a1, long a2)
static long rcfMkPi(long a0)
static native long INTERNALtacticRepeat(long a0, long a1, int a2)
static int goalNumExprs(long a0, long a1)
static int getArity(long a0, long a1)
static long patternToAst(long a0, long a1)
static boolean rcfLt(long a0, long a1, long a2)
static String paramDescrsToString(long a0, long a1)
static long getAlgebraicNumberLower(long a0, long a1, int a2)
static long mkExtRotateRight(long a0, long a1, long a2)
static String fixedpointToString(long a0, long a1, int a2, long[] a3)
static void fixedpointIncRef(long a0, long a1)
static native int INTERNALcheckAssumptions(long a0, int a1, long[] a2, LongPtr a3, LongPtr a4, IntPtr a5, long[] a6)
static native long INTERNALgetDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3)
static native long INTERNALsolverGetParamDescrs(long a0, long a1)
static native long INTERNALmkFpaRtz(long a0)
static native long INTERNALmkNumeral(long a0, String a1, long a2)
static long mkFpaMul(long a0, long a1, long a2, long a3)
static native long INTERNALmkSetSort(long a0, long a1)
static long tacticGetParamDescrs(long a0, long a1)
static native void INTERNALgoalIncRef(long a0, long a1)
static boolean algebraicGt(long a0, long a1, long a2)
static native boolean INTERNALisApp(long a0, long a1)
static native long INTERNALmkFpaLeq(long a0, long a1, long a2)
static native long INTERNALmkContext(long a0)
static void solverPush(long a0, long a1)
static int getBvSortSize(long a0, long a1)
static native String INTERNALgetErrorMsgEx(long a0, int a1)
static native int INTERNALgetPatternNumTerms(long a0, long a1)
static native double INTERNALprobeApply(long a0, long a1, long a2)
static long polynomialSubresultants(long a0, long a1, long a2, long a3)
static native int INTERNALgetDeclKind(long a0, long a1)
static native long INTERNALmkFpaRoundTowardPositive(long a0)
static native String INTERNALpatternToString(long a0, long a1)
static long mkInt2bv(long a0, int a1, long a2)
static void solverAssert(long a0, long a1, long a2)
static native long INTERNALprobeGt(long a0, long a1, long a2)
static native long INTERNALmkFpaRoundToIntegral(long a0, long a1, long a2)
static long getDeclAstParameter(long a0, long a1, int a2)
static void astMapInsert(long a0, long a1, long a2, long a3)
static native long INTERNALfixedpointGetAnswer(long a0, long a1)
static native long INTERNALmkFpaMax(long a0, long a1, long a2)
static native long INTERNALsolverGetUnsatCore(long a0, long a1)
static boolean algebraicLt(long a0, long a1, long a2)
static native long INTERNALrcfInv(long a0, long a1)
static native long INTERNALmkSolverFromTactic(long a0, long a1)
static long mkFpaRtz(long a0)
static native long INTERNALmkIsInt(long a0, long a1)
static long astMapKeys(long a0, long a1)
static long mkBvand(long a0, long a1, long a2)
static long funcInterpGetEntry(long a0, long a1, int a2)
static int goalDepth(long a0, long a1)
static void blockLiterals(long a0, long a1)
static long mkRepeat(long a0, int a1, long a2)
static native long INTERNALmkBvudiv(long a0, long a1, long a2)
static int getQuantifierNumBound(long a0, long a1)
static long mkIntSort(long a0)
static native long INTERNALmkInterpolant(long a0, long a1)
static native long INTERNALmkSub(long a0, int a1, long[] a2)
static native int INTERNALgoalNumExprs(long a0, long a1)
static String solverGetHelp(long a0, long a1)
static String fpaGetNumeralSignificandString(long a0, long a1)
static native long INTERNALmkFpaNumeralInt64Uint64(long a0, boolean a1, long a2, long a3, long a4)
static native void INTERNALtacticDecRef(long a0, long a1)
static void mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
static native long INTERNALmkXor(long a0, long a1, long a2)
static int getSymbolInt(long a0, long a1)
static long getRelationColumn(long a0, long a1, int a2)
static long mkFpaRoundingModeSort(long a0)
static String solverToString(long a0, long a1)
static long mkInjectiveFunction(long a0, long a1, int a2, long[] a3, long a4)
static native long INTERNALmkTrue(long a0)
static native int INTERNALgetErrorCode(long a0)
static long mkConstructorList(long a0, int a1, long[] a2)
static int getQuantifierWeight(long a0, long a1)
static native long INTERNALsubstitute(long a0, long a1, int a2, long[] a3, long[] a4)
static long mkPattern(long a0, int a1, long[] a2)
static long mkFpaRoundToIntegral(long a0, long a1, long a2)
static native long INTERNALmkReal2int(long a0, long a1)
static boolean algebraicIsNeg(long a0, long a1)
static String benchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7)
static long algebraicSub(long a0, long a1, long a2)
static native long INTERNALgetLiteral(long a0, long a1, int a2)
static long rcfSub(long a0, long a1, long a2)
static native long INTERNALmkFpaSort16(long a0)
static native long INTERNALmkBvurem(long a0, long a1, long a2)
static native void setInternalErrorHandler(long ctx)
static void fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4)
static native long INTERNALmkOptimize(long a0)
static native int INTERNALsolverCheckAssumptions(long a0, long a1, int a2, long[] a3)
static long mkFpaNumeralFloat(long a0, float a1, long a2)
static native long INTERNALmkFpaGeq(long a0, long a1, long a2)
static long mkBvult(long a0, long a1, long a2)
static native long INTERNALappToAst(long a0, long a1)
static native boolean INTERNALalgebraicGt(long a0, long a1, long a2)
static native long INTERNALmkBvredand(long a0, long a1)
static native long INTERNALmkBvxnor(long a0, long a1, long a2)
static void setParamValue(long a0, String a1, String a2)
static void parseSmtlibString(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static native String INTERNALgetProbeName(long a0, int a1)
static int getSmtlibNumAssumptions(long a0)
static native long INTERNALrcfNeg(long a0, long a1)
static native boolean INTERNALalgebraicNeq(long a0, long a1, long a2)
static int solverCheckAssumptions(long a0, long a1, int a2, long[] a3)
static native String INTERNALgoalToString(long a0, long a1)
static native boolean INTERNALstatsIsDouble(long a0, long a1, int a2)
static long modelGetFuncDecl(long a0, long a1, int a2)
static int getDeclIntParameter(long a0, long a1, int a2)
static boolean algebraicGe(long a0, long a1, long a2)
static native long INTERNALmodelGetFuncInterp(long a0, long a1, long a2)
static native String INTERNALtacticGetDescr(long a0, String a1)
static void paramsIncRef(long a0, long a1)
static native long INTERNALgetRelevantLiterals(long a0)
static native long INTERNALtranslate(long a0, long a1, long a2)
static long mkAnd(long a0, int a1, long[] a2)
static native long INTERNALmkFpaRoundNearestTiesToAway(long a0)
static boolean isArrayValue(long a0, long a1, long a2, IntPtr a3)
static native long INTERNALmkSetDifference(long a0, long a1, long a2)
static String statisticsToString(long a0)
static long rcfMkSmallInt(long a0, int a1)
static native long INTERNALmkRotateLeft(long a0, int a1, long a2)
static long applyResultConvertModel(long a0, long a1, int a2, long a3)
static native long INTERNALmkFpaNumeralFloat(long a0, float a1, long a2)
static long mkLt(long a0, long a1, long a2)
static native int INTERNALfixedpointGetNumLevels(long a0, long a1, long a2)
static long rcfMkRational(long a0, String a1)
static int astMapSize(long a0, long a1)
static void fixedpointPop(long a0, long a1)
static native int INTERNALparamDescrsGetKind(long a0, long a1, long a2)
static native long INTERNALsortToAst(long a0, long a1)
static native int INTERNALcheck(long a0)
static native void INTERNALprobeDecRef(long a0, long a1)
static native long INTERNALalgebraicSub(long a0, long a1, long a2)
static long mkContextRc(long a0)
static native long INTERNALfixedpointGetParamDescrs(long a0, long a1)
static native long INTERNALgetAppArg(long a0, long a1, int a2)
static long rcfInv(long a0, long a1)
static native long INTERNALmkUnsignedInt(long a0, int a1, long a2)
static native long INTERNALmkFpaRoundingModeSort(long a0)
static long mkFpaRtp(long a0)
static native long INTERNALmkExtRotateLeft(long a0, long a1, long a2)
static int fpaGetSbits(long a0, long a1)
static int fixedpointGetNumLevels(long a0, long a1, long a2)
static native long INTERNALmkFpaRna(long a0)
static native int INTERNALgetTupleSortNumFields(long a0, long a1)
static native void INTERNALfixedpointIncRef(long a0, long a1)
static long simplifyEx(long a0, long a1, long a2)
static long mkFpaRoundTowardPositive(long a0)
static native int INTERNALgetNumLiterals(long a0, long a1)
static native int INTERNALgetRelationArity(long a0, long a1)
static long mkFpaIsSubnormal(long a0, long a1)
static long optimizeGetLower(long a0, long a1, int a2)
static long mkBvsub(long a0, long a1, long a2)
static long mkFpaToIeeeBv(long a0, long a1)
static long mkConstArray(long a0, long a1, long a2)
static native int INTERNALgetQuantifierNumNoPatterns(long a0, long a1)
static native long INTERNALmkArraySort(long a0, long a1, long a2)
static boolean getFiniteDomainSortSize(long a0, long a1, LongPtr a2)
static long mkUninterpretedSort(long a0, long a1)
static native long INTERNALrcfMul(long a0, long a1, long a2)
static String getErrorMsgEx(long a0, int a1)
static long mkInt2real(long a0, long a1)
static long mkConst(long a0, long a1, long a2)
static boolean statsIsDouble(long a0, long a1, int a2)
static native String INTERNALoptimizeGetReasonUnknown(long a0, long a1)
static long mkFpaInf(long a0, long a1, boolean a2)
static native long INTERNALgoalTranslate(long a0, long a1, long a2)
static native long INTERNALmkSolverForLogic(long a0, long a1)
static long mkBvsge(long a0, long a1, long a2)
static native long INTERNALastVectorTranslate(long a0, long a1, long a2)
static native void INTERNALparamDescrsDecRef(long a0, long a1)
static long modelGetSortUniverse(long a0, long a1, long a2)
static long modelGetConstDecl(long a0, long a1, int a2)
static void applyResultDecRef(long a0, long a1)
static native long INTERNALmkIff(long a0, long a1, long a2)
static void assertCnstr(long a0, long a1)
static native long INTERNALmkFpaToFpUnsigned(long a0, long a1, long a2, long a3)
static long mkFpaToFpFloat(long a0, long a1, long a2, long a3)
static long mkFpaRoundNearestTiesToAway(long a0)
static long tacticParAndThen(long a0, long a1, long a2)
static String getProbeName(long a0, int a1)
static native boolean INTERNALrcfNeq(long a0, long a1, long a2)
static native void INTERNALfinalizeMemory()
static native long INTERNALgetModelFuncDecl(long a0, long a1, int a2)
static native long INTERNALtacticGetParamDescrs(long a0, long a1)
static native long INTERNALgetQuantifierBoundSort(long a0, long a1, int a2)
static native long INTERNALtacticParOr(long a0, int a1, long[] a2)
static int algebraicEval(long a0, long a1, int a2, long[] a3)
static native long INTERNALmkFpaSort128(long a0)
static native long INTERNALmkMod(long a0, long a1, long a2)
static void modelDecRef(long a0, long a1)
static native void INTERNALastMapErase(long a0, long a1, long a2)
static native long INTERNALmkSetMember(long a0, long a1, long a2)
static long optimizeGetParamDescrs(long a0, long a1)
static native void INTERNALapplyResultIncRef(long a0, long a1)
static long getAlgebraicNumberUpper(long a0, long a1, int a2)
static String fixedpointGetHelp(long a0, long a1)
static void goalDecRef(long a0, long a1)
static long mkBvashr(long a0, long a1, long a2)
static native long INTERNALmkRem(long a0, long a1, long a2)
static long getNumerator(long a0, long a1)
static native void INTERNALastMapIncRef(long a0, long a1)
static native long INTERNALgetQuantifierPatternAst(long a0, long a1, int a2)
static native long INTERNALmkInt64(long a0, long a1, long a2)
static native long INTERNALmkRotateRight(long a0, int a1, long a2)
static void setError(long a0, int a1)
static native String INTERNALoptimizeGetHelp(long a0, long a1)
static long mkGt(long a0, long a1, long a2)
static native long INTERNALoptimizeGetLower(long a0, long a1, int a2)
static native long INTERNALmkSignExt(long a0, int a1, long a2)
static native long INTERNALfixedpointFromString(long a0, long a1, String a2)
static native int INTERNALfuncInterpGetArity(long a0, long a1)
static native int INTERNALgetSmtlibNumSorts(long a0)
static native int INTERNALgetSymbolKind(long a0, long a1)
static native void INTERNALoptimizeSetParams(long a0, long a1, long a2)
static long mkFullSet(long a0, long a1)
static native String INTERNALparamDescrsToString(long a0, long a1)
static long modelGetConstInterp(long a0, long a1, long a2)
static native long INTERNALmkInt2bv(long a0, int a1, long a2)
static native long INTERNALmkBvshl(long a0, long a1, long a2)
static native long INTERNALastMapFind(long a0, long a1, long a2)
static native void INTERNALappendLog(String a0)
static long mkPble(long a0, int a1, long[] a2, int[] a3, int a4)
static int getSymbolKind(long a0, long a1)
static native long INTERNALalgebraicPower(long a0, long a1, int a2)
static native int INTERNALgetModelFuncNumEntries(long a0, long a1, int a2)
static native int INTERNALgetDeclIntParameter(long a0, long a1, int a2)
static native boolean INTERNALmodelHasInterp(long a0, long a1, long a2)
static void fixedpointPush(long a0, long a1)
static void solverSetParams(long a0, long a1, long a2)
static native void INTERNALinterrupt(long a0)
static long getTupleSortMkDecl(long a0, long a1)
static long getDeclSortParameter(long a0, long a1, int a2)
static String goalToString(long a0, long a1)
static native long INTERNALmkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
static void pop(long a0, int a1)
static long probeLe(long a0, long a1, long a2)
static native void INTERNALincRef(long a0, long a1)
static void solverAssertAndTrack(long a0, long a1, long a2, long a3)
static native boolean INTERNALfpaGetNumeralSign(long a0, long a1, IntPtr a2)
static long mkSetSort(long a0, long a1)
static long algebraicAdd(long a0, long a1, long a2)
static native boolean INTERNALgetNumeralInt(long a0, long a1, IntPtr a2)
static native long INTERNALmkStore(long a0, long a1, long a2, long a3)
static long mkFpaIsInfinite(long a0, long a1)
static native long INTERNALmkFpaIsZero(long a0, long a1)
static long astMapFind(long a0, long a1, long a2)
static int getAstHash(long a0, long a1)
static native long INTERNALoptimizeGetParamDescrs(long a0, long a1)
static native long INTERNALmkBvnot(long a0, long a1)
static native String INTERNALfuncDeclToString(long a0, long a1)
static native long INTERNALmkInterpolationContext(long a0)
static native int INTERNALgetNumScopes(long a0)
static native int INTERNALfpaGetEbits(long a0, long a1)
static native long INTERNALmkFpaLt(long a0, long a1, long a2)
static native long INTERNALalgebraicRoots(long a0, long a1, int a2, long[] a3)
static long mkInterpolationContext(long a0)
static long parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static long mkIntSymbol(long a0, int a1)
static native long INTERNALmkSetAdd(long a0, long a1, long a2)
static long tacticApply(long a0, long a1, long a2)
static void tacticDecRef(long a0, long a1)
static native void INTERNALparseSmtlibFile(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static long mkBvmulNoUnderflow(long a0, long a1, long a2)
static native long INTERNALmkBvmul(long a0, long a1, long a2)
static void astVectorSet(long a0, long a1, int a2, long a3)
static long mkRotateLeft(long a0, int a1, long a2)
static String simplifyGetHelp(long a0)
static long mkFpaNumeralInt64Uint64(long a0, boolean a1, long a2, long a3, long a4)
static native void INTERNALastMapInsert(long a0, long a1, long a2, long a3)
static native long INTERNALsimplify(long a0, long a1)
static boolean algebraicIsPos(long a0, long a1)
static long mkQuantifierConstEx(long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long a11)
static boolean isApp(long a0, long a1)
static native int INTERNALgetAstKind(long a0, long a1)
static void globalParamSet(String a0, String a1)
static void finalizeMemory()
static String paramsToString(long a0, long a1)
static long mkFpaMin(long a0, long a1, long a2)
static native boolean INTERNALgetFiniteDomainSortSize(long a0, long a1, LongPtr a2)
static long mkBvredand(long a0, long a1)
static native long INTERNALmkFpaRoundTowardNegative(long a0)
static native boolean INTERNALeval(long a0, long a1, long a2, LongPtr a3)
static String statsToString(long a0, long a1)
static native boolean INTERNALalgebraicGe(long a0, long a1, long a2)
static long tacticFail(long a0)
static native long INTERNALmkEq(long a0, long a1, long a2)
static int paramDescrsSize(long a0, long a1)
static native long INTERNALrcfMkPi(long a0)
static long mkBvxor(long a0, long a1, long a2)
static native void INTERNALdelModel(long a0, long a1)
static native long INTERNALgetDeclSymbolParameter(long a0, long a1, int a2)
static native long INTERNALmkFpaToFpReal(long a0, long a1, long a2, long a3)
static boolean isEqSort(long a0, long a1, long a2)
static native long INTERNALrcfDiv(long a0, long a1, long a2)
static long tacticUsingParams(long a0, long a1, long a2)
static native void INTERNALfixedpointRegisterRelation(long a0, long a1, long a2)
static native long INTERNALmkFpaSqrt(long a0, long a1, long a2)
static long probeLt(long a0, long a1, long a2)
static long mkFpaIsNormal(long a0, long a1)
static long getAppArg(long a0, long a1, int a2)
static long mkBvudiv(long a0, long a1, long a2)
static native long INTERNALmkFreshConst(long a0, String a1, long a2)
static native long INTERNALmkSimpleSolver(long a0)
static long mkFpaNan(long a0, long a1)
static native boolean INTERNALisWellSorted(long a0, long a1)
static long probeGe(long a0, long a1, long a2)
static long fixedpointGetStatistics(long a0, long a1)
static long mkBvshl(long a0, long a1, long a2)
static native void INTERNALastVectorIncRef(long a0, long a1)
static void decRef(long a0, long a1)
static native long INTERNALalgebraicAdd(long a0, long a1, long a2)
static int getFuncDeclId(long a0, long a1)
static long astVectorGet(long a0, long a1, int a2)
static native long INTERNALmkFuncDecl(long a0, long a1, int a2, long[] a3, long a4)
static native long INTERNALmkBvsubNoOverflow(long a0, long a1, long a2)
static native int INTERNALgetSmtlibNumAssumptions(long a0)
static long mkFalse(long a0)
static long mkFpaRtn(long a0)
static long mkBvsrem(long a0, long a1, long a2)
static long getInterpolant(long a0, long a1, long a2, long a3)
static boolean goalIsDecidedSat(long a0, long a1)
static native long INTERNALmkEmptySet(long a0, long a1)
static long mkFixedpoint(long a0)
static native int INTERNALgetNumProbes(long a0)
static native long INTERNALmkAstMap(long a0)
static String getSmtlibError(long a0)
static long mkEmptySet(long a0, long a1)
static native long INTERNALmkReal(long a0, int a1, int a2)
static long mkFpaRoundNearestTiesToEven(long a0)
static void fixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4)
static void disableLiteral(long a0, long a1, int a2)
static long mkBvsdivNoOverflow(long a0, long a1, long a2)
static native int INTERNALfuncInterpGetNumEntries(long a0, long a1)
static int getAstKind(long a0, long a1)
static native long INTERNALmkConfig()
static void rcfDel(long a0, long a1)
static String getTacticName(long a0, int a1)
static void astMapDecRef(long a0, long a1)
static long tacticTryFor(long a0, long a1, int a2)
static native long INTERNALmkAnd(long a0, int a1, long[] a2)
static native long INTERNALgetTupleSortMkDecl(long a0, long a1)
static void writeInterpolationProblem(long a0, int a1, long[] a2, int[] a3, String a4, int a5, long[] a6)
static long mkParams(long a0)
static long mkArrayDefault(long a0, long a1)
static long mkBvnegNoOverflow(long a0, long a1)
static native long INTERNALmkFpaSortSingle(long a0)
static int getDatatypeSortNumConstructors(long a0, long a1)
static int getSortId(long a0, long a1)
static long mkBound(long a0, int a1, long a2)
static long mkUnsignedInt64(long a0, long a1, long a2)
static native long INTERNALprobeLe(long a0, long a1, long a2)
static void delConstructorList(long a0, long a1)
static long simplify(long a0, long a1)
static long mkTrue(long a0)
static native long INTERNALmkFpaAbs(long a0, long a1)
static long mkFiniteDomainSort(long a0, long a1, long a2)
static long mkFpaSort128(long a0)
static native long INTERNALmkFpaSort(long a0, int a1, int a2)
static native long INTERNALmkQuantifierConst(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7)
static long mkMul(long a0, int a1, long[] a2)
static long mkFpaToFpReal(long a0, long a1, long a2, long a3)
static native long INTERNALmkFpaToIeeeBv(long a0, long a1)
static String sortToString(long a0, long a1)
static long rcfDiv(long a0, long a1, long a2)
static native long INTERNALfixedpointFromFile(long a0, long a1, String a2)
static native void INTERNALfuncInterpIncRef(long a0, long a1)
static boolean isEqFuncDecl(long a0, long a1, long a2)
static long mkReal(long a0, int a1, int a2)
static native int INTERNALgetModelFuncEntryNumArgs(long a0, long a1, int a2, int a3)
static long sortToAst(long a0, long a1)
static int getModelFuncNumEntries(long a0, long a1, int a2)
static native long INTERNALgetNumerator(long a0, long a1)
static void fixedpointAddCover(long a0, long a1, int a2, long a3, long a4)
static long algebraicPower(long a0, long a1, int a2)
static native long INTERNALgetSmtlibAssumption(long a0, int a1)
static long tacticAndThen(long a0, long a1, long a2)
static long getAppDecl(long a0, long a1)
static native long INTERNALmodelGetConstInterp(long a0, long a1, long a2)
static native long INTERNALmkBvule(long a0, long a1, long a2)
static native void INTERNALmodelIncRef(long a0, long a1)
static native String INTERNALbenchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7)
static long mkQuantifierEx(long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long[] a11, long a12)
static boolean rcfEq(long a0, long a1, long a2)
static long mkFpaLt(long a0, long a1, long a2)
static native long INTERNALgetRange(long a0, long a1)
static void delLiterals(long a0, long a1)
static double getDeclDoubleParameter(long a0, long a1, int a2)
static native long INTERNALmkAstVector(long a0)
static long mkEnumerationSort(long a0, long a1, int a2, long[] a3, long[] a4, long[] a5)
static boolean fpaGetNumeralSignificandUint64(long a0, long a1, LongPtr a2)
static void modelIncRef(long a0, long a1)
static long mkBvxnor(long a0, long a1, long a2)
static native long INTERNALmkSetComplement(long a0, long a1)
static native long INTERNALmkBvadd(long a0, long a1, long a2)
static native long INTERNALtoFuncDecl(long a0, long a1)
static long solverGetModel(long a0, long a1)
static long mkFpaMax(long a0, long a1, long a2)
static long mkFpaSub(long a0, long a1, long a2, long a3)
static native void INTERNALsolverAssert(long a0, long a1, long a2)
static long mkSetUnion(long a0, int a1, long[] a2)
static native String INTERNALtacticGetHelp(long a0, long a1)
static native long INTERNALmkLt(long a0, long a1, long a2)
static native long INTERNALastVectorGet(long a0, long a1, int a2)
static boolean rcfGt(long a0, long a1, long a2)
static native long INTERNALtacticUsingParams(long a0, long a1, long a2)
static long mkPower(long a0, long a1, long a2)
static native boolean INTERNALalgebraicLt(long a0, long a1, long a2)
static native String INTERNALprobeGetDescr(long a0, String a1)
static native long INTERNALmkIntSymbol(long a0, int a1)
static native long INTERNALgetSort(long a0, long a1)
static long getModelFuncElse(long a0, long a1, int a2)
static int getModelNumConstants(long a0, long a1)
static native boolean INTERNALgoalInconsistent(long a0, long a1)
static int modelGetNumFuncs(long a0, long a1)
static native boolean INTERNALalgebraicIsZero(long a0, long a1)
static native long INTERNALmkBvnor(long a0, long a1, long a2)
static long mkFpaIsZero(long a0, long a1)
static long getRelevantLiterals(long a0)
static native long INTERNALrcfMkRational(long a0, String a1)
static native long INTERNALtacticSkip(long a0)
static native long INTERNALmkQuantifier(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8)
static native long INTERNALsimplifyGetParamDescrs(long a0)
static native long INTERNALmkDistinct(long a0, int a1, long[] a2)
static void delConstructor(long a0, long a1)
static long mkBvor(long a0, long a1, long a2)
static native long INTERNALmkListSort(long a0, long a1, long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8)
static long getSmtlibFormula(long a0, int a1)
static long mkBoolSort(long a0)
static native boolean INTERNALisEqSort(long a0, long a1, long a2)
static native int INTERNALgetSortId(long a0, long a1)
static native long INTERNALmkFpaAdd(long a0, long a1, long a2, long a3)
static long mkExistsConst(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6)
static native long INTERNALgetDeclName(long a0, long a1)
static native void INTERNALpersistAst(long a0, long a1, int a2)
static native boolean INTERNALgetNumeralRationalInt64(long a0, long a1, LongPtr a2, LongPtr a3)
static long mkBv2int(long a0, long a1, boolean a2)
static native int INTERNALgetIndexValue(long a0, long a1)
static native void INTERNALwriteInterpolationProblem(long a0, int a1, long[] a2, int[] a3, String a4, int a5, long[] a6)
static native long INTERNALmodelGetSortUniverse(long a0, long a1, long a2)
static long getSort(long a0, long a1)
static long mkListSort(long a0, long a1, long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8)
static native long INTERNALgetLabelSymbol(long a0, long a1, int a2)
static native long INTERNALmkInt(long a0, int a1, long a2)
static native long INTERNALpatternToAst(long a0, long a1)
static native void INTERNALfuncInterpDecRef(long a0, long a1)
static long substituteVars(long a0, long a1, int a2, long[] a3)
static native long INTERNALmkFiniteDomainSort(long a0, long a1, long a2)
static void astVectorPush(long a0, long a1, long a2)
static boolean globalParamGet(String a0, StringPtr a1)
static native double INTERNALstatsGetDoubleValue(long a0, long a1, int a2)
static native long INTERNALmkFpaRoundTowardZero(long a0)
static long mkFpaRoundTowardZero(long a0)
static long fixedpointGetAssertions(long a0, long a1)
static long solverGetAssertions(long a0, long a1)
static native long INTERNALgetQuantifierBoundName(long a0, long a1, int a2)
static native long INTERNALmkFpaRem(long a0, long a1, long a2)
static void astVectorResize(long a0, long a1, int a2)
static native long INTERNALmkBvnegNoOverflow(long a0, long a1)
static void astVectorDecRef(long a0, long a1)
static native long INTERNALmkBvor(long a0, long a1, long a2)
static native boolean INTERNALfpaGetNumeralSignificandUint64(long a0, long a1, LongPtr a2)
static native int INTERNALsolverGetNumScopes(long a0, long a1)
static native int INTERNALgetQuantifierWeight(long a0, long a1)
static native long INTERNALalgebraicDiv(long a0, long a1, long a2)
static native long INTERNALgetModelFuncEntryArg(long a0, long a1, int a2, int a3, int a4)
static native long INTERNALmkFpaDiv(long a0, long a1, long a2, long a3)
static native long INTERNALmkLabel(long a0, long a1, boolean a2, long a3)
static int goalSize(long a0, long a1)
static native void INTERNALsetError(long a0, int a1)
static native boolean INTERNALisNumeralAst(long a0, long a1)
static long solverGetUnsatCore(long a0, long a1)
static long probeAnd(long a0, long a1, long a2)
static native long INTERNALmkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
static native long INTERNALmkBvsrem(long a0, long a1, long a2)
static native int INTERNALastMapSize(long a0, long a1)
static native long INTERNALmkFpaToFpBv(long a0, long a1, long a2)
static long mkBvmul(long a0, long a1, long a2)
static long mkFpaSortQuadruple(long a0)
static int funcEntryGetNumArgs(long a0, long a1)
static long paramDescrsGetName(long a0, long a1, int a2)
static long datatypeUpdateField(long a0, long a1, long a2, long a3)
static native long INTERNALmkUnaryMinus(long a0, long a1)
static String modelToString(long a0, long a1)
static int optimizeCheck(long a0, long a1)
static long mkFpaNumeralDouble(long a0, double a1, long a2)
static native long INTERNALmkFpaRne(long a0)
static native long INTERNALmkFpaRtp(long a0)
static native void INTERNALparseSmtlibString(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static boolean getNumeralInt64(long a0, long a1, LongPtr a2)
static long getDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3)
static long applyResultGetSubgoal(long a0, long a1, int a2)
static long mkFpaFma(long a0, long a1, long a2, long a3, long a4)
static native long INTERNALfuncInterpGetElse(long a0, long a1)
static int solverCheck(long a0, long a1)
static native int INTERNALgetAstId(long a0, long a1)
static native int INTERNALparamDescrsSize(long a0, long a1)
static native void INTERNALfixedpointSetParams(long a0, long a1, long a2)
static native long INTERNALrcfAdd(long a0, long a1, long a2)
static native long INTERNALoptimizeGetModel(long a0, long a1)
static native long INTERNALmkBvneg(long a0, long a1)
static boolean isQuantifierForall(long a0, long a1)
static void optimizeIncRef(long a0, long a1)
static String rcfNumToDecimalString(long a0, long a1, int a2)
static String astToString(long a0, long a1)
static long mkReal2int(long a0, long a1)
static native long INTERNALgetTupleSortFieldDecl(long a0, long a1, int a2)
static long appToAst(long a0, long a1)
static long mkFpaSortHalf(long a0)
static long mkFpaToUbv(long a0, long a1, long a2, int a3)
static long tacticWhen(long a0, long a1, long a2)
static native long INTERNALmkFpaSort32(long a0)
static long mkNot(long a0, long a1)
static native long INTERNALmkImplies(long a0, long a1, long a2)
static void paramsDecRef(long a0, long a1)
static boolean isEqAst(long a0, long a1, long a2)
static native int INTERNALgetSmtlibNumFormulas(long a0)
static int fixedpointQuery(long a0, long a1, long a2)
static long mkBvSort(long a0, int a1)
static native long INTERNALmkExists(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7)
static native String INTERNALstatisticsToString(long a0)
static native String INTERNALrcfNumToString(long a0, long a1, boolean a2, boolean a3)
static long mkOptimize(long a0)
static long mkUnsignedInt(long a0, int a1, long a2)
static long mkFpaSort32(long a0)
static long getRange(long a0, long a1)
static native void INTERNALdelConstructorList(long a0, long a1)
static void solverPop(long a0, long a1, int a2)
static int getDeclParameterKind(long a0, long a1, int a2)
static long modelGetFuncInterp(long a0, long a1, long a2)
static native long INTERNALmkFpaMul(long a0, long a1, long a2, long a3)
static void rcfGetNumeratorDenominator(long a0, long a1, LongPtr a2, LongPtr a3)
static native long INTERNALtacticApply(long a0, long a1, long a2)
static void setLogic(long a0, String a1)
static native int INTERNALgetDeclParameterKind(long a0, long a1, int a2)
static void funcEntryIncRef(long a0, long a1)
static boolean fpaGetNumeralSign(long a0, long a1, IntPtr a2)
static native void INTERNALastVectorResize(long a0, long a1, int a2)
static native long INTERNALmkBvashr(long a0, long a1, long a2)
static native long INTERNALgetModelFuncElse(long a0, long a1, int a2)
static long mkIsInt(long a0, long a1)
static long mkFpaLeq(long a0, long a1, long a2)
static long parseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static native int INTERNALrcfMkRoots(long a0, int a1, long[] a2, long[] a3)
static native long INTERNALmkUnsignedInt64(long a0, long a1, long a2)
static native void INTERNALfuncEntryIncRef(long a0, long a1)
static native int INTERNALreadInterpolationProblem(long a0, IntPtr a1, ObjArrayPtr a2, UIntArrayPtr a3, String a4, StringPtr a5, IntPtr a6, ObjArrayPtr a7)
static native long INTERNALprobeConst(long a0, double a1)
static long translate(long a0, long a1, long a2)
static long mkFpaToFpIntReal(long a0, long a1, long a2, long a3, long a4)
static long mkBvsubNoOverflow(long a0, long a1, long a2)
static long mkIff(long a0, long a1, long a2)
static boolean isAlgebraicNumber(long a0, long a1)
static native long INTERNALmkGt(long a0, long a1, long a2)
static native int INTERNALopenLog(String a0)
static native void INTERNALsetLogic(long a0, String a1)
static native void INTERNALqueryConstructor(long a0, long a1, int a2, LongPtr a3, LongPtr a4, long[] a5)
static long mkConstructor(long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6)
static native long INTERNALmkGe(long a0, long a1, long a2)
static void paramDescrsIncRef(long a0, long a1)
static native long INTERNALmkFpaIsNormal(long a0, long a1)
static final Z3_error_code fromInt(int v)
static native void INTERNALfixedpointAddRule(long a0, long a1, long a2, long a3)
static int getImpliedEqualities(long a0, long a1, int a2, long[] a3, int[] a4)
static int checkInterpolant(long a0, int a1, long[] a2, int[] a3, long[] a4, StringPtr a5, int a6, long[] a7)
static native long INTERNALmkFpaSortQuadruple(long a0)
static void funcInterpDecRef(long a0, long a1)
static native long INTERNALgetAppDecl(long a0, long a1)
static long mkGoal(long a0, boolean a1, boolean a2, boolean a3)
static native long INTERNALmkQuantifierEx(long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long[] a11, long a12)
static String fixedpointGetReasonUnknown(long a0, long a1)
static native void INTERNALastMapDecRef(long a0, long a1)
static long getDeclName(long a0, long a1)
static native long INTERNALmkArrayDefault(long a0, long a1)
static native String INTERNALfixedpointGetHelp(long a0, long a1)
static long tacticCond(long a0, long a1, long a2, long a3)
static native long INTERNALfixedpointGetStatistics(long a0, long a1)
static native int INTERNALcheckAndGetModel(long a0, LongPtr a1)
static native long INTERNALtacticOrElse(long a0, long a1, long a2)
static long mkFpaZero(long a0, long a1, boolean a2)
static long mkBvnor(long a0, long a1, long a2)