Package com.microsoft.z3

Class Native

java.lang.Object

com.microsoft.z3.Native

public final class Native
extends Object

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	Native.IntPtr
static class	Native.LongPtr
static class	Native.ObjArrayPtr
static class	Native.StringPtr
static class	Native.UIntArrayPtr

Constructor Summary

Constructors

Constructor	Description
Native()

Method Summary

Modifier and Type	Method	Description
static void	addConstInterp(long a0, long a1, long a2, long a3)
static long	addFuncInterp(long a0, long a1, long a2, long a3)
static void	addRecDef(long a0, long a1, int a2, long[] a3, long a4)
static long	algebraicAdd(long a0, long a1, long a2)
static long	algebraicDiv(long a0, long a1, long a2)
static boolean	algebraicEq(long a0, long a1, long a2)
static int	algebraicEval(long a0, long a1, int a2, long[] a3)
static boolean	algebraicGe(long a0, long a1, long a2)
static int	algebraicGetI(long a0, long a1)
static long	algebraicGetPoly(long a0, long a1)
static boolean	algebraicGt(long a0, long a1, long a2)
static boolean	algebraicIsNeg(long a0, long a1)
static boolean	algebraicIsPos(long a0, long a1)
static boolean	algebraicIsValue(long a0, long a1)
static boolean	algebraicIsZero(long a0, long a1)
static boolean	algebraicLe(long a0, long a1, long a2)
static boolean	algebraicLt(long a0, long a1, long a2)
static long	algebraicMul(long a0, long a1, long a2)
static boolean	algebraicNeq(long a0, long a1, long a2)
static long	algebraicPower(long a0, long a1, int a2)
static long	algebraicRoot(long a0, long a1, int a2)
static long	algebraicRoots(long a0, long a1, int a2, long[] a3)
static int	algebraicSign(long a0, long a1)
static long	algebraicSub(long a0, long a1, long a2)
static void	appendLog(String a0)
static void	applyResultDecRef(long a0, long a1)
static int	applyResultGetNumSubgoals(long a0, long a1)
static long	applyResultGetSubgoal(long a0, long a1, int a2)
static void	applyResultIncRef(long a0, long a1)
static String	applyResultToString(long a0, long a1)
static long	appToAst(long a0, long a1)
static boolean	astMapContains(long a0, long a1, long a2)
static void	astMapDecRef(long a0, long a1)
static void	astMapErase(long a0, long a1, long a2)
static long	astMapFind(long a0, long a1, long a2)
static void	astMapIncRef(long a0, long a1)
static void	astMapInsert(long a0, long a1, long a2, long a3)
static long	astMapKeys(long a0, long a1)
static void	astMapReset(long a0, long a1)
static int	astMapSize(long a0, long a1)
static String	astMapToString(long a0, long a1)
static String	astToString(long a0, long a1)
static void	astVectorDecRef(long a0, long a1)
static long	astVectorGet(long a0, long a1, int a2)
static void	astVectorIncRef(long a0, long a1)
static void	astVectorPush(long a0, long a1, long a2)
static void	astVectorResize(long a0, long a1, int a2)
static void	astVectorSet(long a0, long a1, int a2, long a3)
static int	astVectorSize(long a0, long a1)
static String	astVectorToString(long a0, long a1)
static long	astVectorTranslate(long a0, long a1, long a2)
static String	benchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7)
static void	closeLog()
static long	datatypeUpdateField(long a0, long a1, long a2, long a3)
static void	decRef(long a0, long a1)
static void	delConfig(long a0)
static void	delConstructor(long a0, long a1)
static void	delConstructorList(long a0, long a1)
static void	delContext(long a0)
static void	disableTrace(String a0)
static void	enableTrace(String a0)
static String	evalSmtlib2String(long a0, String a1)
static void	finalizeMemory()
static void	fixedpointAddCover(long a0, long a1, int a2, long a3, long a4)
static void	fixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4)
static void	fixedpointAddInvariant(long a0, long a1, long a2, long a3)
static void	fixedpointAddRule(long a0, long a1, long a2, long a3)
static void	fixedpointAssert(long a0, long a1, long a2)
static void	fixedpointDecRef(long a0, long a1)
static long	fixedpointFromFile(long a0, long a1, String a2)
static long	fixedpointFromString(long a0, long a1, String a2)
static long	fixedpointGetAnswer(long a0, long a1)
static long	fixedpointGetAssertions(long a0, long a1)
static long	fixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
static long	fixedpointGetGroundSatAnswer(long a0, long a1)
static String	fixedpointGetHelp(long a0, long a1)
static int	fixedpointGetNumLevels(long a0, long a1, long a2)
static long	fixedpointGetParamDescrs(long a0, long a1)
static long	fixedpointGetReachable(long a0, long a1, long a2)
static String	fixedpointGetReasonUnknown(long a0, long a1)
static long	fixedpointGetRuleNamesAlongTrace(long a0, long a1)
static long	fixedpointGetRules(long a0, long a1)
static long	fixedpointGetRulesAlongTrace(long a0, long a1)
static long	fixedpointGetStatistics(long a0, long a1)
static void	fixedpointIncRef(long a0, long a1)
static int	fixedpointQuery(long a0, long a1, long a2)
static int	fixedpointQueryFromLvl(long a0, long a1, long a2, int a3)
static int	fixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
static void	fixedpointRegisterRelation(long a0, long a1, long a2)
static void	fixedpointSetParams(long a0, long a1, long a2)
static void	fixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4)
static String	fixedpointToString(long a0, long a1, int a2, long[] a3)
static void	fixedpointUpdateRule(long a0, long a1, long a2, long a3)
static int	fpaGetEbits(long a0, long a1)
static long	fpaGetNumeralExponentBv(long a0, long a1, boolean a2)
static boolean	fpaGetNumeralExponentInt64(long a0, long a1, Native.LongPtr a2, boolean a3)
static String	fpaGetNumeralExponentString(long a0, long a1, boolean a2)
static boolean	fpaGetNumeralSign(long a0, long a1, Native.IntPtr a2)
static long	fpaGetNumeralSignBv(long a0, long a1)
static long	fpaGetNumeralSignificandBv(long a0, long a1)
static String	fpaGetNumeralSignificandString(long a0, long a1)
static boolean	fpaGetNumeralSignificandUint64(long a0, long a1, Native.LongPtr a2)
static int	fpaGetSbits(long a0, long a1)
static boolean	fpaIsNumeralInf(long a0, long a1)
static boolean	fpaIsNumeralNan(long a0, long a1)
static boolean	fpaIsNumeralNegative(long a0, long a1)
static boolean	fpaIsNumeralNormal(long a0, long a1)
static boolean	fpaIsNumeralPositive(long a0, long a1)
static boolean	fpaIsNumeralSubnormal(long a0, long a1)
static boolean	fpaIsNumeralZero(long a0, long a1)
static long	funcDeclToAst(long a0, long a1)
static String	funcDeclToString(long a0, long a1)
static void	funcEntryDecRef(long a0, long a1)
static long	funcEntryGetArg(long a0, long a1, int a2)
static int	funcEntryGetNumArgs(long a0, long a1)
static long	funcEntryGetValue(long a0, long a1)
static void	funcEntryIncRef(long a0, long a1)
static void	funcInterpAddEntry(long a0, long a1, long a2, long a3)
static void	funcInterpDecRef(long a0, long a1)
static int	funcInterpGetArity(long a0, long a1)
static long	funcInterpGetElse(long a0, long a1)
static long	funcInterpGetEntry(long a0, long a1, int a2)
static int	funcInterpGetNumEntries(long a0, long a1)
static void	funcInterpIncRef(long a0, long a1)
static void	funcInterpSetElse(long a0, long a1, long a2)
static long	getAlgebraicNumberLower(long a0, long a1, int a2)
static long	getAlgebraicNumberUpper(long a0, long a1, int a2)
static long	getAppArg(long a0, long a1, int a2)
static long	getAppDecl(long a0, long a1)
static int	getAppNumArgs(long a0, long a1)
static int	getArity(long a0, long a1)
static long	getArraySortDomain(long a0, long a1)
static long	getArraySortDomainN(long a0, long a1, int a2)
static long	getArraySortRange(long a0, long a1)
static long	getAsArrayFuncDecl(long a0, long a1)
static int	getAstHash(long a0, long a1)
static int	getAstId(long a0, long a1)
static int	getAstKind(long a0, long a1)
static int	getBoolValue(long a0, long a1)
static int	getBvSortSize(long a0, long a1)
static long	getDatatypeSortConstructor(long a0, long a1, int a2)
static long	getDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3)
static int	getDatatypeSortNumConstructors(long a0, long a1)
static long	getDatatypeSortRecognizer(long a0, long a1, int a2)
static long	getDeclAstParameter(long a0, long a1, int a2)
static double	getDeclDoubleParameter(long a0, long a1, int a2)
static long	getDeclFuncDeclParameter(long a0, long a1, int a2)
static int	getDeclIntParameter(long a0, long a1, int a2)
static int	getDeclKind(long a0, long a1)
static long	getDeclName(long a0, long a1)
static int	getDeclNumParameters(long a0, long a1)
static int	getDeclParameterKind(long a0, long a1, int a2)
static String	getDeclRationalParameter(long a0, long a1, int a2)
static long	getDeclSortParameter(long a0, long a1, int a2)
static long	getDeclSymbolParameter(long a0, long a1, int a2)
static long	getDenominator(long a0, long a1)
static long	getDomain(long a0, long a1, int a2)
static int	getDomainSize(long a0, long a1)
static int	getErrorCode(long a0)
static String	getErrorMsg(long a0, int a1)
static long	getEstimatedAllocSize()
static boolean	getFiniteDomainSortSize(long a0, long a1, Native.LongPtr a2)
static String	getFullVersion()
static int	getFuncDeclId(long a0, long a1)
static int	getImpliedEqualities(long a0, long a1, int a2, long[] a3, int[] a4)
static int	getIndexValue(long a0, long a1)
static long	getLstring(long a0, long a1, Native.IntPtr a2)
static String	getNumeralBinaryString(long a0, long a1)
static String	getNumeralDecimalString(long a0, long a1, int a2)
static double	getNumeralDouble(long a0, long a1)
static boolean	getNumeralInt(long a0, long a1, Native.IntPtr a2)
static boolean	getNumeralInt64(long a0, long a1, Native.LongPtr a2)
static boolean	getNumeralRationalInt64(long a0, long a1, Native.LongPtr a2, Native.LongPtr a3)
static boolean	getNumeralSmall(long a0, long a1, Native.LongPtr a2, Native.LongPtr a3)
static String	getNumeralString(long a0, long a1)
static boolean	getNumeralUint(long a0, long a1, Native.IntPtr a2)
static boolean	getNumeralUint64(long a0, long a1, Native.LongPtr a2)
static long	getNumerator(long a0, long a1)
static int	getNumProbes(long a0)
static int	getNumTactics(long a0)
static long	getPattern(long a0, long a1, int a2)
static int	getPatternNumTerms(long a0, long a1)
static String	getProbeName(long a0, int a1)
static long	getQuantifierBody(long a0, long a1)
static long	getQuantifierBoundName(long a0, long a1, int a2)
static long	getQuantifierBoundSort(long a0, long a1, int a2)
static long	getQuantifierNoPatternAst(long a0, long a1, int a2)
static int	getQuantifierNumBound(long a0, long a1)
static int	getQuantifierNumNoPatterns(long a0, long a1)
static int	getQuantifierNumPatterns(long a0, long a1)
static long	getQuantifierPatternAst(long a0, long a1, int a2)
static int	getQuantifierWeight(long a0, long a1)
static long	getRange(long a0, long a1)
static int	getRelationArity(long a0, long a1)
static long	getRelationColumn(long a0, long a1, int a2)
static long	getReSortBasis(long a0, long a1)
static long	getSeqSortBasis(long a0, long a1)
static long	getSort(long a0, long a1)
static int	getSortId(long a0, long a1)
static int	getSortKind(long a0, long a1)
static long	getSortName(long a0, long a1)
static String	getString(long a0, long a1)
static void	getStringContents(long a0, long a1, int a2, int[] a3)
static int	getStringLength(long a0, long a1)
static int	getSymbolInt(long a0, long a1)
static int	getSymbolKind(long a0, long a1)
static String	getSymbolString(long a0, long a1)
static String	getTacticName(long a0, int a1)
static long	getTupleSortFieldDecl(long a0, long a1, int a2)
static long	getTupleSortMkDecl(long a0, long a1)
static int	getTupleSortNumFields(long a0, long a1)
static void	getVersion(Native.IntPtr a0, Native.IntPtr a1, Native.IntPtr a2, Native.IntPtr a3)
static boolean	globalParamGet(String a0, Native.StringPtr a1)
static void	globalParamResetAll()
static void	globalParamSet(String a0, String a1)
static void	goalAssert(long a0, long a1, long a2)
static long	goalConvertModel(long a0, long a1, long a2)
static void	goalDecRef(long a0, long a1)
static int	goalDepth(long a0, long a1)
static long	goalFormula(long a0, long a1, int a2)
static boolean	goalInconsistent(long a0, long a1)
static void	goalIncRef(long a0, long a1)
static boolean	goalIsDecidedSat(long a0, long a1)
static boolean	goalIsDecidedUnsat(long a0, long a1)
static int	goalNumExprs(long a0, long a1)
static int	goalPrecision(long a0, long a1)
static void	goalReset(long a0, long a1)
static int	goalSize(long a0, long a1)
static String	goalToDimacsString(long a0, long a1, boolean a2)
static String	goalToString(long a0, long a1)
static long	goalTranslate(long a0, long a1, long a2)
static void	incRef(long a0, long a1)
protected static void	INTERNALaddConstInterp(long a0, long a1, long a2, long a3)
protected static long	INTERNALaddFuncInterp(long a0, long a1, long a2, long a3)
protected static void	INTERNALaddRecDef(long a0, long a1, int a2, long[] a3, long a4)
protected static long	INTERNALalgebraicAdd(long a0, long a1, long a2)
protected static long	INTERNALalgebraicDiv(long a0, long a1, long a2)
protected static boolean	INTERNALalgebraicEq(long a0, long a1, long a2)
protected static int	INTERNALalgebraicEval(long a0, long a1, int a2, long[] a3)
protected static boolean	INTERNALalgebraicGe(long a0, long a1, long a2)
protected static int	INTERNALalgebraicGetI(long a0, long a1)
protected static long	INTERNALalgebraicGetPoly(long a0, long a1)
protected static boolean	INTERNALalgebraicGt(long a0, long a1, long a2)
protected static boolean	INTERNALalgebraicIsNeg(long a0, long a1)
protected static boolean	INTERNALalgebraicIsPos(long a0, long a1)
protected static boolean	INTERNALalgebraicIsValue(long a0, long a1)
protected static boolean	INTERNALalgebraicIsZero(long a0, long a1)
protected static boolean	INTERNALalgebraicLe(long a0, long a1, long a2)
protected static boolean	INTERNALalgebraicLt(long a0, long a1, long a2)
protected static long	INTERNALalgebraicMul(long a0, long a1, long a2)
protected static boolean	INTERNALalgebraicNeq(long a0, long a1, long a2)
protected static long	INTERNALalgebraicPower(long a0, long a1, int a2)
protected static long	INTERNALalgebraicRoot(long a0, long a1, int a2)
protected static long	INTERNALalgebraicRoots(long a0, long a1, int a2, long[] a3)
protected static int	INTERNALalgebraicSign(long a0, long a1)
protected static long	INTERNALalgebraicSub(long a0, long a1, long a2)
protected static void	INTERNALappendLog(String a0)
protected static void	INTERNALapplyResultDecRef(long a0, long a1)
protected static int	INTERNALapplyResultGetNumSubgoals(long a0, long a1)
protected static long	INTERNALapplyResultGetSubgoal(long a0, long a1, int a2)
protected static void	INTERNALapplyResultIncRef(long a0, long a1)
protected static String	INTERNALapplyResultToString(long a0, long a1)
protected static long	INTERNALappToAst(long a0, long a1)
protected static boolean	INTERNALastMapContains(long a0, long a1, long a2)
protected static void	INTERNALastMapDecRef(long a0, long a1)
protected static void	INTERNALastMapErase(long a0, long a1, long a2)
protected static long	INTERNALastMapFind(long a0, long a1, long a2)
protected static void	INTERNALastMapIncRef(long a0, long a1)
protected static void	INTERNALastMapInsert(long a0, long a1, long a2, long a3)
protected static long	INTERNALastMapKeys(long a0, long a1)
protected static void	INTERNALastMapReset(long a0, long a1)
protected static int	INTERNALastMapSize(long a0, long a1)
protected static String	INTERNALastMapToString(long a0, long a1)
protected static String	INTERNALastToString(long a0, long a1)
protected static void	INTERNALastVectorDecRef(long a0, long a1)
protected static long	INTERNALastVectorGet(long a0, long a1, int a2)
protected static void	INTERNALastVectorIncRef(long a0, long a1)
protected static void	INTERNALastVectorPush(long a0, long a1, long a2)
protected static void	INTERNALastVectorResize(long a0, long a1, int a2)
protected static void	INTERNALastVectorSet(long a0, long a1, int a2, long a3)
protected static int	INTERNALastVectorSize(long a0, long a1)
protected static String	INTERNALastVectorToString(long a0, long a1)
protected static long	INTERNALastVectorTranslate(long a0, long a1, long a2)
protected static String	INTERNALbenchmarkToSmtlibString(long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7)
protected static void	INTERNALcloseLog()
protected static long	INTERNALdatatypeUpdateField(long a0, long a1, long a2, long a3)
protected static void	INTERNALdecRef(long a0, long a1)
protected static void	INTERNALdelConfig(long a0)
protected static void	INTERNALdelConstructor(long a0, long a1)
protected static void	INTERNALdelConstructorList(long a0, long a1)
protected static void	INTERNALdelContext(long a0)
protected static void	INTERNALdisableTrace(String a0)
protected static void	INTERNALenableTrace(String a0)
protected static String	INTERNALevalSmtlib2String(long a0, String a1)
protected static void	INTERNALfinalizeMemory()
protected static void	INTERNALfixedpointAddCover(long a0, long a1, int a2, long a3, long a4)
protected static void	INTERNALfixedpointAddFact(long a0, long a1, long a2, int a3, int[] a4)
protected static void	INTERNALfixedpointAddInvariant(long a0, long a1, long a2, long a3)
protected static void	INTERNALfixedpointAddRule(long a0, long a1, long a2, long a3)
protected static void	INTERNALfixedpointAssert(long a0, long a1, long a2)
protected static void	INTERNALfixedpointDecRef(long a0, long a1)
protected static long	INTERNALfixedpointFromFile(long a0, long a1, String a2)
protected static long	INTERNALfixedpointFromString(long a0, long a1, String a2)
protected static long	INTERNALfixedpointGetAnswer(long a0, long a1)
protected static long	INTERNALfixedpointGetAssertions(long a0, long a1)
protected static long	INTERNALfixedpointGetCoverDelta(long a0, long a1, int a2, long a3)
protected static long	INTERNALfixedpointGetGroundSatAnswer(long a0, long a1)
protected static String	INTERNALfixedpointGetHelp(long a0, long a1)
protected static int	INTERNALfixedpointGetNumLevels(long a0, long a1, long a2)
protected static long	INTERNALfixedpointGetParamDescrs(long a0, long a1)
protected static long	INTERNALfixedpointGetReachable(long a0, long a1, long a2)
protected static String	INTERNALfixedpointGetReasonUnknown(long a0, long a1)
protected static long	INTERNALfixedpointGetRuleNamesAlongTrace(long a0, long a1)
protected static long	INTERNALfixedpointGetRules(long a0, long a1)
protected static long	INTERNALfixedpointGetRulesAlongTrace(long a0, long a1)
protected static long	INTERNALfixedpointGetStatistics(long a0, long a1)
protected static void	INTERNALfixedpointIncRef(long a0, long a1)
protected static int	INTERNALfixedpointQuery(long a0, long a1, long a2)
protected static int	INTERNALfixedpointQueryFromLvl(long a0, long a1, long a2, int a3)
protected static int	INTERNALfixedpointQueryRelations(long a0, long a1, int a2, long[] a3)
protected static void	INTERNALfixedpointRegisterRelation(long a0, long a1, long a2)
protected static void	INTERNALfixedpointSetParams(long a0, long a1, long a2)
protected static void	INTERNALfixedpointSetPredicateRepresentation(long a0, long a1, long a2, int a3, long[] a4)
protected static String	INTERNALfixedpointToString(long a0, long a1, int a2, long[] a3)
protected static void	INTERNALfixedpointUpdateRule(long a0, long a1, long a2, long a3)
protected static int	INTERNALfpaGetEbits(long a0, long a1)
protected static long	INTERNALfpaGetNumeralExponentBv(long a0, long a1, boolean a2)
protected static boolean	INTERNALfpaGetNumeralExponentInt64(long a0, long a1, Native.LongPtr a2, boolean a3)
protected static String	INTERNALfpaGetNumeralExponentString(long a0, long a1, boolean a2)
protected static boolean	INTERNALfpaGetNumeralSign(long a0, long a1, Native.IntPtr a2)
protected static long	INTERNALfpaGetNumeralSignBv(long a0, long a1)
protected static long	INTERNALfpaGetNumeralSignificandBv(long a0, long a1)
protected static String	INTERNALfpaGetNumeralSignificandString(long a0, long a1)
protected static boolean	INTERNALfpaGetNumeralSignificandUint64(long a0, long a1, Native.LongPtr a2)
protected static int	INTERNALfpaGetSbits(long a0, long a1)
protected static boolean	INTERNALfpaIsNumeralInf(long a0, long a1)
protected static boolean	INTERNALfpaIsNumeralNan(long a0, long a1)
protected static boolean	INTERNALfpaIsNumeralNegative(long a0, long a1)
protected static boolean	INTERNALfpaIsNumeralNormal(long a0, long a1)
protected static boolean	INTERNALfpaIsNumeralPositive(long a0, long a1)
protected static boolean	INTERNALfpaIsNumeralSubnormal(long a0, long a1)
protected static boolean	INTERNALfpaIsNumeralZero(long a0, long a1)
protected static long	INTERNALfuncDeclToAst(long a0, long a1)
protected static String	INTERNALfuncDeclToString(long a0, long a1)
protected static void	INTERNALfuncEntryDecRef(long a0, long a1)
protected static long	INTERNALfuncEntryGetArg(long a0, long a1, int a2)
protected static int	INTERNALfuncEntryGetNumArgs(long a0, long a1)
protected static long	INTERNALfuncEntryGetValue(long a0, long a1)
protected static void	INTERNALfuncEntryIncRef(long a0, long a1)
protected static void	INTERNALfuncInterpAddEntry(long a0, long a1, long a2, long a3)
protected static void	INTERNALfuncInterpDecRef(long a0, long a1)
protected static int	INTERNALfuncInterpGetArity(long a0, long a1)
protected static long	INTERNALfuncInterpGetElse(long a0, long a1)
protected static long	INTERNALfuncInterpGetEntry(long a0, long a1, int a2)
protected static int	INTERNALfuncInterpGetNumEntries(long a0, long a1)
protected static void	INTERNALfuncInterpIncRef(long a0, long a1)
protected static void	INTERNALfuncInterpSetElse(long a0, long a1, long a2)
protected static long	INTERNALgetAlgebraicNumberLower(long a0, long a1, int a2)
protected static long	INTERNALgetAlgebraicNumberUpper(long a0, long a1, int a2)
protected static long	INTERNALgetAppArg(long a0, long a1, int a2)
protected static long	INTERNALgetAppDecl(long a0, long a1)
protected static int	INTERNALgetAppNumArgs(long a0, long a1)
protected static int	INTERNALgetArity(long a0, long a1)
protected static long	INTERNALgetArraySortDomain(long a0, long a1)
protected static long	INTERNALgetArraySortDomainN(long a0, long a1, int a2)
protected static long	INTERNALgetArraySortRange(long a0, long a1)
protected static long	INTERNALgetAsArrayFuncDecl(long a0, long a1)
protected static int	INTERNALgetAstHash(long a0, long a1)
protected static int	INTERNALgetAstId(long a0, long a1)
protected static int	INTERNALgetAstKind(long a0, long a1)
protected static int	INTERNALgetBoolValue(long a0, long a1)
protected static int	INTERNALgetBvSortSize(long a0, long a1)
protected static long	INTERNALgetDatatypeSortConstructor(long a0, long a1, int a2)
protected static long	INTERNALgetDatatypeSortConstructorAccessor(long a0, long a1, int a2, int a3)
protected static int	INTERNALgetDatatypeSortNumConstructors(long a0, long a1)
protected static long	INTERNALgetDatatypeSortRecognizer(long a0, long a1, int a2)
protected static long	INTERNALgetDeclAstParameter(long a0, long a1, int a2)
protected static double	INTERNALgetDeclDoubleParameter(long a0, long a1, int a2)
protected static long	INTERNALgetDeclFuncDeclParameter(long a0, long a1, int a2)
protected static int	INTERNALgetDeclIntParameter(long a0, long a1, int a2)
protected static int	INTERNALgetDeclKind(long a0, long a1)
protected static long	INTERNALgetDeclName(long a0, long a1)
protected static int	INTERNALgetDeclNumParameters(long a0, long a1)
protected static int	INTERNALgetDeclParameterKind(long a0, long a1, int a2)
protected static String	INTERNALgetDeclRationalParameter(long a0, long a1, int a2)
protected static long	INTERNALgetDeclSortParameter(long a0, long a1, int a2)
protected static long	INTERNALgetDeclSymbolParameter(long a0, long a1, int a2)
protected static long	INTERNALgetDenominator(long a0, long a1)
protected static long	INTERNALgetDomain(long a0, long a1, int a2)
protected static int	INTERNALgetDomainSize(long a0, long a1)
protected static int	INTERNALgetErrorCode(long a0)
protected static String	INTERNALgetErrorMsg(long a0, int a1)
protected static long	INTERNALgetEstimatedAllocSize()
protected static boolean	INTERNALgetFiniteDomainSortSize(long a0, long a1, Native.LongPtr a2)
protected static String	INTERNALgetFullVersion()
protected static int	INTERNALgetFuncDeclId(long a0, long a1)
protected static int	INTERNALgetImpliedEqualities(long a0, long a1, int a2, long[] a3, int[] a4)
protected static int	INTERNALgetIndexValue(long a0, long a1)
protected static long	INTERNALgetLstring(long a0, long a1, Native.IntPtr a2)
protected static String	INTERNALgetNumeralBinaryString(long a0, long a1)
protected static String	INTERNALgetNumeralDecimalString(long a0, long a1, int a2)
protected static double	INTERNALgetNumeralDouble(long a0, long a1)
protected static boolean	INTERNALgetNumeralInt(long a0, long a1, Native.IntPtr a2)
protected static boolean	INTERNALgetNumeralInt64(long a0, long a1, Native.LongPtr a2)
protected static boolean	INTERNALgetNumeralRationalInt64(long a0, long a1, Native.LongPtr a2, Native.LongPtr a3)
protected static boolean	INTERNALgetNumeralSmall(long a0, long a1, Native.LongPtr a2, Native.LongPtr a3)
protected static String	INTERNALgetNumeralString(long a0, long a1)
protected static boolean	INTERNALgetNumeralUint(long a0, long a1, Native.IntPtr a2)
protected static boolean	INTERNALgetNumeralUint64(long a0, long a1, Native.LongPtr a2)
protected static long	INTERNALgetNumerator(long a0, long a1)
protected static int	INTERNALgetNumProbes(long a0)
protected static int	INTERNALgetNumTactics(long a0)
protected static long	INTERNALgetPattern(long a0, long a1, int a2)
protected static int	INTERNALgetPatternNumTerms(long a0, long a1)
protected static String	INTERNALgetProbeName(long a0, int a1)
protected static long	INTERNALgetQuantifierBody(long a0, long a1)
protected static long	INTERNALgetQuantifierBoundName(long a0, long a1, int a2)
protected static long	INTERNALgetQuantifierBoundSort(long a0, long a1, int a2)
protected static long	INTERNALgetQuantifierNoPatternAst(long a0, long a1, int a2)
protected static int	INTERNALgetQuantifierNumBound(long a0, long a1)
protected static int	INTERNALgetQuantifierNumNoPatterns(long a0, long a1)
protected static int	INTERNALgetQuantifierNumPatterns(long a0, long a1)
protected static long	INTERNALgetQuantifierPatternAst(long a0, long a1, int a2)
protected static int	INTERNALgetQuantifierWeight(long a0, long a1)
protected static long	INTERNALgetRange(long a0, long a1)
protected static int	INTERNALgetRelationArity(long a0, long a1)
protected static long	INTERNALgetRelationColumn(long a0, long a1, int a2)
protected static long	INTERNALgetReSortBasis(long a0, long a1)
protected static long	INTERNALgetSeqSortBasis(long a0, long a1)
protected static long	INTERNALgetSort(long a0, long a1)
protected static int	INTERNALgetSortId(long a0, long a1)
protected static int	INTERNALgetSortKind(long a0, long a1)
protected static long	INTERNALgetSortName(long a0, long a1)
protected static String	INTERNALgetString(long a0, long a1)
protected static void	INTERNALgetStringContents(long a0, long a1, int a2, int[] a3)
protected static int	INTERNALgetStringLength(long a0, long a1)
protected static int	INTERNALgetSymbolInt(long a0, long a1)
protected static int	INTERNALgetSymbolKind(long a0, long a1)
protected static String	INTERNALgetSymbolString(long a0, long a1)
protected static String	INTERNALgetTacticName(long a0, int a1)
protected static long	INTERNALgetTupleSortFieldDecl(long a0, long a1, int a2)
protected static long	INTERNALgetTupleSortMkDecl(long a0, long a1)
protected static int	INTERNALgetTupleSortNumFields(long a0, long a1)
protected static void	INTERNALgetVersion(Native.IntPtr a0, Native.IntPtr a1, Native.IntPtr a2, Native.IntPtr a3)
protected static boolean	INTERNALglobalParamGet(String a0, Native.StringPtr a1)
protected static void	INTERNALglobalParamResetAll()
protected static void	INTERNALglobalParamSet(String a0, String a1)
protected static void	INTERNALgoalAssert(long a0, long a1, long a2)
protected static long	INTERNALgoalConvertModel(long a0, long a1, long a2)
protected static void	INTERNALgoalDecRef(long a0, long a1)
protected static int	INTERNALgoalDepth(long a0, long a1)
protected static long	INTERNALgoalFormula(long a0, long a1, int a2)
protected static boolean	INTERNALgoalInconsistent(long a0, long a1)
protected static void	INTERNALgoalIncRef(long a0, long a1)
protected static boolean	INTERNALgoalIsDecidedSat(long a0, long a1)
protected static boolean	INTERNALgoalIsDecidedUnsat(long a0, long a1)
protected static int	INTERNALgoalNumExprs(long a0, long a1)
protected static int	INTERNALgoalPrecision(long a0, long a1)
protected static void	INTERNALgoalReset(long a0, long a1)
protected static int	INTERNALgoalSize(long a0, long a1)
protected static String	INTERNALgoalToDimacsString(long a0, long a1, boolean a2)
protected static String	INTERNALgoalToString(long a0, long a1)
protected static long	INTERNALgoalTranslate(long a0, long a1, long a2)
protected static void	INTERNALincRef(long a0, long a1)
protected static void	INTERNALinterrupt(long a0)
protected static boolean	INTERNALisAlgebraicNumber(long a0, long a1)
protected static boolean	INTERNALisApp(long a0, long a1)
protected static boolean	INTERNALisAsArray(long a0, long a1)
protected static boolean	INTERNALisCharSort(long a0, long a1)
protected static boolean	INTERNALisEqAst(long a0, long a1, long a2)
protected static boolean	INTERNALisEqFuncDecl(long a0, long a1, long a2)
protected static boolean	INTERNALisEqSort(long a0, long a1, long a2)
protected static boolean	INTERNALisLambda(long a0, long a1)
protected static boolean	INTERNALisNumeralAst(long a0, long a1)
protected static boolean	INTERNALisQuantifierExists(long a0, long a1)
protected static boolean	INTERNALisQuantifierForall(long a0, long a1)
protected static boolean	INTERNALisReSort(long a0, long a1)
protected static boolean	INTERNALisSeqSort(long a0, long a1)
protected static boolean	INTERNALisString(long a0, long a1)
protected static boolean	INTERNALisStringSort(long a0, long a1)
protected static boolean	INTERNALisWellSorted(long a0, long a1)
protected static long	INTERNALmkAdd(long a0, int a1, long[] a2)
protected static long	INTERNALmkAnd(long a0, int a1, long[] a2)
protected static long	INTERNALmkApp(long a0, long a1, int a2, long[] a3)
protected static long	INTERNALmkArrayDefault(long a0, long a1)
protected static long	INTERNALmkArrayExt(long a0, long a1, long a2)
protected static long	INTERNALmkArraySort(long a0, long a1, long a2)
protected static long	INTERNALmkArraySortN(long a0, int a1, long[] a2, long a3)
protected static long	INTERNALmkAsArray(long a0, long a1)
protected static long	INTERNALmkAstMap(long a0)
protected static long	INTERNALmkAstVector(long a0)
protected static long	INTERNALmkAtleast(long a0, int a1, long[] a2, int a3)
protected static long	INTERNALmkAtmost(long a0, int a1, long[] a2, int a3)
protected static long	INTERNALmkBoolSort(long a0)
protected static long	INTERNALmkBound(long a0, int a1, long a2)
protected static long	INTERNALmkBv2int(long a0, long a1, boolean a2)
protected static long	INTERNALmkBvadd(long a0, long a1, long a2)
protected static long	INTERNALmkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
protected static long	INTERNALmkBvaddNoUnderflow(long a0, long a1, long a2)
protected static long	INTERNALmkBvand(long a0, long a1, long a2)
protected static long	INTERNALmkBvashr(long a0, long a1, long a2)
protected static long	INTERNALmkBvlshr(long a0, long a1, long a2)
protected static long	INTERNALmkBvmul(long a0, long a1, long a2)
protected static long	INTERNALmkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
protected static long	INTERNALmkBvmulNoUnderflow(long a0, long a1, long a2)
protected static long	INTERNALmkBvnand(long a0, long a1, long a2)
protected static long	INTERNALmkBvneg(long a0, long a1)
protected static long	INTERNALmkBvnegNoOverflow(long a0, long a1)
protected static long	INTERNALmkBvnor(long a0, long a1, long a2)
protected static long	INTERNALmkBvnot(long a0, long a1)
protected static long	INTERNALmkBvNumeral(long a0, int a1, boolean[] a2)
protected static long	INTERNALmkBvor(long a0, long a1, long a2)
protected static long	INTERNALmkBvredand(long a0, long a1)
protected static long	INTERNALmkBvredor(long a0, long a1)
protected static long	INTERNALmkBvsdiv(long a0, long a1, long a2)
protected static long	INTERNALmkBvsdivNoOverflow(long a0, long a1, long a2)
protected static long	INTERNALmkBvsge(long a0, long a1, long a2)
protected static long	INTERNALmkBvsgt(long a0, long a1, long a2)
protected static long	INTERNALmkBvshl(long a0, long a1, long a2)
protected static long	INTERNALmkBvsle(long a0, long a1, long a2)
protected static long	INTERNALmkBvslt(long a0, long a1, long a2)
protected static long	INTERNALmkBvsmod(long a0, long a1, long a2)
protected static long	INTERNALmkBvSort(long a0, int a1)
protected static long	INTERNALmkBvsrem(long a0, long a1, long a2)
protected static long	INTERNALmkBvsub(long a0, long a1, long a2)
protected static long	INTERNALmkBvsubNoOverflow(long a0, long a1, long a2)
protected static long	INTERNALmkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
protected static long	INTERNALmkBvudiv(long a0, long a1, long a2)
protected static long	INTERNALmkBvuge(long a0, long a1, long a2)
protected static long	INTERNALmkBvugt(long a0, long a1, long a2)
protected static long	INTERNALmkBvule(long a0, long a1, long a2)
protected static long	INTERNALmkBvult(long a0, long a1, long a2)
protected static long	INTERNALmkBvurem(long a0, long a1, long a2)
protected static long	INTERNALmkBvxnor(long a0, long a1, long a2)
protected static long	INTERNALmkBvxor(long a0, long a1, long a2)
protected static long	INTERNALmkChar(long a0, int a1)
protected static long	INTERNALmkCharFromBv(long a0, long a1)
protected static long	INTERNALmkCharIsDigit(long a0, long a1)
protected static long	INTERNALmkCharLe(long a0, long a1, long a2)
protected static long	INTERNALmkCharSort(long a0)
protected static long	INTERNALmkCharToBv(long a0, long a1)
protected static long	INTERNALmkCharToInt(long a0, long a1)
protected static long	INTERNALmkConcat(long a0, long a1, long a2)
protected static long	INTERNALmkConfig()
protected static long	INTERNALmkConst(long a0, long a1, long a2)
protected static long	INTERNALmkConstArray(long a0, long a1, long a2)
protected static long	INTERNALmkConstructor(long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6)
protected static long	INTERNALmkConstructorList(long a0, int a1, long[] a2)
protected static long	INTERNALmkContext(long a0)
protected static long	INTERNALmkContextRc(long a0)
protected static long	INTERNALmkDatatype(long a0, long a1, int a2, long[] a3)
protected static void	INTERNALmkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
protected static long	INTERNALmkDistinct(long a0, int a1, long[] a2)
protected static long	INTERNALmkDiv(long a0, long a1, long a2)
protected static long	INTERNALmkDivides(long a0, long a1, long a2)
protected static long	INTERNALmkEmptySet(long a0, long a1)
protected static long	INTERNALmkEnumerationSort(long a0, long a1, int a2, long[] a3, long[] a4, long[] a5)
protected static long	INTERNALmkEq(long a0, long a1, long a2)
protected static long	INTERNALmkExists(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7)
protected static long	INTERNALmkExistsConst(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6)
protected static long	INTERNALmkExtract(long a0, int a1, int a2, long a3)
protected static long	INTERNALmkExtRotateLeft(long a0, long a1, long a2)
protected static long	INTERNALmkExtRotateRight(long a0, long a1, long a2)
protected static long	INTERNALmkFalse(long a0)
protected static long	INTERNALmkFiniteDomainSort(long a0, long a1, long a2)
protected static long	INTERNALmkFixedpoint(long a0)
protected static long	INTERNALmkForall(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7)
protected static long	INTERNALmkForallConst(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6)
protected static long	INTERNALmkFpaAbs(long a0, long a1)
protected static long	INTERNALmkFpaAdd(long a0, long a1, long a2, long a3)
protected static long	INTERNALmkFpaDiv(long a0, long a1, long a2, long a3)
protected static long	INTERNALmkFpaEq(long a0, long a1, long a2)
protected static long	INTERNALmkFpaFma(long a0, long a1, long a2, long a3, long a4)
protected static long	INTERNALmkFpaFp(long a0, long a1, long a2, long a3)
protected static long	INTERNALmkFpaGeq(long a0, long a1, long a2)
protected static long	INTERNALmkFpaGt(long a0, long a1, long a2)
protected static long	INTERNALmkFpaInf(long a0, long a1, boolean a2)
protected static long	INTERNALmkFpaIsInfinite(long a0, long a1)
protected static long	INTERNALmkFpaIsNan(long a0, long a1)
protected static long	INTERNALmkFpaIsNegative(long a0, long a1)
protected static long	INTERNALmkFpaIsNormal(long a0, long a1)
protected static long	INTERNALmkFpaIsPositive(long a0, long a1)
protected static long	INTERNALmkFpaIsSubnormal(long a0, long a1)
protected static long	INTERNALmkFpaIsZero(long a0, long a1)
protected static long	INTERNALmkFpaLeq(long a0, long a1, long a2)
protected static long	INTERNALmkFpaLt(long a0, long a1, long a2)
protected static long	INTERNALmkFpaMax(long a0, long a1, long a2)
protected static long	INTERNALmkFpaMin(long a0, long a1, long a2)
protected static long	INTERNALmkFpaMul(long a0, long a1, long a2, long a3)
protected static long	INTERNALmkFpaNan(long a0, long a1)
protected static long	INTERNALmkFpaNeg(long a0, long a1)
protected static long	INTERNALmkFpaNumeralDouble(long a0, double a1, long a2)
protected static long	INTERNALmkFpaNumeralFloat(long a0, float a1, long a2)
protected static long	INTERNALmkFpaNumeralInt(long a0, int a1, long a2)
protected static long	INTERNALmkFpaNumeralInt64Uint64(long a0, boolean a1, long a2, long a3, long a4)
protected static long	INTERNALmkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
protected static long	INTERNALmkFpaRem(long a0, long a1, long a2)
protected static long	INTERNALmkFpaRna(long a0)
protected static long	INTERNALmkFpaRne(long a0)
protected static long	INTERNALmkFpaRoundingModeSort(long a0)
protected static long	INTERNALmkFpaRoundNearestTiesToAway(long a0)
protected static long	INTERNALmkFpaRoundNearestTiesToEven(long a0)
protected static long	INTERNALmkFpaRoundToIntegral(long a0, long a1, long a2)
protected static long	INTERNALmkFpaRoundTowardNegative(long a0)
protected static long	INTERNALmkFpaRoundTowardPositive(long a0)
protected static long	INTERNALmkFpaRoundTowardZero(long a0)
protected static long	INTERNALmkFpaRtn(long a0)
protected static long	INTERNALmkFpaRtp(long a0)
protected static long	INTERNALmkFpaRtz(long a0)
protected static long	INTERNALmkFpaSort(long a0, int a1, int a2)
protected static long	INTERNALmkFpaSort128(long a0)
protected static long	INTERNALmkFpaSort16(long a0)
protected static long	INTERNALmkFpaSort32(long a0)
protected static long	INTERNALmkFpaSort64(long a0)
protected static long	INTERNALmkFpaSortDouble(long a0)
protected static long	INTERNALmkFpaSortHalf(long a0)
protected static long	INTERNALmkFpaSortQuadruple(long a0)
protected static long	INTERNALmkFpaSortSingle(long a0)
protected static long	INTERNALmkFpaSqrt(long a0, long a1, long a2)
protected static long	INTERNALmkFpaSub(long a0, long a1, long a2, long a3)
protected static long	INTERNALmkFpaToFpBv(long a0, long a1, long a2)
protected static long	INTERNALmkFpaToFpFloat(long a0, long a1, long a2, long a3)
protected static long	INTERNALmkFpaToFpIntReal(long a0, long a1, long a2, long a3, long a4)
protected static long	INTERNALmkFpaToFpReal(long a0, long a1, long a2, long a3)
protected static long	INTERNALmkFpaToFpSigned(long a0, long a1, long a2, long a3)
protected static long	INTERNALmkFpaToFpUnsigned(long a0, long a1, long a2, long a3)
protected static long	INTERNALmkFpaToIeeeBv(long a0, long a1)
protected static long	INTERNALmkFpaToReal(long a0, long a1)
protected static long	INTERNALmkFpaToSbv(long a0, long a1, long a2, int a3)
protected static long	INTERNALmkFpaToUbv(long a0, long a1, long a2, int a3)
protected static long	INTERNALmkFpaZero(long a0, long a1, boolean a2)
protected static long	INTERNALmkFreshConst(long a0, String a1, long a2)
protected static long	INTERNALmkFreshFuncDecl(long a0, String a1, int a2, long[] a3, long a4)
protected static long	INTERNALmkFullSet(long a0, long a1)
protected static long	INTERNALmkFuncDecl(long a0, long a1, int a2, long[] a3, long a4)
protected static long	INTERNALmkGe(long a0, long a1, long a2)
protected static long	INTERNALmkGoal(long a0, boolean a1, boolean a2, boolean a3)
protected static long	INTERNALmkGt(long a0, long a1, long a2)
protected static long	INTERNALmkIff(long a0, long a1, long a2)
protected static long	INTERNALmkImplies(long a0, long a1, long a2)
protected static long	INTERNALmkInt(long a0, int a1, long a2)
protected static long	INTERNALmkInt2bv(long a0, int a1, long a2)
protected static long	INTERNALmkInt2real(long a0, long a1)
protected static long	INTERNALmkInt64(long a0, long a1, long a2)
protected static long	INTERNALmkIntSort(long a0)
protected static long	INTERNALmkIntSymbol(long a0, int a1)
protected static long	INTERNALmkIntToStr(long a0, long a1)
protected static long	INTERNALmkIsInt(long a0, long a1)
protected static long	INTERNALmkIte(long a0, long a1, long a2, long a3)
protected static long	INTERNALmkLambda(long a0, int a1, long[] a2, long[] a3, long a4)
protected static long	INTERNALmkLambdaConst(long a0, int a1, long[] a2, long a3)
protected static long	INTERNALmkLe(long a0, long a1, long a2)
protected static long	INTERNALmkLinearOrder(long a0, long a1, int a2)
protected static long	INTERNALmkListSort(long a0, long a1, long a2, Native.LongPtr a3, Native.LongPtr a4, Native.LongPtr a5, Native.LongPtr a6, Native.LongPtr a7, Native.LongPtr a8)
protected static long	INTERNALmkLstring(long a0, int a1, String a2)
protected static long	INTERNALmkLt(long a0, long a1, long a2)
protected static long	INTERNALmkMap(long a0, long a1, int a2, long[] a3)
protected static long	INTERNALmkMod(long a0, long a1, long a2)
protected static long	INTERNALmkModel(long a0)
protected static long	INTERNALmkMul(long a0, int a1, long[] a2)
protected static long	INTERNALmkNot(long a0, long a1)
protected static long	INTERNALmkNumeral(long a0, String a1, long a2)
protected static long	INTERNALmkOptimize(long a0)
protected static long	INTERNALmkOr(long a0, int a1, long[] a2)
protected static long	INTERNALmkParams(long a0)
protected static long	INTERNALmkPartialOrder(long a0, long a1, int a2)
protected static long	INTERNALmkPattern(long a0, int a1, long[] a2)
protected static long	INTERNALmkPbeq(long a0, int a1, long[] a2, int[] a3, int a4)
protected static long	INTERNALmkPbge(long a0, int a1, long[] a2, int[] a3, int a4)
protected static long	INTERNALmkPble(long a0, int a1, long[] a2, int[] a3, int a4)
protected static long	INTERNALmkPiecewiseLinearOrder(long a0, long a1, int a2)
protected static long	INTERNALmkPower(long a0, long a1, long a2)
protected static long	INTERNALmkProbe(long a0, String a1)
protected static long	INTERNALmkQuantifier(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8)
protected static long	INTERNALmkQuantifierConst(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7)
protected static 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)
protected static 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)
protected static long	INTERNALmkReal(long a0, int a1, int a2)
protected static long	INTERNALmkReal2int(long a0, long a1)
protected static long	INTERNALmkReAllchar(long a0, long a1)
protected static long	INTERNALmkRealSort(long a0)
protected static long	INTERNALmkRecFuncDecl(long a0, long a1, int a2, long[] a3, long a4)
protected static long	INTERNALmkReComplement(long a0, long a1)
protected static long	INTERNALmkReConcat(long a0, int a1, long[] a2)
protected static long	INTERNALmkReDiff(long a0, long a1, long a2)
protected static long	INTERNALmkReEmpty(long a0, long a1)
protected static long	INTERNALmkReFull(long a0, long a1)
protected static long	INTERNALmkReIntersect(long a0, int a1, long[] a2)
protected static long	INTERNALmkReLoop(long a0, long a1, int a2, int a3)
protected static long	INTERNALmkRem(long a0, long a1, long a2)
protected static long	INTERNALmkReOption(long a0, long a1)
protected static long	INTERNALmkRepeat(long a0, int a1, long a2)
protected static long	INTERNALmkRePlus(long a0, long a1)
protected static long	INTERNALmkRePower(long a0, long a1, int a2)
protected static long	INTERNALmkReRange(long a0, long a1, long a2)
protected static long	INTERNALmkReSort(long a0, long a1)
protected static long	INTERNALmkReStar(long a0, long a1)
protected static long	INTERNALmkReUnion(long a0, int a1, long[] a2)
protected static long	INTERNALmkRotateLeft(long a0, int a1, long a2)
protected static long	INTERNALmkRotateRight(long a0, int a1, long a2)
protected static long	INTERNALmkSbvToStr(long a0, long a1)
protected static long	INTERNALmkSelect(long a0, long a1, long a2)
protected static long	INTERNALmkSelectN(long a0, long a1, int a2, long[] a3)
protected static long	INTERNALmkSeqAt(long a0, long a1, long a2)
protected static long	INTERNALmkSeqConcat(long a0, int a1, long[] a2)
protected static long	INTERNALmkSeqContains(long a0, long a1, long a2)
protected static long	INTERNALmkSeqEmpty(long a0, long a1)
protected static long	INTERNALmkSeqExtract(long a0, long a1, long a2, long a3)
protected static long	INTERNALmkSeqIndex(long a0, long a1, long a2, long a3)
protected static long	INTERNALmkSeqInRe(long a0, long a1, long a2)
protected static long	INTERNALmkSeqLastIndex(long a0, long a1, long a2)
protected static long	INTERNALmkSeqLength(long a0, long a1)
protected static long	INTERNALmkSeqNth(long a0, long a1, long a2)
protected static long	INTERNALmkSeqPrefix(long a0, long a1, long a2)
protected static long	INTERNALmkSeqReplace(long a0, long a1, long a2, long a3)
protected static long	INTERNALmkSeqSort(long a0, long a1)
protected static long	INTERNALmkSeqSuffix(long a0, long a1, long a2)
protected static long	INTERNALmkSeqToRe(long a0, long a1)
protected static long	INTERNALmkSeqUnit(long a0, long a1)
protected static long	INTERNALmkSetAdd(long a0, long a1, long a2)
protected static long	INTERNALmkSetComplement(long a0, long a1)
protected static long	INTERNALmkSetDel(long a0, long a1, long a2)
protected static long	INTERNALmkSetDifference(long a0, long a1, long a2)
protected static long	INTERNALmkSetHasSize(long a0, long a1, long a2)
protected static long	INTERNALmkSetIntersect(long a0, int a1, long[] a2)
protected static long	INTERNALmkSetMember(long a0, long a1, long a2)
protected static long	INTERNALmkSetSort(long a0, long a1)
protected static long	INTERNALmkSetSubset(long a0, long a1, long a2)
protected static long	INTERNALmkSetUnion(long a0, int a1, long[] a2)
protected static long	INTERNALmkSignExt(long a0, int a1, long a2)
protected static long	INTERNALmkSimpleSolver(long a0)
protected static long	INTERNALmkSolver(long a0)
protected static long	INTERNALmkSolverForLogic(long a0, long a1)
protected static long	INTERNALmkSolverFromTactic(long a0, long a1)
protected static long	INTERNALmkStore(long a0, long a1, long a2, long a3)
protected static long	INTERNALmkStoreN(long a0, long a1, int a2, long[] a3, long a4)
protected static long	INTERNALmkString(long a0, String a1)
protected static long	INTERNALmkStringFromCode(long a0, long a1)
protected static long	INTERNALmkStringSort(long a0)
protected static long	INTERNALmkStringSymbol(long a0, String a1)
protected static long	INTERNALmkStringToCode(long a0, long a1)
protected static long	INTERNALmkStrLe(long a0, long a1, long a2)
protected static long	INTERNALmkStrLt(long a0, long a1, long a2)
protected static long	INTERNALmkStrToInt(long a0, long a1)
protected static long	INTERNALmkSub(long a0, int a1, long[] a2)
protected static long	INTERNALmkTactic(long a0, String a1)
protected static long	INTERNALmkTransitiveClosure(long a0, long a1)
protected static long	INTERNALmkTreeOrder(long a0, long a1, int a2)
protected static long	INTERNALmkTrue(long a0)
protected static long	INTERNALmkTupleSort(long a0, long a1, int a2, long[] a3, long[] a4, Native.LongPtr a5, long[] a6)
protected static long	INTERNALmkU32string(long a0, int a1, int[] a2)
protected static long	INTERNALmkUbvToStr(long a0, long a1)
protected static long	INTERNALmkUnaryMinus(long a0, long a1)
protected static long	INTERNALmkUninterpretedSort(long a0, long a1)
protected static long	INTERNALmkUnsignedInt(long a0, int a1, long a2)
protected static long	INTERNALmkUnsignedInt64(long a0, long a1, long a2)
protected static long	INTERNALmkXor(long a0, long a1, long a2)
protected static long	INTERNALmkZeroExt(long a0, int a1, long a2)
protected static void	INTERNALmodelDecRef(long a0, long a1)
protected static boolean	INTERNALmodelEval(long a0, long a1, long a2, boolean a3, Native.LongPtr a4)
protected static long	INTERNALmodelExtrapolate(long a0, long a1, long a2)
protected static long	INTERNALmodelGetConstDecl(long a0, long a1, int a2)
protected static long	INTERNALmodelGetConstInterp(long a0, long a1, long a2)
protected static long	INTERNALmodelGetFuncDecl(long a0, long a1, int a2)
protected static long	INTERNALmodelGetFuncInterp(long a0, long a1, long a2)
protected static int	INTERNALmodelGetNumConsts(long a0, long a1)
protected static int	INTERNALmodelGetNumFuncs(long a0, long a1)
protected static int	INTERNALmodelGetNumSorts(long a0, long a1)
protected static long	INTERNALmodelGetSort(long a0, long a1, int a2)
protected static long	INTERNALmodelGetSortUniverse(long a0, long a1, long a2)
protected static boolean	INTERNALmodelHasInterp(long a0, long a1, long a2)
protected static void	INTERNALmodelIncRef(long a0, long a1)
protected static String	INTERNALmodelToString(long a0, long a1)
protected static long	INTERNALmodelTranslate(long a0, long a1, long a2)
protected static int	INTERNALopenLog(String a0)
protected static void	INTERNALoptimizeAssert(long a0, long a1, long a2)
protected static void	INTERNALoptimizeAssertAndTrack(long a0, long a1, long a2, long a3)
protected static int	INTERNALoptimizeAssertSoft(long a0, long a1, long a2, String a3, long a4)
protected static int	INTERNALoptimizeCheck(long a0, long a1, int a2, long[] a3)
protected static void	INTERNALoptimizeDecRef(long a0, long a1)
protected static void	INTERNALoptimizeFromFile(long a0, long a1, String a2)
protected static void	INTERNALoptimizeFromString(long a0, long a1, String a2)
protected static long	INTERNALoptimizeGetAssertions(long a0, long a1)
protected static String	INTERNALoptimizeGetHelp(long a0, long a1)
protected static long	INTERNALoptimizeGetLower(long a0, long a1, int a2)
protected static long	INTERNALoptimizeGetLowerAsVector(long a0, long a1, int a2)
protected static long	INTERNALoptimizeGetModel(long a0, long a1)
protected static long	INTERNALoptimizeGetObjectives(long a0, long a1)
protected static long	INTERNALoptimizeGetParamDescrs(long a0, long a1)
protected static String	INTERNALoptimizeGetReasonUnknown(long a0, long a1)
protected static long	INTERNALoptimizeGetStatistics(long a0, long a1)
protected static long	INTERNALoptimizeGetUnsatCore(long a0, long a1)
protected static long	INTERNALoptimizeGetUpper(long a0, long a1, int a2)
protected static long	INTERNALoptimizeGetUpperAsVector(long a0, long a1, int a2)
protected static void	INTERNALoptimizeIncRef(long a0, long a1)
protected static int	INTERNALoptimizeMaximize(long a0, long a1, long a2)
protected static int	INTERNALoptimizeMinimize(long a0, long a1, long a2)
protected static void	INTERNALoptimizePop(long a0, long a1)
protected static void	INTERNALoptimizePush(long a0, long a1)
protected static void	INTERNALoptimizeSetParams(long a0, long a1, long a2)
protected static String	INTERNALoptimizeToString(long a0, long a1)
protected static void	INTERNALparamDescrsDecRef(long a0, long a1)
protected static String	INTERNALparamDescrsGetDocumentation(long a0, long a1, long a2)
protected static int	INTERNALparamDescrsGetKind(long a0, long a1, long a2)
protected static long	INTERNALparamDescrsGetName(long a0, long a1, int a2)
protected static void	INTERNALparamDescrsIncRef(long a0, long a1)
protected static int	INTERNALparamDescrsSize(long a0, long a1)
protected static String	INTERNALparamDescrsToString(long a0, long a1)
protected static void	INTERNALparamsDecRef(long a0, long a1)
protected static void	INTERNALparamsIncRef(long a0, long a1)
protected static void	INTERNALparamsSetBool(long a0, long a1, long a2, boolean a3)
protected static void	INTERNALparamsSetDouble(long a0, long a1, long a2, double a3)
protected static void	INTERNALparamsSetSymbol(long a0, long a1, long a2, long a3)
protected static void	INTERNALparamsSetUint(long a0, long a1, long a2, int a3)
protected static String	INTERNALparamsToString(long a0, long a1)
protected static void	INTERNALparamsValidate(long a0, long a1, long a2)
protected static long	INTERNALparseSmtlib2File(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
protected static long	INTERNALparseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
protected static long	INTERNALpatternToAst(long a0, long a1)
protected static String	INTERNALpatternToString(long a0, long a1)
protected static long	INTERNALpolynomialSubresultants(long a0, long a1, long a2, long a3)
protected static long	INTERNALprobeAnd(long a0, long a1, long a2)
protected static double	INTERNALprobeApply(long a0, long a1, long a2)
protected static long	INTERNALprobeConst(long a0, double a1)
protected static void	INTERNALprobeDecRef(long a0, long a1)
protected static long	INTERNALprobeEq(long a0, long a1, long a2)
protected static long	INTERNALprobeGe(long a0, long a1, long a2)
protected static String	INTERNALprobeGetDescr(long a0, String a1)
protected static long	INTERNALprobeGt(long a0, long a1, long a2)
protected static void	INTERNALprobeIncRef(long a0, long a1)
protected static long	INTERNALprobeLe(long a0, long a1, long a2)
protected static long	INTERNALprobeLt(long a0, long a1, long a2)
protected static long	INTERNALprobeNot(long a0, long a1)
protected static long	INTERNALprobeOr(long a0, long a1, long a2)
protected static long	INTERNALqeLite(long a0, long a1, long a2)
protected static long	INTERNALqeModelProject(long a0, long a1, int a2, long[] a3, long a4)
protected static long	INTERNALqeModelProjectSkolem(long a0, long a1, int a2, long[] a3, long a4, long a5)
protected static void	INTERNALqueryConstructor(long a0, long a1, int a2, Native.LongPtr a3, Native.LongPtr a4, long[] a5)
protected static long	INTERNALrcfAdd(long a0, long a1, long a2)
protected static void	INTERNALrcfDel(long a0, long a1)
protected static long	INTERNALrcfDiv(long a0, long a1, long a2)
protected static boolean	INTERNALrcfEq(long a0, long a1, long a2)
protected static boolean	INTERNALrcfGe(long a0, long a1, long a2)
protected static void	INTERNALrcfGetNumeratorDenominator(long a0, long a1, Native.LongPtr a2, Native.LongPtr a3)
protected static boolean	INTERNALrcfGt(long a0, long a1, long a2)
protected static long	INTERNALrcfInv(long a0, long a1)
protected static boolean	INTERNALrcfLe(long a0, long a1, long a2)
protected static boolean	INTERNALrcfLt(long a0, long a1, long a2)
protected static long	INTERNALrcfMkE(long a0)
protected static long	INTERNALrcfMkInfinitesimal(long a0)
protected static long	INTERNALrcfMkPi(long a0)
protected static long	INTERNALrcfMkRational(long a0, String a1)
protected static int	INTERNALrcfMkRoots(long a0, int a1, long[] a2, long[] a3)
protected static long	INTERNALrcfMkSmallInt(long a0, int a1)
protected static long	INTERNALrcfMul(long a0, long a1, long a2)
protected static long	INTERNALrcfNeg(long a0, long a1)
protected static boolean	INTERNALrcfNeq(long a0, long a1, long a2)
protected static String	INTERNALrcfNumToDecimalString(long a0, long a1, int a2)
protected static String	INTERNALrcfNumToString(long a0, long a1, boolean a2, boolean a3)
protected static long	INTERNALrcfPower(long a0, long a1, int a2)
protected static long	INTERNALrcfSub(long a0, long a1, long a2)
protected static void	INTERNALresetMemory()
protected static void	INTERNALsetAstPrintMode(long a0, int a1)
protected static void	INTERNALsetError(long a0, int a1)
protected static void	INTERNALsetParamValue(long a0, String a1, String a2)
protected static long	INTERNALsimplify(long a0, long a1)
protected static long	INTERNALsimplifyEx(long a0, long a1, long a2)
protected static String	INTERNALsimplifyGetHelp(long a0)
protected static long	INTERNALsimplifyGetParamDescrs(long a0)
protected static void	INTERNALsolverAssert(long a0, long a1, long a2)
protected static void	INTERNALsolverAssertAndTrack(long a0, long a1, long a2, long a3)
protected static int	INTERNALsolverCheck(long a0, long a1)
protected static int	INTERNALsolverCheckAssumptions(long a0, long a1, int a2, long[] a3)
protected static long	INTERNALsolverCube(long a0, long a1, long a2, int a3)
protected static void	INTERNALsolverDecRef(long a0, long a1)
protected static void	INTERNALsolverFromFile(long a0, long a1, String a2)
protected static void	INTERNALsolverFromString(long a0, long a1, String a2)
protected static long	INTERNALsolverGetAssertions(long a0, long a1)
protected static int	INTERNALsolverGetConsequences(long a0, long a1, long a2, long a3, long a4)
protected static String	INTERNALsolverGetHelp(long a0, long a1)
protected static void	INTERNALsolverGetLevels(long a0, long a1, long a2, int a3, int[] a4)
protected static long	INTERNALsolverGetModel(long a0, long a1)
protected static long	INTERNALsolverGetNonUnits(long a0, long a1)
protected static int	INTERNALsolverGetNumScopes(long a0, long a1)
protected static long	INTERNALsolverGetParamDescrs(long a0, long a1)
protected static long	INTERNALsolverGetProof(long a0, long a1)
protected static String	INTERNALsolverGetReasonUnknown(long a0, long a1)
protected static long	INTERNALsolverGetStatistics(long a0, long a1)
protected static long	INTERNALsolverGetTrail(long a0, long a1)
protected static long	INTERNALsolverGetUnits(long a0, long a1)
protected static long	INTERNALsolverGetUnsatCore(long a0, long a1)
protected static void	INTERNALsolverImportModelConverter(long a0, long a1, long a2)
protected static void	INTERNALsolverIncRef(long a0, long a1)
protected static void	INTERNALsolverInterrupt(long a0, long a1)
protected static void	INTERNALsolverPop(long a0, long a1, int a2)
protected static void	INTERNALsolverPropagateConsequence(long a0, long a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7)
protected static long	INTERNALsolverPropagateDeclare(long a0, long a1, int a2, long[] a3, long a4)
protected static void	INTERNALsolverPropagateRegister(long a0, long a1, long a2)
protected static void	INTERNALsolverPropagateRegisterCb(long a0, long a1, long a2)
protected static void	INTERNALsolverPush(long a0, long a1)
protected static void	INTERNALsolverReset(long a0, long a1)
protected static void	INTERNALsolverSetParams(long a0, long a1, long a2)
protected static String	INTERNALsolverToDimacsString(long a0, long a1, boolean a2)
protected static String	INTERNALsolverToString(long a0, long a1)
protected static long	INTERNALsolverTranslate(long a0, long a1, long a2)
protected static long	INTERNALsortToAst(long a0, long a1)
protected static String	INTERNALsortToString(long a0, long a1)
protected static void	INTERNALstatsDecRef(long a0, long a1)
protected static double	INTERNALstatsGetDoubleValue(long a0, long a1, int a2)
protected static String	INTERNALstatsGetKey(long a0, long a1, int a2)
protected static int	INTERNALstatsGetUintValue(long a0, long a1, int a2)
protected static void	INTERNALstatsIncRef(long a0, long a1)
protected static boolean	INTERNALstatsIsDouble(long a0, long a1, int a2)
protected static boolean	INTERNALstatsIsUint(long a0, long a1, int a2)
protected static int	INTERNALstatsSize(long a0, long a1)
protected static String	INTERNALstatsToString(long a0, long a1)
protected static long	INTERNALsubstitute(long a0, long a1, int a2, long[] a3, long[] a4)
protected static long	INTERNALsubstituteVars(long a0, long a1, int a2, long[] a3)
protected static long	INTERNALtacticAndThen(long a0, long a1, long a2)
protected static long	INTERNALtacticApply(long a0, long a1, long a2)
protected static long	INTERNALtacticApplyEx(long a0, long a1, long a2, long a3)
protected static long	INTERNALtacticCond(long a0, long a1, long a2, long a3)
protected static void	INTERNALtacticDecRef(long a0, long a1)
protected static long	INTERNALtacticFail(long a0)
protected static long	INTERNALtacticFailIf(long a0, long a1)
protected static long	INTERNALtacticFailIfNotDecided(long a0)
protected static String	INTERNALtacticGetDescr(long a0, String a1)
protected static String	INTERNALtacticGetHelp(long a0, long a1)
protected static long	INTERNALtacticGetParamDescrs(long a0, long a1)
protected static void	INTERNALtacticIncRef(long a0, long a1)
protected static long	INTERNALtacticOrElse(long a0, long a1, long a2)
protected static long	INTERNALtacticParAndThen(long a0, long a1, long a2)
protected static long	INTERNALtacticParOr(long a0, int a1, long[] a2)
protected static long	INTERNALtacticRepeat(long a0, long a1, int a2)
protected static long	INTERNALtacticSkip(long a0)
protected static long	INTERNALtacticTryFor(long a0, long a1, int a2)
protected static long	INTERNALtacticUsingParams(long a0, long a1, long a2)
protected static long	INTERNALtacticWhen(long a0, long a1, long a2)
protected static long	INTERNALtoApp(long a0, long a1)
protected static long	INTERNALtoFuncDecl(long a0, long a1)
protected static void	INTERNALtoggleWarningMessages(boolean a0)
protected static long	INTERNALtranslate(long a0, long a1, long a2)
protected static void	INTERNALupdateParamValue(long a0, String a1, String a2)
protected static long	INTERNALupdateTerm(long a0, long a1, int a2, long[] a3)
static void	interrupt(long a0)
static boolean	isAlgebraicNumber(long a0, long a1)
static boolean	isApp(long a0, long a1)
static boolean	isAsArray(long a0, long a1)
static boolean	isCharSort(long a0, long a1)
static boolean	isEqAst(long a0, long a1, long a2)
static boolean	isEqFuncDecl(long a0, long a1, long a2)
static boolean	isEqSort(long a0, long a1, long a2)
static boolean	isLambda(long a0, long a1)
static boolean	isNumeralAst(long a0, long a1)
static boolean	isQuantifierExists(long a0, long a1)
static boolean	isQuantifierForall(long a0, long a1)
static boolean	isReSort(long a0, long a1)
static boolean	isSeqSort(long a0, long a1)
static boolean	isString(long a0, long a1)
static boolean	isStringSort(long a0, long a1)
static boolean	isWellSorted(long a0, long a1)
static long	mkAdd(long a0, int a1, long[] a2)
static long	mkAnd(long a0, int a1, long[] a2)
static long	mkApp(long a0, long a1, int a2, long[] a3)
static long	mkArrayDefault(long a0, long a1)
static long	mkArrayExt(long a0, long a1, long a2)
static long	mkArraySort(long a0, long a1, long a2)
static long	mkArraySortN(long a0, int a1, long[] a2, long a3)
static long	mkAsArray(long a0, long a1)
static long	mkAstMap(long a0)
static long	mkAstVector(long a0)
static long	mkAtleast(long a0, int a1, long[] a2, int a3)
static long	mkAtmost(long a0, int a1, long[] a2, int a3)
static long	mkBoolSort(long a0)
static long	mkBound(long a0, int a1, long a2)
static long	mkBv2int(long a0, long a1, boolean a2)
static long	mkBvadd(long a0, long a1, long a2)
static long	mkBvaddNoOverflow(long a0, long a1, long a2, boolean a3)
static long	mkBvaddNoUnderflow(long a0, long a1, long a2)
static long	mkBvand(long a0, long a1, long a2)
static long	mkBvashr(long a0, long a1, long a2)
static long	mkBvlshr(long a0, long a1, long a2)
static long	mkBvmul(long a0, long a1, long a2)
static long	mkBvmulNoOverflow(long a0, long a1, long a2, boolean a3)
static long	mkBvmulNoUnderflow(long a0, long a1, long a2)
static long	mkBvnand(long a0, long a1, long a2)
static long	mkBvneg(long a0, long a1)
static long	mkBvnegNoOverflow(long a0, long a1)
static long	mkBvnor(long a0, long a1, long a2)
static long	mkBvnot(long a0, long a1)
static long	mkBvNumeral(long a0, int a1, boolean[] a2)
static long	mkBvor(long a0, long a1, long a2)
static long	mkBvredand(long a0, long a1)
static long	mkBvredor(long a0, long a1)
static long	mkBvsdiv(long a0, long a1, long a2)
static long	mkBvsdivNoOverflow(long a0, long a1, long a2)
static long	mkBvsge(long a0, long a1, long a2)
static long	mkBvsgt(long a0, long a1, long a2)
static long	mkBvshl(long a0, long a1, long a2)
static long	mkBvsle(long a0, long a1, long a2)
static long	mkBvslt(long a0, long a1, long a2)
static long	mkBvsmod(long a0, long a1, long a2)
static long	mkBvSort(long a0, int a1)
static long	mkBvsrem(long a0, long a1, long a2)
static long	mkBvsub(long a0, long a1, long a2)
static long	mkBvsubNoOverflow(long a0, long a1, long a2)
static long	mkBvsubNoUnderflow(long a0, long a1, long a2, boolean a3)
static long	mkBvudiv(long a0, long a1, long a2)
static long	mkBvuge(long a0, long a1, long a2)
static long	mkBvugt(long a0, long a1, long a2)
static long	mkBvule(long a0, long a1, long a2)
static long	mkBvult(long a0, long a1, long a2)
static long	mkBvurem(long a0, long a1, long a2)
static long	mkBvxnor(long a0, long a1, long a2)
static long	mkBvxor(long a0, long a1, long a2)
static long	mkChar(long a0, int a1)
static long	mkCharFromBv(long a0, long a1)
static long	mkCharIsDigit(long a0, long a1)
static long	mkCharLe(long a0, long a1, long a2)
static long	mkCharSort(long a0)
static long	mkCharToBv(long a0, long a1)
static long	mkCharToInt(long a0, long a1)
static long	mkConcat(long a0, long a1, long a2)
static long	mkConfig()
static long	mkConst(long a0, long a1, long a2)
static long	mkConstArray(long a0, long a1, long a2)
static long	mkConstructor(long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6)
static long	mkConstructorList(long a0, int a1, long[] a2)
static long	mkContext(long a0)
static long	mkContextRc(long a0)
static long	mkDatatype(long a0, long a1, int a2, long[] a3)
static void	mkDatatypes(long a0, int a1, long[] a2, long[] a3, long[] a4)
static long	mkDistinct(long a0, int a1, long[] a2)
static long	mkDiv(long a0, long a1, long a2)
static long	mkDivides(long a0, long a1, long a2)
static long	mkEmptySet(long a0, long a1)
static long	mkEnumerationSort(long a0, long a1, int a2, long[] a3, long[] a4, long[] a5)
static long	mkEq(long a0, long a1, long a2)
static long	mkExists(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7)
static long	mkExistsConst(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6)
static long	mkExtract(long a0, int a1, int a2, long a3)
static long	mkExtRotateLeft(long a0, long a1, long a2)
static long	mkExtRotateRight(long a0, long a1, long a2)
static long	mkFalse(long a0)
static long	mkFiniteDomainSort(long a0, long a1, long a2)
static long	mkFixedpoint(long a0)
static long	mkForall(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7)
static long	mkForallConst(long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6)
static long	mkFpaAbs(long a0, long a1)
static long	mkFpaAdd(long a0, long a1, long a2, long a3)
static long	mkFpaDiv(long a0, long a1, long a2, long a3)
static long	mkFpaEq(long a0, long a1, long a2)
static long	mkFpaFma(long a0, long a1, long a2, long a3, long a4)
static long	mkFpaFp(long a0, long a1, long a2, long a3)
static long	mkFpaGeq(long a0, long a1, long a2)
static long	mkFpaGt(long a0, long a1, long a2)
static long	mkFpaInf(long a0, long a1, boolean a2)
static long	mkFpaIsInfinite(long a0, long a1)
static long	mkFpaIsNan(long a0, long a1)
static long	mkFpaIsNegative(long a0, long a1)
static long	mkFpaIsNormal(long a0, long a1)
static long	mkFpaIsPositive(long a0, long a1)
static long	mkFpaIsSubnormal(long a0, long a1)
static long	mkFpaIsZero(long a0, long a1)
static long	mkFpaLeq(long a0, long a1, long a2)
static long	mkFpaLt(long a0, long a1, long a2)
static long	mkFpaMax(long a0, long a1, long a2)
static long	mkFpaMin(long a0, long a1, long a2)
static long	mkFpaMul(long a0, long a1, long a2, long a3)
static long	mkFpaNan(long a0, long a1)
static long	mkFpaNeg(long a0, long a1)
static long	mkFpaNumeralDouble(long a0, double a1, long a2)
static long	mkFpaNumeralFloat(long a0, float a1, long a2)
static long	mkFpaNumeralInt(long a0, int a1, long a2)
static long	mkFpaNumeralInt64Uint64(long a0, boolean a1, long a2, long a3, long a4)
static long	mkFpaNumeralIntUint(long a0, boolean a1, int a2, int a3, long a4)
static long	mkFpaRem(long a0, long a1, long a2)
static long	mkFpaRna(long a0)
static long	mkFpaRne(long a0)
static long	mkFpaRoundingModeSort(long a0)
static long	mkFpaRoundNearestTiesToAway(long a0)
static long	mkFpaRoundNearestTiesToEven(long a0)
static long	mkFpaRoundToIntegral(long a0, long a1, long a2)
static long	mkFpaRoundTowardNegative(long a0)
static long	mkFpaRoundTowardPositive(long a0)
static long	mkFpaRoundTowardZero(long a0)
static long	mkFpaRtn(long a0)
static long	mkFpaRtp(long a0)
static long	mkFpaRtz(long a0)
static long	mkFpaSort(long a0, int a1, int a2)
static long	mkFpaSort128(long a0)
static long	mkFpaSort16(long a0)
static long	mkFpaSort32(long a0)
static long	mkFpaSort64(long a0)
static long	mkFpaSortDouble(long a0)
static long	mkFpaSortHalf(long a0)
static long	mkFpaSortQuadruple(long a0)
static long	mkFpaSortSingle(long a0)
static long	mkFpaSqrt(long a0, long a1, long a2)
static long	mkFpaSub(long a0, long a1, long a2, long a3)
static long	mkFpaToFpBv(long a0, long a1, long a2)
static long	mkFpaToFpFloat(long a0, long a1, long a2, long a3)
static long	mkFpaToFpIntReal(long a0, long a1, long a2, long a3, long a4)
static long	mkFpaToFpReal(long a0, long a1, long a2, long a3)
static long	mkFpaToFpSigned(long a0, long a1, long a2, long a3)
static long	mkFpaToFpUnsigned(long a0, long a1, long a2, long a3)
static long	mkFpaToIeeeBv(long a0, long a1)
static long	mkFpaToReal(long a0, long a1)
static long	mkFpaToSbv(long a0, long a1, long a2, int a3)
static long	mkFpaToUbv(long a0, long a1, long a2, int a3)
static long	mkFpaZero(long a0, long a1, boolean a2)
static long	mkFreshConst(long a0, String a1, long a2)
static long	mkFreshFuncDecl(long a0, String a1, int a2, long[] a3, long a4)
static long	mkFullSet(long a0, long a1)
static long	mkFuncDecl(long a0, long a1, int a2, long[] a3, long a4)
static long	mkGe(long a0, long a1, long a2)
static long	mkGoal(long a0, boolean a1, boolean a2, boolean a3)
static long	mkGt(long a0, long a1, long a2)
static long	mkIff(long a0, long a1, long a2)
static long	mkImplies(long a0, long a1, long a2)
static long	mkInt(long a0, int a1, long a2)
static long	mkInt2bv(long a0, int a1, long a2)
static long	mkInt2real(long a0, long a1)
static long	mkInt64(long a0, long a1, long a2)
static long	mkIntSort(long a0)
static long	mkIntSymbol(long a0, int a1)
static long	mkIntToStr(long a0, long a1)
static long	mkIsInt(long a0, long a1)
static long	mkIte(long a0, long a1, long a2, long a3)
static long	mkLambda(long a0, int a1, long[] a2, long[] a3, long a4)
static long	mkLambdaConst(long a0, int a1, long[] a2, long a3)
static long	mkLe(long a0, long a1, long a2)
static long	mkLinearOrder(long a0, long a1, int a2)
static long	mkListSort(long a0, long a1, long a2, Native.LongPtr a3, Native.LongPtr a4, Native.LongPtr a5, Native.LongPtr a6, Native.LongPtr a7, Native.LongPtr a8)
static long	mkLstring(long a0, int a1, String a2)
static long	mkLt(long a0, long a1, long a2)
static long	mkMap(long a0, long a1, int a2, long[] a3)
static long	mkMod(long a0, long a1, long a2)
static long	mkModel(long a0)
static long	mkMul(long a0, int a1, long[] a2)
static long	mkNot(long a0, long a1)
static long	mkNumeral(long a0, String a1, long a2)
static long	mkOptimize(long a0)
static long	mkOr(long a0, int a1, long[] a2)
static long	mkParams(long a0)
static long	mkPartialOrder(long a0, long a1, int a2)
static long	mkPattern(long a0, int a1, long[] a2)
static long	mkPbeq(long a0, int a1, long[] a2, int[] a3, int a4)
static long	mkPbge(long a0, int a1, long[] a2, int[] a3, int a4)
static long	mkPble(long a0, int a1, long[] a2, int[] a3, int a4)
static long	mkPiecewiseLinearOrder(long a0, long a1, int a2)
static long	mkPower(long a0, long a1, long a2)
static long	mkProbe(long a0, String a1)
static long	mkQuantifier(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8)
static long	mkQuantifierConst(long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7)
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 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 long	mkReal(long a0, int a1, int a2)
static long	mkReal2int(long a0, long a1)
static long	mkReAllchar(long a0, long a1)
static long	mkRealSort(long a0)
static long	mkRecFuncDecl(long a0, long a1, int a2, long[] a3, long a4)
static long	mkReComplement(long a0, long a1)
static long	mkReConcat(long a0, int a1, long[] a2)
static long	mkReDiff(long a0, long a1, long a2)
static long	mkReEmpty(long a0, long a1)
static long	mkReFull(long a0, long a1)
static long	mkReIntersect(long a0, int a1, long[] a2)
static long	mkReLoop(long a0, long a1, int a2, int a3)
static long	mkRem(long a0, long a1, long a2)
static long	mkReOption(long a0, long a1)
static long	mkRepeat(long a0, int a1, long a2)
static long	mkRePlus(long a0, long a1)
static long	mkRePower(long a0, long a1, int a2)
static long	mkReRange(long a0, long a1, long a2)
static long	mkReSort(long a0, long a1)
static long	mkReStar(long a0, long a1)
static long	mkReUnion(long a0, int a1, long[] a2)
static long	mkRotateLeft(long a0, int a1, long a2)
static long	mkRotateRight(long a0, int a1, long a2)
static long	mkSbvToStr(long a0, long a1)
static long	mkSelect(long a0, long a1, long a2)
static long	mkSelectN(long a0, long a1, int a2, long[] a3)
static long	mkSeqAt(long a0, long a1, long a2)
static long	mkSeqConcat(long a0, int a1, long[] a2)
static long	mkSeqContains(long a0, long a1, long a2)
static long	mkSeqEmpty(long a0, long a1)
static long	mkSeqExtract(long a0, long a1, long a2, long a3)
static long	mkSeqIndex(long a0, long a1, long a2, long a3)
static long	mkSeqInRe(long a0, long a1, long a2)
static long	mkSeqLastIndex(long a0, long a1, long a2)
static long	mkSeqLength(long a0, long a1)
static long	mkSeqNth(long a0, long a1, long a2)
static long	mkSeqPrefix(long a0, long a1, long a2)
static long	mkSeqReplace(long a0, long a1, long a2, long a3)
static long	mkSeqSort(long a0, long a1)
static long	mkSeqSuffix(long a0, long a1, long a2)
static long	mkSeqToRe(long a0, long a1)
static long	mkSeqUnit(long a0, long a1)
static long	mkSetAdd(long a0, long a1, long a2)
static long	mkSetComplement(long a0, long a1)
static long	mkSetDel(long a0, long a1, long a2)
static long	mkSetDifference(long a0, long a1, long a2)
static long	mkSetHasSize(long a0, long a1, long a2)
static long	mkSetIntersect(long a0, int a1, long[] a2)
static long	mkSetMember(long a0, long a1, long a2)
static long	mkSetSort(long a0, long a1)
static long	mkSetSubset(long a0, long a1, long a2)
static long	mkSetUnion(long a0, int a1, long[] a2)
static long	mkSignExt(long a0, int a1, long a2)
static long	mkSimpleSolver(long a0)
static long	mkSolver(long a0)
static long	mkSolverForLogic(long a0, long a1)
static long	mkSolverFromTactic(long a0, long a1)
static long	mkStore(long a0, long a1, long a2, long a3)
static long	mkStoreN(long a0, long a1, int a2, long[] a3, long a4)
static long	mkString(long a0, String a1)
static long	mkStringFromCode(long a0, long a1)
static long	mkStringSort(long a0)
static long	mkStringSymbol(long a0, String a1)
static long	mkStringToCode(long a0, long a1)
static long	mkStrLe(long a0, long a1, long a2)
static long	mkStrLt(long a0, long a1, long a2)
static long	mkStrToInt(long a0, long a1)
static long	mkSub(long a0, int a1, long[] a2)
static long	mkTactic(long a0, String a1)
static long	mkTransitiveClosure(long a0, long a1)
static long	mkTreeOrder(long a0, long a1, int a2)
static long	mkTrue(long a0)
static long	mkTupleSort(long a0, long a1, int a2, long[] a3, long[] a4, Native.LongPtr a5, long[] a6)
static long	mkU32string(long a0, int a1, int[] a2)
static long	mkUbvToStr(long a0, long a1)
static long	mkUnaryMinus(long a0, long a1)
static long	mkUninterpretedSort(long a0, long a1)
static long	mkUnsignedInt(long a0, int a1, long a2)
static long	mkUnsignedInt64(long a0, long a1, long a2)
static long	mkXor(long a0, long a1, long a2)
static long	mkZeroExt(long a0, int a1, long a2)
static void	modelDecRef(long a0, long a1)
static boolean	modelEval(long a0, long a1, long a2, boolean a3, Native.LongPtr a4)
static long	modelExtrapolate(long a0, long a1, long a2)
static long	modelGetConstDecl(long a0, long a1, int a2)
static long	modelGetConstInterp(long a0, long a1, long a2)
static long	modelGetFuncDecl(long a0, long a1, int a2)
static long	modelGetFuncInterp(long a0, long a1, long a2)
static int	modelGetNumConsts(long a0, long a1)
static int	modelGetNumFuncs(long a0, long a1)
static int	modelGetNumSorts(long a0, long a1)
static long	modelGetSort(long a0, long a1, int a2)
static long	modelGetSortUniverse(long a0, long a1, long a2)
static boolean	modelHasInterp(long a0, long a1, long a2)
static void	modelIncRef(long a0, long a1)
static String	modelToString(long a0, long a1)
static long	modelTranslate(long a0, long a1, long a2)
static int	openLog(String a0)
static void	optimizeAssert(long a0, long a1, long a2)
static void	optimizeAssertAndTrack(long a0, long a1, long a2, long a3)
static int	optimizeAssertSoft(long a0, long a1, long a2, String a3, long a4)
static int	optimizeCheck(long a0, long a1, int a2, long[] a3)
static void	optimizeDecRef(long a0, long a1)
static void	optimizeFromFile(long a0, long a1, String a2)
static void	optimizeFromString(long a0, long a1, String a2)
static long	optimizeGetAssertions(long a0, long a1)
static String	optimizeGetHelp(long a0, long a1)
static long	optimizeGetLower(long a0, long a1, int a2)
static long	optimizeGetLowerAsVector(long a0, long a1, int a2)
static long	optimizeGetModel(long a0, long a1)
static long	optimizeGetObjectives(long a0, long a1)
static long	optimizeGetParamDescrs(long a0, long a1)
static String	optimizeGetReasonUnknown(long a0, long a1)
static long	optimizeGetStatistics(long a0, long a1)
static long	optimizeGetUnsatCore(long a0, long a1)
static long	optimizeGetUpper(long a0, long a1, int a2)
static long	optimizeGetUpperAsVector(long a0, long a1, int a2)
static void	optimizeIncRef(long a0, long a1)
static int	optimizeMaximize(long a0, long a1, long a2)
static int	optimizeMinimize(long a0, long a1, long a2)
static void	optimizePop(long a0, long a1)
static void	optimizePush(long a0, long a1)
static void	optimizeSetParams(long a0, long a1, long a2)
static String	optimizeToString(long a0, long a1)
static void	paramDescrsDecRef(long a0, long a1)
static String	paramDescrsGetDocumentation(long a0, long a1, long a2)
static int	paramDescrsGetKind(long a0, long a1, long a2)
static long	paramDescrsGetName(long a0, long a1, int a2)
static void	paramDescrsIncRef(long a0, long a1)
static int	paramDescrsSize(long a0, long a1)
static String	paramDescrsToString(long a0, long a1)
static void	paramsDecRef(long a0, long a1)
static void	paramsIncRef(long a0, long a1)
static void	paramsSetBool(long a0, long a1, long a2, boolean a3)
static void	paramsSetDouble(long a0, long a1, long a2, double a3)
static void	paramsSetSymbol(long a0, long a1, long a2, long a3)
static void	paramsSetUint(long a0, long a1, long a2, int a3)
static String	paramsToString(long a0, long a1)
static void	paramsValidate(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 long	parseSmtlib2String(long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7)
static long	patternToAst(long a0, long a1)
static String	patternToString(long a0, long a1)
static long	polynomialSubresultants(long a0, long a1, long a2, long a3)
static long	probeAnd(long a0, long a1, long a2)
static double	probeApply(long a0, long a1, long a2)
static long	probeConst(long a0, double a1)
static void	probeDecRef(long a0, long a1)
static long	probeEq(long a0, long a1, long a2)
static long	probeGe(long a0, long a1, long a2)
static String	probeGetDescr(long a0, String a1)
static long	probeGt(long a0, long a1, long a2)
static void	probeIncRef(long a0, long a1)
static long	probeLe(long a0, long a1, long a2)
static long	probeLt(long a0, long a1, long a2)
static long	probeNot(long a0, long a1)
static long	probeOr(long a0, long a1, long a2)
static long	qeLite(long a0, long a1, long a2)
static long	qeModelProject(long a0, long a1, int a2, long[] a3, long a4)
static long	qeModelProjectSkolem(long a0, long a1, int a2, long[] a3, long a4, long a5)
static void	queryConstructor(long a0, long a1, int a2, Native.LongPtr a3, Native.LongPtr a4, long[] a5)
static long	rcfAdd(long a0, long a1, long a2)
static void	rcfDel(long a0, long a1)
static long	rcfDiv(long a0, long a1, long a2)
static boolean	rcfEq(long a0, long a1, long a2)
static boolean	rcfGe(long a0, long a1, long a2)
static void	rcfGetNumeratorDenominator(long a0, long a1, Native.LongPtr a2, Native.LongPtr a3)
static boolean	rcfGt(long a0, long a1, long a2)
static long	rcfInv(long a0, long a1)
static boolean	rcfLe(long a0, long a1, long a2)
static boolean	rcfLt(long a0, long a1, long a2)
static long	rcfMkE(long a0)
static long	rcfMkInfinitesimal(long a0)
static long	rcfMkPi(long a0)
static long	rcfMkRational(long a0, String a1)
static int	rcfMkRoots(long a0, int a1, long[] a2, long[] a3)
static long	rcfMkSmallInt(long a0, int a1)
static long	rcfMul(long a0, long a1, long a2)
static long	rcfNeg(long a0, long a1)
static boolean	rcfNeq(long a0, long a1, long a2)
static String	rcfNumToDecimalString(long a0, long a1, int a2)
static String	rcfNumToString(long a0, long a1, boolean a2, boolean a3)
static long	rcfPower(long a0, long a1, int a2)
static long	rcfSub(long a0, long a1, long a2)
static void	resetMemory()
static void	setAstPrintMode(long a0, int a1)
static void	setError(long a0, int a1)
static void	setInternalErrorHandler(long ctx)
static void	setParamValue(long a0, String a1, String a2)
static long	simplify(long a0, long a1)
static long	simplifyEx(long a0, long a1, long a2)
static String	simplifyGetHelp(long a0)
static long	simplifyGetParamDescrs(long a0)
static void	solverAssert(long a0, long a1, long a2)
static void	solverAssertAndTrack(long a0, long a1, long a2, long a3)
static int	solverCheck(long a0, long a1)
static int	solverCheckAssumptions(long a0, long a1, int a2, long[] a3)
static long	solverCube(long a0, long a1, long a2, int a3)
static void	solverDecRef(long a0, long a1)
static void	solverFromFile(long a0, long a1, String a2)
static void	solverFromString(long a0, long a1, String a2)
static long	solverGetAssertions(long a0, long a1)
static int	solverGetConsequences(long a0, long a1, long a2, long a3, long a4)
static String	solverGetHelp(long a0, long a1)
static void	solverGetLevels(long a0, long a1, long a2, int a3, int[] a4)
static long	solverGetModel(long a0, long a1)
static long	solverGetNonUnits(long a0, long a1)
static int	solverGetNumScopes(long a0, long a1)
static long	solverGetParamDescrs(long a0, long a1)
static long	solverGetProof(long a0, long a1)
static String	solverGetReasonUnknown(long a0, long a1)
static long	solverGetStatistics(long a0, long a1)
static long	solverGetTrail(long a0, long a1)
static long	solverGetUnits(long a0, long a1)
static long	solverGetUnsatCore(long a0, long a1)
static void	solverImportModelConverter(long a0, long a1, long a2)
static void	solverIncRef(long a0, long a1)
static void	solverInterrupt(long a0, long a1)
static void	solverPop(long a0, long a1, int a2)
static void	solverPropagateConsequence(long a0, long a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7)
static long	solverPropagateDeclare(long a0, long a1, int a2, long[] a3, long a4)
static void	solverPropagateRegister(long a0, long a1, long a2)
static void	solverPropagateRegisterCb(long a0, long a1, long a2)
static void	solverPush(long a0, long a1)
static void	solverReset(long a0, long a1)
static void	solverSetParams(long a0, long a1, long a2)
static String	solverToDimacsString(long a0, long a1, boolean a2)
static String	solverToString(long a0, long a1)
static long	solverTranslate(long a0, long a1, long a2)
static long	sortToAst(long a0, long a1)
static String	sortToString(long a0, long a1)
static void	statsDecRef(long a0, long a1)
static double	statsGetDoubleValue(long a0, long a1, int a2)
static String	statsGetKey(long a0, long a1, int a2)
static int	statsGetUintValue(long a0, long a1, int a2)
static void	statsIncRef(long a0, long a1)
static boolean	statsIsDouble(long a0, long a1, int a2)
static boolean	statsIsUint(long a0, long a1, int a2)
static int	statsSize(long a0, long a1)
static String	statsToString(long a0, long a1)
static long	substitute(long a0, long a1, int a2, long[] a3, long[] a4)
static long	substituteVars(long a0, long a1, int a2, long[] a3)
static long	tacticAndThen(long a0, long a1, long a2)
static long	tacticApply(long a0, long a1, long a2)
static long	tacticApplyEx(long a0, long a1, long a2, long a3)
static long	tacticCond(long a0, long a1, long a2, long a3)
static void	tacticDecRef(long a0, long a1)
static long	tacticFail(long a0)
static long	tacticFailIf(long a0, long a1)
static long	tacticFailIfNotDecided(long a0)
static String	tacticGetDescr(long a0, String a1)
static String	tacticGetHelp(long a0, long a1)
static long	tacticGetParamDescrs(long a0, long a1)
static void	tacticIncRef(long a0, long a1)
static long	tacticOrElse(long a0, long a1, long a2)
static long	tacticParAndThen(long a0, long a1, long a2)
static long	tacticParOr(long a0, int a1, long[] a2)
static long	tacticRepeat(long a0, long a1, int a2)
static long	tacticSkip(long a0)
static long	tacticTryFor(long a0, long a1, int a2)
static long	tacticUsingParams(long a0, long a1, long a2)
static long	tacticWhen(long a0, long a1, long a2)
static long	toApp(long a0, long a1)
static long	toFuncDecl(long a0, long a1)
static void	toggleWarningMessages(boolean a0)
static long	translate(long a0, long a1, long a2)
static void	updateParamValue(long a0, String a1, String a2)
static long	updateTerm(long a0, long a1, int a2, long[] a3)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

Native

public Native()

Method Details

setInternalErrorHandler

public static void setInternalErrorHandler(long ctx)

INTERNALglobalParamSet

protected static void INTERNALglobalParamSet(String a0,
 String a1)

INTERNALglobalParamResetAll

protected static void INTERNALglobalParamResetAll()

INTERNALglobalParamGet

protected static boolean INTERNALglobalParamGet(String a0,
 Native.StringPtr a1)

INTERNALmkConfig

protected static long INTERNALmkConfig()

INTERNALdelConfig

protected static void INTERNALdelConfig(long a0)

INTERNALsetParamValue

protected static void INTERNALsetParamValue(long a0,
 String a1,
 String a2)

INTERNALmkContext

protected static long INTERNALmkContext(long a0)

INTERNALmkContextRc

protected static long INTERNALmkContextRc(long a0)

INTERNALdelContext

protected static void INTERNALdelContext(long a0)

INTERNALincRef

protected static void INTERNALincRef(long a0,
 long a1)

INTERNALdecRef

protected static void INTERNALdecRef(long a0,
 long a1)

INTERNALupdateParamValue

protected static void INTERNALupdateParamValue(long a0,
 String a1,
 String a2)

INTERNALinterrupt

protected static void INTERNALinterrupt(long a0)

INTERNALmkParams

protected static long INTERNALmkParams(long a0)

INTERNALparamsIncRef

protected static void INTERNALparamsIncRef(long a0,
 long a1)

INTERNALparamsDecRef

protected static void INTERNALparamsDecRef(long a0,
 long a1)

INTERNALparamsSetBool

protected static void INTERNALparamsSetBool(long a0,
 long a1,
 long a2,
 boolean a3)

INTERNALparamsSetUint

protected static void INTERNALparamsSetUint(long a0,
 long a1,
 long a2,
 int a3)

INTERNALparamsSetDouble

protected static void INTERNALparamsSetDouble(long a0,
 long a1,
 long a2,
 double a3)

INTERNALparamsSetSymbol

protected static void INTERNALparamsSetSymbol(long a0,
 long a1,
 long a2,
 long a3)

INTERNALparamsToString

protected static String INTERNALparamsToString(long a0,
 long a1)

INTERNALparamsValidate

protected static void INTERNALparamsValidate(long a0,
 long a1,
 long a2)

INTERNALparamDescrsIncRef

protected static void INTERNALparamDescrsIncRef(long a0,
 long a1)

INTERNALparamDescrsDecRef

protected static void INTERNALparamDescrsDecRef(long a0,
 long a1)

INTERNALparamDescrsGetKind

protected static int INTERNALparamDescrsGetKind(long a0,
 long a1,
 long a2)

INTERNALparamDescrsSize

protected static int INTERNALparamDescrsSize(long a0,
 long a1)

INTERNALparamDescrsGetName

protected static long INTERNALparamDescrsGetName(long a0,
 long a1,
 int a2)

INTERNALparamDescrsGetDocumentation

protected static String INTERNALparamDescrsGetDocumentation(long a0,
 long a1,
 long a2)

INTERNALparamDescrsToString

protected static String INTERNALparamDescrsToString(long a0,
 long a1)

INTERNALmkIntSymbol

protected static long INTERNALmkIntSymbol(long a0,
 int a1)

INTERNALmkStringSymbol

protected static long INTERNALmkStringSymbol(long a0,
 String a1)

INTERNALmkUninterpretedSort

protected static long INTERNALmkUninterpretedSort(long a0,
 long a1)

INTERNALmkBoolSort

protected static long INTERNALmkBoolSort(long a0)

INTERNALmkIntSort

protected static long INTERNALmkIntSort(long a0)

INTERNALmkRealSort

protected static long INTERNALmkRealSort(long a0)

INTERNALmkBvSort

protected static long INTERNALmkBvSort(long a0,
 int a1)

INTERNALmkFiniteDomainSort

protected static long INTERNALmkFiniteDomainSort(long a0,
 long a1,
 long a2)

INTERNALmkArraySort

protected static long INTERNALmkArraySort(long a0,
 long a1,
 long a2)

INTERNALmkArraySortN

protected static long INTERNALmkArraySortN(long a0,
 int a1,
 long[] a2,
 long a3)

INTERNALmkTupleSort

protected static long INTERNALmkTupleSort(long a0,
 long a1,
 int a2,
 long[] a3,
 long[] a4,
 Native.LongPtr a5,
 long[] a6)

INTERNALmkEnumerationSort

protected static long INTERNALmkEnumerationSort(long a0,
 long a1,
 int a2,
 long[] a3,
 long[] a4,
 long[] a5)

INTERNALmkListSort

protected static long INTERNALmkListSort(long a0,
 long a1,
 long a2,
 Native.LongPtr a3,
 Native.LongPtr a4,
 Native.LongPtr a5,
 Native.LongPtr a6,
 Native.LongPtr a7,
 Native.LongPtr a8)

INTERNALmkConstructor

protected static long INTERNALmkConstructor(long a0,
 long a1,
 long a2,
 int a3,
 long[] a4,
 long[] a5,
 int[] a6)

INTERNALdelConstructor

protected static void INTERNALdelConstructor(long a0,
 long a1)

INTERNALmkDatatype

protected static long INTERNALmkDatatype(long a0,
 long a1,
 int a2,
 long[] a3)

INTERNALmkConstructorList

protected static long INTERNALmkConstructorList(long a0,
 int a1,
 long[] a2)

INTERNALdelConstructorList

protected static void INTERNALdelConstructorList(long a0,
 long a1)

INTERNALmkDatatypes

protected static void INTERNALmkDatatypes(long a0,
 int a1,
 long[] a2,
 long[] a3,
 long[] a4)

INTERNALqueryConstructor

protected static void INTERNALqueryConstructor(long a0,
 long a1,
 int a2,
 Native.LongPtr a3,
 Native.LongPtr a4,
 long[] a5)

INTERNALmkFuncDecl

protected static long INTERNALmkFuncDecl(long a0,
 long a1,
 int a2,
 long[] a3,
 long a4)

INTERNALmkApp

protected static long INTERNALmkApp(long a0,
 long a1,
 int a2,
 long[] a3)

INTERNALmkConst

protected static long INTERNALmkConst(long a0,
 long a1,
 long a2)

INTERNALmkFreshFuncDecl

protected static long INTERNALmkFreshFuncDecl(long a0,
 String a1,
 int a2,
 long[] a3,
 long a4)

INTERNALmkFreshConst

protected static long INTERNALmkFreshConst(long a0,
 String a1,
 long a2)

INTERNALmkRecFuncDecl

protected static long INTERNALmkRecFuncDecl(long a0,
 long a1,
 int a2,
 long[] a3,
 long a4)

INTERNALaddRecDef

protected static void INTERNALaddRecDef(long a0,
 long a1,
 int a2,
 long[] a3,
 long a4)

INTERNALmkTrue

protected static long INTERNALmkTrue(long a0)

INTERNALmkFalse

protected static long INTERNALmkFalse(long a0)

INTERNALmkEq

protected static long INTERNALmkEq(long a0,
 long a1,
 long a2)

INTERNALmkDistinct

protected static long INTERNALmkDistinct(long a0,
 int a1,
 long[] a2)

INTERNALmkNot

protected static long INTERNALmkNot(long a0,
 long a1)

INTERNALmkIte

protected static long INTERNALmkIte(long a0,
 long a1,
 long a2,
 long a3)

INTERNALmkIff

protected static long INTERNALmkIff(long a0,
 long a1,
 long a2)

INTERNALmkImplies

protected static long INTERNALmkImplies(long a0,
 long a1,
 long a2)

INTERNALmkXor

protected static long INTERNALmkXor(long a0,
 long a1,
 long a2)

INTERNALmkAnd

protected static long INTERNALmkAnd(long a0,
 int a1,
 long[] a2)

INTERNALmkOr

protected static long INTERNALmkOr(long a0,
 int a1,
 long[] a2)

INTERNALmkAdd

protected static long INTERNALmkAdd(long a0,
 int a1,
 long[] a2)

INTERNALmkMul

protected static long INTERNALmkMul(long a0,
 int a1,
 long[] a2)

INTERNALmkSub

protected static long INTERNALmkSub(long a0,
 int a1,
 long[] a2)

INTERNALmkUnaryMinus

protected static long INTERNALmkUnaryMinus(long a0,
 long a1)

INTERNALmkDiv

protected static long INTERNALmkDiv(long a0,
 long a1,
 long a2)

INTERNALmkMod

protected static long INTERNALmkMod(long a0,
 long a1,
 long a2)

INTERNALmkRem

protected static long INTERNALmkRem(long a0,
 long a1,
 long a2)

INTERNALmkPower

protected static long INTERNALmkPower(long a0,
 long a1,
 long a2)

INTERNALmkLt

protected static long INTERNALmkLt(long a0,
 long a1,
 long a2)

INTERNALmkLe

protected static long INTERNALmkLe(long a0,
 long a1,
 long a2)

INTERNALmkGt

protected static long INTERNALmkGt(long a0,
 long a1,
 long a2)

INTERNALmkGe

protected static long INTERNALmkGe(long a0,
 long a1,
 long a2)

INTERNALmkDivides

protected static long INTERNALmkDivides(long a0,
 long a1,
 long a2)

INTERNALmkInt2real

protected static long INTERNALmkInt2real(long a0,
 long a1)

INTERNALmkReal2int

protected static long INTERNALmkReal2int(long a0,
 long a1)

INTERNALmkIsInt

protected static long INTERNALmkIsInt(long a0,
 long a1)

INTERNALmkBvnot

protected static long INTERNALmkBvnot(long a0,
 long a1)

INTERNALmkBvredand

protected static long INTERNALmkBvredand(long a0,
 long a1)

INTERNALmkBvredor

protected static long INTERNALmkBvredor(long a0,
 long a1)

INTERNALmkBvand

protected static long INTERNALmkBvand(long a0,
 long a1,
 long a2)

INTERNALmkBvor

protected static long INTERNALmkBvor(long a0,
 long a1,
 long a2)

INTERNALmkBvxor

protected static long INTERNALmkBvxor(long a0,
 long a1,
 long a2)

INTERNALmkBvnand

protected static long INTERNALmkBvnand(long a0,
 long a1,
 long a2)

INTERNALmkBvnor

protected static long INTERNALmkBvnor(long a0,
 long a1,
 long a2)

INTERNALmkBvxnor

protected static long INTERNALmkBvxnor(long a0,
 long a1,
 long a2)

INTERNALmkBvneg

protected static long INTERNALmkBvneg(long a0,
 long a1)

INTERNALmkBvadd

protected static long INTERNALmkBvadd(long a0,
 long a1,
 long a2)

INTERNALmkBvsub

protected static long INTERNALmkBvsub(long a0,
 long a1,
 long a2)

INTERNALmkBvmul

protected static long INTERNALmkBvmul(long a0,
 long a1,
 long a2)

INTERNALmkBvudiv

protected static long INTERNALmkBvudiv(long a0,
 long a1,
 long a2)

INTERNALmkBvsdiv

protected static long INTERNALmkBvsdiv(long a0,
 long a1,
 long a2)

INTERNALmkBvurem

protected static long INTERNALmkBvurem(long a0,
 long a1,
 long a2)

INTERNALmkBvsrem

protected static long INTERNALmkBvsrem(long a0,
 long a1,
 long a2)

INTERNALmkBvsmod

protected static long INTERNALmkBvsmod(long a0,
 long a1,
 long a2)

INTERNALmkBvult

protected static long INTERNALmkBvult(long a0,
 long a1,
 long a2)

INTERNALmkBvslt

protected static long INTERNALmkBvslt(long a0,
 long a1,
 long a2)

INTERNALmkBvule

protected static long INTERNALmkBvule(long a0,
 long a1,
 long a2)

INTERNALmkBvsle

protected static long INTERNALmkBvsle(long a0,
 long a1,
 long a2)

INTERNALmkBvuge

protected static long INTERNALmkBvuge(long a0,
 long a1,
 long a2)

INTERNALmkBvsge

protected static long INTERNALmkBvsge(long a0,
 long a1,
 long a2)

INTERNALmkBvugt

protected static long INTERNALmkBvugt(long a0,
 long a1,
 long a2)

INTERNALmkBvsgt

protected static long INTERNALmkBvsgt(long a0,
 long a1,
 long a2)

INTERNALmkConcat

protected static long INTERNALmkConcat(long a0,
 long a1,
 long a2)

INTERNALmkExtract

protected static long INTERNALmkExtract(long a0,
 int a1,
 int a2,
 long a3)

INTERNALmkSignExt

protected static long INTERNALmkSignExt(long a0,
 int a1,
 long a2)

INTERNALmkZeroExt

protected static long INTERNALmkZeroExt(long a0,
 int a1,
 long a2)

INTERNALmkRepeat

protected static long INTERNALmkRepeat(long a0,
 int a1,
 long a2)

INTERNALmkBvshl

protected static long INTERNALmkBvshl(long a0,
 long a1,
 long a2)

INTERNALmkBvlshr

protected static long INTERNALmkBvlshr(long a0,
 long a1,
 long a2)

INTERNALmkBvashr

protected static long INTERNALmkBvashr(long a0,
 long a1,
 long a2)

INTERNALmkRotateLeft

protected static long INTERNALmkRotateLeft(long a0,
 int a1,
 long a2)

INTERNALmkRotateRight

protected static long INTERNALmkRotateRight(long a0,
 int a1,
 long a2)

INTERNALmkExtRotateLeft

protected static long INTERNALmkExtRotateLeft(long a0,
 long a1,
 long a2)

INTERNALmkExtRotateRight

protected static long INTERNALmkExtRotateRight(long a0,
 long a1,
 long a2)

INTERNALmkInt2bv

protected static long INTERNALmkInt2bv(long a0,
 int a1,
 long a2)

INTERNALmkBv2int

protected static long INTERNALmkBv2int(long a0,
 long a1,
 boolean a2)

INTERNALmkBvaddNoOverflow

protected static long INTERNALmkBvaddNoOverflow(long a0,
 long a1,
 long a2,
 boolean a3)

INTERNALmkBvaddNoUnderflow

protected static long INTERNALmkBvaddNoUnderflow(long a0,
 long a1,
 long a2)

INTERNALmkBvsubNoOverflow

protected static long INTERNALmkBvsubNoOverflow(long a0,
 long a1,
 long a2)

INTERNALmkBvsubNoUnderflow

protected static long INTERNALmkBvsubNoUnderflow(long a0,
 long a1,
 long a2,
 boolean a3)

INTERNALmkBvsdivNoOverflow

protected static long INTERNALmkBvsdivNoOverflow(long a0,
 long a1,
 long a2)

INTERNALmkBvnegNoOverflow

protected static long INTERNALmkBvnegNoOverflow(long a0,
 long a1)

INTERNALmkBvmulNoOverflow

protected static long INTERNALmkBvmulNoOverflow(long a0,
 long a1,
 long a2,
 boolean a3)

INTERNALmkBvmulNoUnderflow

protected static long INTERNALmkBvmulNoUnderflow(long a0,
 long a1,
 long a2)

INTERNALmkSelect

protected static long INTERNALmkSelect(long a0,
 long a1,
 long a2)

INTERNALmkSelectN

protected static long INTERNALmkSelectN(long a0,
 long a1,
 int a2,
 long[] a3)

INTERNALmkStore

protected static long INTERNALmkStore(long a0,
 long a1,
 long a2,
 long a3)

INTERNALmkStoreN

protected static long INTERNALmkStoreN(long a0,
 long a1,
 int a2,
 long[] a3,
 long a4)

INTERNALmkConstArray

protected static long INTERNALmkConstArray(long a0,
 long a1,
 long a2)

INTERNALmkMap

protected static long INTERNALmkMap(long a0,
 long a1,
 int a2,
 long[] a3)

INTERNALmkArrayDefault

protected static long INTERNALmkArrayDefault(long a0,
 long a1)

INTERNALmkAsArray

protected static long INTERNALmkAsArray(long a0,
 long a1)

INTERNALmkSetHasSize

protected static long INTERNALmkSetHasSize(long a0,
 long a1,
 long a2)

INTERNALmkSetSort

protected static long INTERNALmkSetSort(long a0,
 long a1)

INTERNALmkEmptySet

protected static long INTERNALmkEmptySet(long a0,
 long a1)

INTERNALmkFullSet

protected static long INTERNALmkFullSet(long a0,
 long a1)

INTERNALmkSetAdd

protected static long INTERNALmkSetAdd(long a0,
 long a1,
 long a2)

INTERNALmkSetDel

protected static long INTERNALmkSetDel(long a0,
 long a1,
 long a2)

INTERNALmkSetUnion

protected static long INTERNALmkSetUnion(long a0,
 int a1,
 long[] a2)

INTERNALmkSetIntersect

protected static long INTERNALmkSetIntersect(long a0,
 int a1,
 long[] a2)

INTERNALmkSetDifference

protected static long INTERNALmkSetDifference(long a0,
 long a1,
 long a2)

INTERNALmkSetComplement

protected static long INTERNALmkSetComplement(long a0,
 long a1)

INTERNALmkSetMember

protected static long INTERNALmkSetMember(long a0,
 long a1,
 long a2)

INTERNALmkSetSubset

protected static long INTERNALmkSetSubset(long a0,
 long a1,
 long a2)

INTERNALmkArrayExt

protected static long INTERNALmkArrayExt(long a0,
 long a1,
 long a2)

INTERNALmkNumeral

protected static long INTERNALmkNumeral(long a0,
 String a1,
 long a2)

INTERNALmkReal

protected static long INTERNALmkReal(long a0,
 int a1,
 int a2)

INTERNALmkInt

protected static long INTERNALmkInt(long a0,
 int a1,
 long a2)

INTERNALmkUnsignedInt

protected static long INTERNALmkUnsignedInt(long a0,
 int a1,
 long a2)

INTERNALmkInt64

protected static long INTERNALmkInt64(long a0,
 long a1,
 long a2)

INTERNALmkUnsignedInt64

protected static long INTERNALmkUnsignedInt64(long a0,
 long a1,
 long a2)

INTERNALmkBvNumeral

protected static long INTERNALmkBvNumeral(long a0,
 int a1,
 boolean[] a2)

INTERNALmkSeqSort

protected static long INTERNALmkSeqSort(long a0,
 long a1)

INTERNALisSeqSort

protected static boolean INTERNALisSeqSort(long a0,
 long a1)

INTERNALgetSeqSortBasis

protected static long INTERNALgetSeqSortBasis(long a0,
 long a1)

INTERNALmkReSort

protected static long INTERNALmkReSort(long a0,
 long a1)

INTERNALisReSort

protected static boolean INTERNALisReSort(long a0,
 long a1)

INTERNALgetReSortBasis

protected static long INTERNALgetReSortBasis(long a0,
 long a1)

INTERNALmkStringSort

protected static long INTERNALmkStringSort(long a0)

INTERNALmkCharSort

protected static long INTERNALmkCharSort(long a0)

INTERNALisStringSort

protected static boolean INTERNALisStringSort(long a0,
 long a1)

INTERNALisCharSort

protected static boolean INTERNALisCharSort(long a0,
 long a1)

INTERNALmkString

protected static long INTERNALmkString(long a0,
 String a1)

INTERNALmkLstring

protected static long INTERNALmkLstring(long a0,
 int a1,
 String a2)

INTERNALmkU32string

protected static long INTERNALmkU32string(long a0,
 int a1,
 int[] a2)

INTERNALisString

protected static boolean INTERNALisString(long a0,
 long a1)

INTERNALgetString

protected static String INTERNALgetString(long a0,
 long a1)

INTERNALgetLstring

protected static long INTERNALgetLstring(long a0,
 long a1,
 Native.IntPtr a2)

INTERNALgetStringLength

protected static int INTERNALgetStringLength(long a0,
 long a1)

INTERNALgetStringContents

protected static void INTERNALgetStringContents(long a0,
 long a1,
 int a2,
 int[] a3)

INTERNALmkSeqEmpty

protected static long INTERNALmkSeqEmpty(long a0,
 long a1)

INTERNALmkSeqUnit

protected static long INTERNALmkSeqUnit(long a0,
 long a1)

INTERNALmkSeqConcat

protected static long INTERNALmkSeqConcat(long a0,
 int a1,
 long[] a2)

INTERNALmkSeqPrefix

protected static long INTERNALmkSeqPrefix(long a0,
 long a1,
 long a2)

INTERNALmkSeqSuffix

protected static long INTERNALmkSeqSuffix(long a0,
 long a1,
 long a2)

INTERNALmkSeqContains

protected static long INTERNALmkSeqContains(long a0,
 long a1,
 long a2)

INTERNALmkStrLt

protected static long INTERNALmkStrLt(long a0,
 long a1,
 long a2)

INTERNALmkStrLe

protected static long INTERNALmkStrLe(long a0,
 long a1,
 long a2)

INTERNALmkSeqExtract

protected static long INTERNALmkSeqExtract(long a0,
 long a1,
 long a2,
 long a3)

INTERNALmkSeqReplace

protected static long INTERNALmkSeqReplace(long a0,
 long a1,
 long a2,
 long a3)

INTERNALmkSeqAt

protected static long INTERNALmkSeqAt(long a0,
 long a1,
 long a2)

INTERNALmkSeqNth

protected static long INTERNALmkSeqNth(long a0,
 long a1,
 long a2)

INTERNALmkSeqLength

protected static long INTERNALmkSeqLength(long a0,
 long a1)

INTERNALmkSeqIndex

protected static long INTERNALmkSeqIndex(long a0,
 long a1,
 long a2,
 long a3)

INTERNALmkSeqLastIndex

protected static long INTERNALmkSeqLastIndex(long a0,
 long a1,
 long a2)

INTERNALmkStrToInt

protected static long INTERNALmkStrToInt(long a0,
 long a1)

INTERNALmkIntToStr

protected static long INTERNALmkIntToStr(long a0,
 long a1)

INTERNALmkStringToCode

protected static long INTERNALmkStringToCode(long a0,
 long a1)

INTERNALmkStringFromCode

protected static long INTERNALmkStringFromCode(long a0,
 long a1)

INTERNALmkUbvToStr

protected static long INTERNALmkUbvToStr(long a0,
 long a1)

INTERNALmkSbvToStr

protected static long INTERNALmkSbvToStr(long a0,
 long a1)

INTERNALmkSeqToRe

protected static long INTERNALmkSeqToRe(long a0,
 long a1)

INTERNALmkSeqInRe

protected static long INTERNALmkSeqInRe(long a0,
 long a1,
 long a2)

INTERNALmkRePlus

protected static long INTERNALmkRePlus(long a0,
 long a1)

INTERNALmkReStar

protected static long INTERNALmkReStar(long a0,
 long a1)

INTERNALmkReOption

protected static long INTERNALmkReOption(long a0,
 long a1)

INTERNALmkReUnion

protected static long INTERNALmkReUnion(long a0,
 int a1,
 long[] a2)

INTERNALmkReConcat

protected static long INTERNALmkReConcat(long a0,
 int a1,
 long[] a2)

INTERNALmkReRange

protected static long INTERNALmkReRange(long a0,
 long a1,
 long a2)

INTERNALmkReAllchar

protected static long INTERNALmkReAllchar(long a0,
 long a1)

INTERNALmkReLoop

protected static long INTERNALmkReLoop(long a0,
 long a1,
 int a2,
 int a3)

INTERNALmkRePower

protected static long INTERNALmkRePower(long a0,
 long a1,
 int a2)

INTERNALmkReIntersect

protected static long INTERNALmkReIntersect(long a0,
 int a1,
 long[] a2)

INTERNALmkReComplement

protected static long INTERNALmkReComplement(long a0,
 long a1)

INTERNALmkReDiff

protected static long INTERNALmkReDiff(long a0,
 long a1,
 long a2)

INTERNALmkReEmpty

protected static long INTERNALmkReEmpty(long a0,
 long a1)

INTERNALmkReFull

protected static long INTERNALmkReFull(long a0,
 long a1)

INTERNALmkChar

protected static long INTERNALmkChar(long a0,
 int a1)

INTERNALmkCharLe

protected static long INTERNALmkCharLe(long a0,
 long a1,
 long a2)

INTERNALmkCharToInt

protected static long INTERNALmkCharToInt(long a0,
 long a1)

INTERNALmkCharToBv

protected static long INTERNALmkCharToBv(long a0,
 long a1)

INTERNALmkCharFromBv

protected static long INTERNALmkCharFromBv(long a0,
 long a1)

INTERNALmkCharIsDigit

protected static long INTERNALmkCharIsDigit(long a0,
 long a1)

INTERNALmkLinearOrder

protected static long INTERNALmkLinearOrder(long a0,
 long a1,
 int a2)

INTERNALmkPartialOrder

protected static long INTERNALmkPartialOrder(long a0,
 long a1,
 int a2)

INTERNALmkPiecewiseLinearOrder

protected static long INTERNALmkPiecewiseLinearOrder(long a0,
 long a1,
 int a2)

INTERNALmkTreeOrder

protected static long INTERNALmkTreeOrder(long a0,
 long a1,
 int a2)

INTERNALmkTransitiveClosure

protected static long INTERNALmkTransitiveClosure(long a0,
 long a1)

INTERNALmkPattern

protected static long INTERNALmkPattern(long a0,
 int a1,
 long[] a2)

INTERNALmkBound

protected static long INTERNALmkBound(long a0,
 int a1,
 long a2)

INTERNALmkForall

protected static long INTERNALmkForall(long a0,
 int a1,
 int a2,
 long[] a3,
 int a4,
 long[] a5,
 long[] a6,
 long a7)

INTERNALmkExists

protected static long INTERNALmkExists(long a0,
 int a1,
 int a2,
 long[] a3,
 int a4,
 long[] a5,
 long[] a6,
 long a7)

INTERNALmkQuantifier

protected static long INTERNALmkQuantifier(long a0,
 boolean a1,
 int a2,
 int a3,
 long[] a4,
 int a5,
 long[] a6,
 long[] a7,
 long a8)

INTERNALmkQuantifierEx

protected static 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)

INTERNALmkForallConst

protected static long INTERNALmkForallConst(long a0,
 int a1,
 int a2,
 long[] a3,
 int a4,
 long[] a5,
 long a6)

INTERNALmkExistsConst

protected static long INTERNALmkExistsConst(long a0,
 int a1,
 int a2,
 long[] a3,
 int a4,
 long[] a5,
 long a6)

INTERNALmkQuantifierConst

protected static long INTERNALmkQuantifierConst(long a0,
 boolean a1,
 int a2,
 int a3,
 long[] a4,
 int a5,
 long[] a6,
 long a7)

INTERNALmkQuantifierConstEx

protected static 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)

INTERNALmkLambda

protected static long INTERNALmkLambda(long a0,
 int a1,
 long[] a2,
 long[] a3,
 long a4)

INTERNALmkLambdaConst

protected static long INTERNALmkLambdaConst(long a0,
 int a1,
 long[] a2,
 long a3)

INTERNALgetSymbolKind

protected static int INTERNALgetSymbolKind(long a0,
 long a1)

INTERNALgetSymbolInt

protected static int INTERNALgetSymbolInt(long a0,
 long a1)

INTERNALgetSymbolString

protected static String INTERNALgetSymbolString(long a0,
 long a1)

INTERNALgetSortName

protected static long INTERNALgetSortName(long a0,
 long a1)

INTERNALgetSortId

protected static int INTERNALgetSortId(long a0,
 long a1)

INTERNALsortToAst

protected static long INTERNALsortToAst(long a0,
 long a1)

INTERNALisEqSort

protected static boolean INTERNALisEqSort(long a0,
 long a1,
 long a2)

INTERNALgetSortKind

protected static int INTERNALgetSortKind(long a0,
 long a1)

INTERNALgetBvSortSize

protected static int INTERNALgetBvSortSize(long a0,
 long a1)

INTERNALgetFiniteDomainSortSize

protected static boolean INTERNALgetFiniteDomainSortSize(long a0,
 long a1,
 Native.LongPtr a2)

INTERNALgetArraySortDomain

protected static long INTERNALgetArraySortDomain(long a0,
 long a1)

INTERNALgetArraySortDomainN

protected static long INTERNALgetArraySortDomainN(long a0,
 long a1,
 int a2)

INTERNALgetArraySortRange

protected static long INTERNALgetArraySortRange(long a0,
 long a1)

INTERNALgetTupleSortMkDecl

protected static long INTERNALgetTupleSortMkDecl(long a0,
 long a1)

INTERNALgetTupleSortNumFields

protected static int INTERNALgetTupleSortNumFields(long a0,
 long a1)

INTERNALgetTupleSortFieldDecl

protected static long INTERNALgetTupleSortFieldDecl(long a0,
 long a1,
 int a2)

INTERNALgetDatatypeSortNumConstructors

protected static int INTERNALgetDatatypeSortNumConstructors(long a0,
 long a1)

INTERNALgetDatatypeSortConstructor

protected static long INTERNALgetDatatypeSortConstructor(long a0,
 long a1,
 int a2)

INTERNALgetDatatypeSortRecognizer

protected static long INTERNALgetDatatypeSortRecognizer(long a0,
 long a1,
 int a2)

INTERNALgetDatatypeSortConstructorAccessor

protected static long INTERNALgetDatatypeSortConstructorAccessor(long a0,
 long a1,
 int a2,
 int a3)

INTERNALdatatypeUpdateField

protected static long INTERNALdatatypeUpdateField(long a0,
 long a1,
 long a2,
 long a3)

INTERNALgetRelationArity

protected static int INTERNALgetRelationArity(long a0,
 long a1)

INTERNALgetRelationColumn

protected static long INTERNALgetRelationColumn(long a0,
 long a1,
 int a2)

INTERNALmkAtmost

protected static long INTERNALmkAtmost(long a0,
 int a1,
 long[] a2,
 int a3)

INTERNALmkAtleast

protected static long INTERNALmkAtleast(long a0,
 int a1,
 long[] a2,
 int a3)

INTERNALmkPble

protected static long INTERNALmkPble(long a0,
 int a1,
 long[] a2,
 int[] a3,
 int a4)

INTERNALmkPbge

protected static long INTERNALmkPbge(long a0,
 int a1,
 long[] a2,
 int[] a3,
 int a4)

INTERNALmkPbeq

protected static long INTERNALmkPbeq(long a0,
 int a1,
 long[] a2,
 int[] a3,
 int a4)

INTERNALfuncDeclToAst

protected static long INTERNALfuncDeclToAst(long a0,
 long a1)

INTERNALisEqFuncDecl

protected static boolean INTERNALisEqFuncDecl(long a0,
 long a1,
 long a2)

INTERNALgetFuncDeclId

protected static int INTERNALgetFuncDeclId(long a0,
 long a1)

INTERNALgetDeclName

protected static long INTERNALgetDeclName(long a0,
 long a1)

INTERNALgetDeclKind

protected static int INTERNALgetDeclKind(long a0,
 long a1)

INTERNALgetDomainSize

protected static int INTERNALgetDomainSize(long a0,
 long a1)

INTERNALgetArity

protected static int INTERNALgetArity(long a0,
 long a1)

INTERNALgetDomain

protected static long INTERNALgetDomain(long a0,
 long a1,
 int a2)

INTERNALgetRange

protected static long INTERNALgetRange(long a0,
 long a1)

INTERNALgetDeclNumParameters

protected static int INTERNALgetDeclNumParameters(long a0,
 long a1)

INTERNALgetDeclParameterKind

protected static int INTERNALgetDeclParameterKind(long a0,
 long a1,
 int a2)

INTERNALgetDeclIntParameter

protected static int INTERNALgetDeclIntParameter(long a0,
 long a1,
 int a2)

INTERNALgetDeclDoubleParameter

protected static double INTERNALgetDeclDoubleParameter(long a0,
 long a1,
 int a2)

INTERNALgetDeclSymbolParameter

protected static long INTERNALgetDeclSymbolParameter(long a0,
 long a1,
 int a2)

INTERNALgetDeclSortParameter

protected static long INTERNALgetDeclSortParameter(long a0,
 long a1,
 int a2)

INTERNALgetDeclAstParameter

protected static long INTERNALgetDeclAstParameter(long a0,
 long a1,
 int a2)

INTERNALgetDeclFuncDeclParameter

protected static long INTERNALgetDeclFuncDeclParameter(long a0,
 long a1,
 int a2)

INTERNALgetDeclRationalParameter

protected static String INTERNALgetDeclRationalParameter(long a0,
 long a1,
 int a2)

INTERNALappToAst

protected static long INTERNALappToAst(long a0,
 long a1)

INTERNALgetAppDecl

protected static long INTERNALgetAppDecl(long a0,
 long a1)

INTERNALgetAppNumArgs

protected static int INTERNALgetAppNumArgs(long a0,
 long a1)

INTERNALgetAppArg

protected static long INTERNALgetAppArg(long a0,
 long a1,
 int a2)

INTERNALisEqAst

protected static boolean INTERNALisEqAst(long a0,
 long a1,
 long a2)

INTERNALgetAstId

protected static int INTERNALgetAstId(long a0,
 long a1)

INTERNALgetAstHash

protected static int INTERNALgetAstHash(long a0,
 long a1)

INTERNALgetSort

protected static long INTERNALgetSort(long a0,
 long a1)

INTERNALisWellSorted

protected static boolean INTERNALisWellSorted(long a0,
 long a1)

INTERNALgetBoolValue

protected static int INTERNALgetBoolValue(long a0,
 long a1)

INTERNALgetAstKind

protected static int INTERNALgetAstKind(long a0,
 long a1)

INTERNALisApp

protected static boolean INTERNALisApp(long a0,
 long a1)

INTERNALisNumeralAst

protected static boolean INTERNALisNumeralAst(long a0,
 long a1)

INTERNALisAlgebraicNumber

protected static boolean INTERNALisAlgebraicNumber(long a0,
 long a1)

INTERNALtoApp

protected static long INTERNALtoApp(long a0,
 long a1)

INTERNALtoFuncDecl

protected static long INTERNALtoFuncDecl(long a0,
 long a1)

INTERNALgetNumeralString

protected static String INTERNALgetNumeralString(long a0,
 long a1)

INTERNALgetNumeralBinaryString

protected static String INTERNALgetNumeralBinaryString(long a0,
 long a1)

INTERNALgetNumeralDecimalString

protected static String INTERNALgetNumeralDecimalString(long a0,
 long a1,
 int a2)

INTERNALgetNumeralDouble

protected static double INTERNALgetNumeralDouble(long a0,
 long a1)

INTERNALgetNumerator

protected static long INTERNALgetNumerator(long a0,
 long a1)

INTERNALgetDenominator

protected static long INTERNALgetDenominator(long a0,
 long a1)

INTERNALgetNumeralSmall

protected static boolean INTERNALgetNumeralSmall(long a0,
 long a1,
 Native.LongPtr a2,
 Native.LongPtr a3)

INTERNALgetNumeralInt

protected static boolean INTERNALgetNumeralInt(long a0,
 long a1,
 Native.IntPtr a2)

INTERNALgetNumeralUint

protected static boolean INTERNALgetNumeralUint(long a0,
 long a1,
 Native.IntPtr a2)

INTERNALgetNumeralUint64

protected static boolean INTERNALgetNumeralUint64(long a0,
 long a1,
 Native.LongPtr a2)

INTERNALgetNumeralInt64

protected static boolean INTERNALgetNumeralInt64(long a0,
 long a1,
 Native.LongPtr a2)

INTERNALgetNumeralRationalInt64

protected static boolean INTERNALgetNumeralRationalInt64(long a0,
 long a1,
 Native.LongPtr a2,
 Native.LongPtr a3)

INTERNALgetAlgebraicNumberLower

protected static long INTERNALgetAlgebraicNumberLower(long a0,
 long a1,
 int a2)

INTERNALgetAlgebraicNumberUpper

protected static long INTERNALgetAlgebraicNumberUpper(long a0,
 long a1,
 int a2)

INTERNALpatternToAst

protected static long INTERNALpatternToAst(long a0,
 long a1)

INTERNALgetPatternNumTerms

protected static int INTERNALgetPatternNumTerms(long a0,
 long a1)

INTERNALgetPattern

protected static long INTERNALgetPattern(long a0,
 long a1,
 int a2)

INTERNALgetIndexValue

protected static int INTERNALgetIndexValue(long a0,
 long a1)

INTERNALisQuantifierForall

protected static boolean INTERNALisQuantifierForall(long a0,
 long a1)

INTERNALisQuantifierExists

protected static boolean INTERNALisQuantifierExists(long a0,
 long a1)

INTERNALisLambda

protected static boolean INTERNALisLambda(long a0,
 long a1)

INTERNALgetQuantifierWeight

protected static int INTERNALgetQuantifierWeight(long a0,
 long a1)

INTERNALgetQuantifierNumPatterns

protected static int INTERNALgetQuantifierNumPatterns(long a0,
 long a1)

INTERNALgetQuantifierPatternAst

protected static long INTERNALgetQuantifierPatternAst(long a0,
 long a1,
 int a2)

INTERNALgetQuantifierNumNoPatterns

protected static int INTERNALgetQuantifierNumNoPatterns(long a0,
 long a1)

INTERNALgetQuantifierNoPatternAst

protected static long INTERNALgetQuantifierNoPatternAst(long a0,
 long a1,
 int a2)

INTERNALgetQuantifierNumBound

protected static int INTERNALgetQuantifierNumBound(long a0,
 long a1)

INTERNALgetQuantifierBoundName

protected static long INTERNALgetQuantifierBoundName(long a0,
 long a1,
 int a2)

INTERNALgetQuantifierBoundSort

protected static long INTERNALgetQuantifierBoundSort(long a0,
 long a1,
 int a2)

INTERNALgetQuantifierBody

protected static long INTERNALgetQuantifierBody(long a0,
 long a1)

INTERNALsimplify

protected static long INTERNALsimplify(long a0,
 long a1)

INTERNALsimplifyEx

protected static long INTERNALsimplifyEx(long a0,
 long a1,
 long a2)

INTERNALsimplifyGetHelp

protected static String INTERNALsimplifyGetHelp(long a0)

INTERNALsimplifyGetParamDescrs

protected static long INTERNALsimplifyGetParamDescrs(long a0)

INTERNALupdateTerm

protected static long INTERNALupdateTerm(long a0,
 long a1,
 int a2,
 long[] a3)

INTERNALsubstitute

protected static long INTERNALsubstitute(long a0,
 long a1,
 int a2,
 long[] a3,
 long[] a4)

INTERNALsubstituteVars

protected static long INTERNALsubstituteVars(long a0,
 long a1,
 int a2,
 long[] a3)

INTERNALtranslate

protected static long INTERNALtranslate(long a0,
 long a1,
 long a2)

INTERNALmkModel

protected static long INTERNALmkModel(long a0)

INTERNALmodelIncRef

protected static void INTERNALmodelIncRef(long a0,
 long a1)

INTERNALmodelDecRef

protected static void INTERNALmodelDecRef(long a0,
 long a1)

INTERNALmodelEval

protected static boolean INTERNALmodelEval(long a0,
 long a1,
 long a2,
 boolean a3,
 Native.LongPtr a4)

INTERNALmodelGetConstInterp

protected static long INTERNALmodelGetConstInterp(long a0,
 long a1,
 long a2)

INTERNALmodelHasInterp

protected static boolean INTERNALmodelHasInterp(long a0,
 long a1,
 long a2)

INTERNALmodelGetFuncInterp

protected static long INTERNALmodelGetFuncInterp(long a0,
 long a1,
 long a2)

INTERNALmodelGetNumConsts

protected static int INTERNALmodelGetNumConsts(long a0,
 long a1)

INTERNALmodelGetConstDecl

protected static long INTERNALmodelGetConstDecl(long a0,
 long a1,
 int a2)

INTERNALmodelGetNumFuncs

protected static int INTERNALmodelGetNumFuncs(long a0,
 long a1)

INTERNALmodelGetFuncDecl

protected static long INTERNALmodelGetFuncDecl(long a0,
 long a1,
 int a2)

INTERNALmodelGetNumSorts

protected static int INTERNALmodelGetNumSorts(long a0,
 long a1)

INTERNALmodelGetSort

protected static long INTERNALmodelGetSort(long a0,
 long a1,
 int a2)

INTERNALmodelGetSortUniverse

protected static long INTERNALmodelGetSortUniverse(long a0,
 long a1,
 long a2)

INTERNALmodelTranslate

protected static long INTERNALmodelTranslate(long a0,
 long a1,
 long a2)

INTERNALisAsArray

protected static boolean INTERNALisAsArray(long a0,
 long a1)

INTERNALgetAsArrayFuncDecl

protected static long INTERNALgetAsArrayFuncDecl(long a0,
 long a1)

INTERNALaddFuncInterp

protected static long INTERNALaddFuncInterp(long a0,
 long a1,
 long a2,
 long a3)

INTERNALaddConstInterp

protected static void INTERNALaddConstInterp(long a0,
 long a1,
 long a2,
 long a3)

INTERNALfuncInterpIncRef

protected static void INTERNALfuncInterpIncRef(long a0,
 long a1)

INTERNALfuncInterpDecRef

protected static void INTERNALfuncInterpDecRef(long a0,
 long a1)

INTERNALfuncInterpGetNumEntries

protected static int INTERNALfuncInterpGetNumEntries(long a0,
 long a1)

INTERNALfuncInterpGetEntry

protected static long INTERNALfuncInterpGetEntry(long a0,
 long a1,
 int a2)

INTERNALfuncInterpGetElse

protected static long INTERNALfuncInterpGetElse(long a0,
 long a1)

INTERNALfuncInterpSetElse

protected static void INTERNALfuncInterpSetElse(long a0,
 long a1,
 long a2)

INTERNALfuncInterpGetArity

protected static int INTERNALfuncInterpGetArity(long a0,
 long a1)

INTERNALfuncInterpAddEntry

protected static void INTERNALfuncInterpAddEntry(long a0,
 long a1,
 long a2,
 long a3)

INTERNALfuncEntryIncRef

protected static void INTERNALfuncEntryIncRef(long a0,
 long a1)

INTERNALfuncEntryDecRef

protected static void INTERNALfuncEntryDecRef(long a0,
 long a1)

INTERNALfuncEntryGetValue

protected static long INTERNALfuncEntryGetValue(long a0,
 long a1)

INTERNALfuncEntryGetNumArgs

protected static int INTERNALfuncEntryGetNumArgs(long a0,
 long a1)

INTERNALfuncEntryGetArg

protected static long INTERNALfuncEntryGetArg(long a0,
 long a1,
 int a2)

INTERNALopenLog

protected static int INTERNALopenLog(String a0)

INTERNALappendLog

protected static void INTERNALappendLog(String a0)

INTERNALcloseLog

protected static void INTERNALcloseLog()

INTERNALtoggleWarningMessages

protected static void INTERNALtoggleWarningMessages(boolean a0)

INTERNALsetAstPrintMode

protected static void INTERNALsetAstPrintMode(long a0,
 int a1)

INTERNALastToString

protected static String INTERNALastToString(long a0,
 long a1)

INTERNALpatternToString

protected static String INTERNALpatternToString(long a0,
 long a1)

INTERNALsortToString

protected static String INTERNALsortToString(long a0,
 long a1)

INTERNALfuncDeclToString

protected static String INTERNALfuncDeclToString(long a0,
 long a1)

INTERNALmodelToString

protected static String INTERNALmodelToString(long a0,
 long a1)

INTERNALbenchmarkToSmtlibString

protected static String INTERNALbenchmarkToSmtlibString(long a0,
 String a1,
 String a2,
 String a3,
 String a4,
 int a5,
 long[] a6,
 long a7)

INTERNALparseSmtlib2String

protected static long INTERNALparseSmtlib2String(long a0,
 String a1,
 int a2,
 long[] a3,
 long[] a4,
 int a5,
 long[] a6,
 long[] a7)

INTERNALparseSmtlib2File

protected static long INTERNALparseSmtlib2File(long a0,
 String a1,
 int a2,
 long[] a3,
 long[] a4,
 int a5,
 long[] a6,
 long[] a7)

INTERNALevalSmtlib2String

protected static String INTERNALevalSmtlib2String(long a0,
 String a1)

INTERNALgetErrorCode

protected static int INTERNALgetErrorCode(long a0)

INTERNALsetError

protected static void INTERNALsetError(long a0,
 int a1)

INTERNALgetErrorMsg

protected static String INTERNALgetErrorMsg(long a0,
 int a1)

INTERNALgetVersion

protected static void INTERNALgetVersion(Native.IntPtr a0,
 Native.IntPtr a1,
 Native.IntPtr a2,
 Native.IntPtr a3)

INTERNALgetFullVersion

protected static String INTERNALgetFullVersion()

INTERNALenableTrace

protected static void INTERNALenableTrace(String a0)

INTERNALdisableTrace

protected static void INTERNALdisableTrace(String a0)

INTERNALresetMemory

protected static void INTERNALresetMemory()

INTERNALfinalizeMemory

protected static void INTERNALfinalizeMemory()

INTERNALmkGoal

protected static long INTERNALmkGoal(long a0,
 boolean a1,
 boolean a2,
 boolean a3)

INTERNALgoalIncRef

protected static void INTERNALgoalIncRef(long a0,
 long a1)

INTERNALgoalDecRef

protected static void INTERNALgoalDecRef(long a0,
 long a1)

INTERNALgoalPrecision

protected static int INTERNALgoalPrecision(long a0,
 long a1)

INTERNALgoalAssert

protected static void INTERNALgoalAssert(long a0,
 long a1,
 long a2)

INTERNALgoalInconsistent

protected static boolean INTERNALgoalInconsistent(long a0,
 long a1)

INTERNALgoalDepth

protected static int INTERNALgoalDepth(long a0,
 long a1)

INTERNALgoalReset

protected static void INTERNALgoalReset(long a0,
 long a1)

INTERNALgoalSize

protected static int INTERNALgoalSize(long a0,
 long a1)

INTERNALgoalFormula

protected static long INTERNALgoalFormula(long a0,
 long a1,
 int a2)

INTERNALgoalNumExprs

protected static int INTERNALgoalNumExprs(long a0,
 long a1)

INTERNALgoalIsDecidedSat

protected static boolean INTERNALgoalIsDecidedSat(long a0,
 long a1)

INTERNALgoalIsDecidedUnsat

protected static boolean INTERNALgoalIsDecidedUnsat(long a0,
 long a1)

INTERNALgoalTranslate

protected static long INTERNALgoalTranslate(long a0,
 long a1,
 long a2)

INTERNALgoalConvertModel

protected static long INTERNALgoalConvertModel(long a0,
 long a1,
 long a2)

INTERNALgoalToString

protected static String INTERNALgoalToString(long a0,
 long a1)

INTERNALgoalToDimacsString

protected static String INTERNALgoalToDimacsString(long a0,
 long a1,
 boolean a2)

INTERNALmkTactic

protected static long INTERNALmkTactic(long a0,
 String a1)

INTERNALtacticIncRef

protected static void INTERNALtacticIncRef(long a0,
 long a1)

INTERNALtacticDecRef

protected static void INTERNALtacticDecRef(long a0,
 long a1)

INTERNALmkProbe

protected static long INTERNALmkProbe(long a0,
 String a1)

INTERNALprobeIncRef

protected static void INTERNALprobeIncRef(long a0,
 long a1)

INTERNALprobeDecRef

protected static void INTERNALprobeDecRef(long a0,
 long a1)

INTERNALtacticAndThen

protected static long INTERNALtacticAndThen(long a0,
 long a1,
 long a2)

INTERNALtacticOrElse

protected static long INTERNALtacticOrElse(long a0,
 long a1,
 long a2)

INTERNALtacticParOr

protected static long INTERNALtacticParOr(long a0,
 int a1,
 long[] a2)

INTERNALtacticParAndThen

protected static long INTERNALtacticParAndThen(long a0,
 long a1,
 long a2)

INTERNALtacticTryFor

protected static long INTERNALtacticTryFor(long a0,
 long a1,
 int a2)

INTERNALtacticWhen

protected static long INTERNALtacticWhen(long a0,
 long a1,
 long a2)

INTERNALtacticCond

protected static long INTERNALtacticCond(long a0,
 long a1,
 long a2,
 long a3)

INTERNALtacticRepeat

protected static long INTERNALtacticRepeat(long a0,
 long a1,
 int a2)

INTERNALtacticSkip

protected static long INTERNALtacticSkip(long a0)

INTERNALtacticFail

protected static long INTERNALtacticFail(long a0)

INTERNALtacticFailIf

protected static long INTERNALtacticFailIf(long a0,
 long a1)

INTERNALtacticFailIfNotDecided

protected static long INTERNALtacticFailIfNotDecided(long a0)

INTERNALtacticUsingParams

protected static long INTERNALtacticUsingParams(long a0,
 long a1,
 long a2)

INTERNALprobeConst

protected static long INTERNALprobeConst(long a0,
 double a1)

INTERNALprobeLt

protected static long INTERNALprobeLt(long a0,
 long a1,
 long a2)

INTERNALprobeGt

protected static long INTERNALprobeGt(long a0,
 long a1,
 long a2)

INTERNALprobeLe

protected static long INTERNALprobeLe(long a0,
 long a1,
 long a2)

INTERNALprobeGe

protected static long INTERNALprobeGe(long a0,
 long a1,
 long a2)

INTERNALprobeEq

protected static long INTERNALprobeEq(long a0,
 long a1,
 long a2)

INTERNALprobeAnd

protected static long INTERNALprobeAnd(long a0,
 long a1,
 long a2)

INTERNALprobeOr

protected static long INTERNALprobeOr(long a0,
 long a1,
 long a2)

INTERNALprobeNot

protected static long INTERNALprobeNot(long a0,
 long a1)

INTERNALgetNumTactics

protected static int INTERNALgetNumTactics(long a0)

INTERNALgetTacticName

protected static String INTERNALgetTacticName(long a0,
 int a1)

INTERNALgetNumProbes

protected static int INTERNALgetNumProbes(long a0)

INTERNALgetProbeName

protected static String INTERNALgetProbeName(long a0,
 int a1)

INTERNALtacticGetHelp

protected static String INTERNALtacticGetHelp(long a0,
 long a1)

INTERNALtacticGetParamDescrs

protected static long INTERNALtacticGetParamDescrs(long a0,
 long a1)

INTERNALtacticGetDescr

protected static String INTERNALtacticGetDescr(long a0,
 String a1)

INTERNALprobeGetDescr

protected static String INTERNALprobeGetDescr(long a0,
 String a1)

INTERNALprobeApply

protected static double INTERNALprobeApply(long a0,
 long a1,
 long a2)

INTERNALtacticApply

protected static long INTERNALtacticApply(long a0,
 long a1,
 long a2)

INTERNALtacticApplyEx

protected static long INTERNALtacticApplyEx(long a0,
 long a1,
 long a2,
 long a3)

INTERNALapplyResultIncRef

protected static void INTERNALapplyResultIncRef(long a0,
 long a1)

INTERNALapplyResultDecRef

protected static void INTERNALapplyResultDecRef(long a0,
 long a1)

INTERNALapplyResultToString

protected static String INTERNALapplyResultToString(long a0,
 long a1)

INTERNALapplyResultGetNumSubgoals

protected static int INTERNALapplyResultGetNumSubgoals(long a0,
 long a1)

INTERNALapplyResultGetSubgoal

protected static long INTERNALapplyResultGetSubgoal(long a0,
 long a1,
 int a2)

INTERNALmkSolver

protected static long INTERNALmkSolver(long a0)

INTERNALmkSimpleSolver

protected static long INTERNALmkSimpleSolver(long a0)

INTERNALmkSolverForLogic

protected static long INTERNALmkSolverForLogic(long a0,
 long a1)

INTERNALmkSolverFromTactic

protected static long INTERNALmkSolverFromTactic(long a0,
 long a1)

INTERNALsolverTranslate

protected static long INTERNALsolverTranslate(long a0,
 long a1,
 long a2)

INTERNALsolverImportModelConverter

protected static void INTERNALsolverImportModelConverter(long a0,
 long a1,
 long a2)

INTERNALsolverGetHelp

protected static String INTERNALsolverGetHelp(long a0,
 long a1)

INTERNALsolverGetParamDescrs

protected static long INTERNALsolverGetParamDescrs(long a0,
 long a1)

INTERNALsolverSetParams

protected static void INTERNALsolverSetParams(long a0,
 long a1,
 long a2)

INTERNALsolverIncRef

protected static void INTERNALsolverIncRef(long a0,
 long a1)

INTERNALsolverDecRef

protected static void INTERNALsolverDecRef(long a0,
 long a1)

INTERNALsolverInterrupt

protected static void INTERNALsolverInterrupt(long a0,
 long a1)

INTERNALsolverPush

protected static void INTERNALsolverPush(long a0,
 long a1)

INTERNALsolverPop

protected static void INTERNALsolverPop(long a0,
 long a1,
 int a2)

INTERNALsolverReset

protected static void INTERNALsolverReset(long a0,
 long a1)

INTERNALsolverGetNumScopes

protected static int INTERNALsolverGetNumScopes(long a0,
 long a1)

INTERNALsolverAssert

protected static void INTERNALsolverAssert(long a0,
 long a1,
 long a2)

INTERNALsolverAssertAndTrack

protected static void INTERNALsolverAssertAndTrack(long a0,
 long a1,
 long a2,
 long a3)

INTERNALsolverFromFile

protected static void INTERNALsolverFromFile(long a0,
 long a1,
 String a2)

INTERNALsolverFromString

protected static void INTERNALsolverFromString(long a0,
 long a1,
 String a2)

INTERNALsolverGetAssertions

protected static long INTERNALsolverGetAssertions(long a0,
 long a1)

INTERNALsolverGetUnits

protected static long INTERNALsolverGetUnits(long a0,
 long a1)

INTERNALsolverGetTrail

protected static long INTERNALsolverGetTrail(long a0,
 long a1)

INTERNALsolverGetNonUnits

protected static long INTERNALsolverGetNonUnits(long a0,
 long a1)

INTERNALsolverGetLevels

protected static void INTERNALsolverGetLevels(long a0,
 long a1,
 long a2,
 int a3,
 int[] a4)

INTERNALsolverPropagateDeclare

protected static long INTERNALsolverPropagateDeclare(long a0,
 long a1,
 int a2,
 long[] a3,
 long a4)

INTERNALsolverPropagateRegister

protected static void INTERNALsolverPropagateRegister(long a0,
 long a1,
 long a2)

INTERNALsolverPropagateRegisterCb

protected static void INTERNALsolverPropagateRegisterCb(long a0,
 long a1,
 long a2)

INTERNALsolverPropagateConsequence

protected static void INTERNALsolverPropagateConsequence(long a0,
 long a1,
 int a2,
 long[] a3,
 int a4,
 long[] a5,
 long[] a6,
 long a7)

INTERNALsolverCheck

protected static int INTERNALsolverCheck(long a0,
 long a1)

INTERNALsolverCheckAssumptions

protected static int INTERNALsolverCheckAssumptions(long a0,
 long a1,
 int a2,
 long[] a3)

INTERNALgetImpliedEqualities

protected static int INTERNALgetImpliedEqualities(long a0,
 long a1,
 int a2,
 long[] a3,
 int[] a4)

INTERNALsolverGetConsequences

protected static int INTERNALsolverGetConsequences(long a0,
 long a1,
 long a2,
 long a3,
 long a4)

INTERNALsolverCube

protected static long INTERNALsolverCube(long a0,
 long a1,
 long a2,
 int a3)

INTERNALsolverGetModel

protected static long INTERNALsolverGetModel(long a0,
 long a1)

INTERNALsolverGetProof

protected static long INTERNALsolverGetProof(long a0,
 long a1)

INTERNALsolverGetUnsatCore

protected static long INTERNALsolverGetUnsatCore(long a0,
 long a1)

INTERNALsolverGetReasonUnknown

protected static String INTERNALsolverGetReasonUnknown(long a0,
 long a1)

INTERNALsolverGetStatistics

protected static long INTERNALsolverGetStatistics(long a0,
 long a1)

INTERNALsolverToString

protected static String INTERNALsolverToString(long a0,
 long a1)

INTERNALsolverToDimacsString

protected static String INTERNALsolverToDimacsString(long a0,
 long a1,
 boolean a2)

INTERNALstatsToString

protected static String INTERNALstatsToString(long a0,
 long a1)

INTERNALstatsIncRef

protected static void INTERNALstatsIncRef(long a0,
 long a1)

INTERNALstatsDecRef

protected static void INTERNALstatsDecRef(long a0,
 long a1)

INTERNALstatsSize

protected static int INTERNALstatsSize(long a0,
 long a1)

INTERNALstatsGetKey

protected static String INTERNALstatsGetKey(long a0,
 long a1,
 int a2)

INTERNALstatsIsUint

protected static boolean INTERNALstatsIsUint(long a0,
 long a1,
 int a2)

INTERNALstatsIsDouble

protected static boolean INTERNALstatsIsDouble(long a0,
 long a1,
 int a2)

INTERNALstatsGetUintValue

protected static int INTERNALstatsGetUintValue(long a0,
 long a1,
 int a2)

INTERNALstatsGetDoubleValue

protected static double INTERNALstatsGetDoubleValue(long a0,
 long a1,
 int a2)

INTERNALgetEstimatedAllocSize

protected static long INTERNALgetEstimatedAllocSize()

INTERNALmkAstVector

protected static long INTERNALmkAstVector(long a0)

INTERNALastVectorIncRef

protected static void INTERNALastVectorIncRef(long a0,
 long a1)

INTERNALastVectorDecRef

protected static void INTERNALastVectorDecRef(long a0,
 long a1)

INTERNALastVectorSize

protected static int INTERNALastVectorSize(long a0,
 long a1)

INTERNALastVectorGet

protected static long INTERNALastVectorGet(long a0,
 long a1,
 int a2)

INTERNALastVectorSet

protected static void INTERNALastVectorSet(long a0,
 long a1,
 int a2,
 long a3)

INTERNALastVectorResize

protected static void INTERNALastVectorResize(long a0,
 long a1,
 int a2)

INTERNALastVectorPush

protected static void INTERNALastVectorPush(long a0,
 long a1,
 long a2)

INTERNALastVectorTranslate

protected static long INTERNALastVectorTranslate(long a0,
 long a1,
 long a2)

INTERNALastVectorToString

protected static String INTERNALastVectorToString(long a0,
 long a1)

INTERNALmkAstMap

protected static long INTERNALmkAstMap(long a0)

INTERNALastMapIncRef

protected static void INTERNALastMapIncRef(long a0,
 long a1)

INTERNALastMapDecRef

protected static void INTERNALastMapDecRef(long a0,
 long a1)

INTERNALastMapContains

protected static boolean INTERNALastMapContains(long a0,
 long a1,
 long a2)

INTERNALastMapFind

protected static long INTERNALastMapFind(long a0,
 long a1,
 long a2)

INTERNALastMapInsert

protected static void INTERNALastMapInsert(long a0,
 long a1,
 long a2,
 long a3)

INTERNALastMapErase

protected static void INTERNALastMapErase(long a0,
 long a1,
 long a2)

INTERNALastMapReset

protected static void INTERNALastMapReset(long a0,
 long a1)

INTERNALastMapSize

protected static int INTERNALastMapSize(long a0,
 long a1)

INTERNALastMapKeys

protected static long INTERNALastMapKeys(long a0,
 long a1)

INTERNALastMapToString

protected static String INTERNALastMapToString(long a0,
 long a1)

INTERNALalgebraicIsValue

protected static boolean INTERNALalgebraicIsValue(long a0,
 long a1)

INTERNALalgebraicIsPos

protected static boolean INTERNALalgebraicIsPos(long a0,
 long a1)

INTERNALalgebraicIsNeg

protected static boolean INTERNALalgebraicIsNeg(long a0,
 long a1)

INTERNALalgebraicIsZero

protected static boolean INTERNALalgebraicIsZero(long a0,
 long a1)

INTERNALalgebraicSign

protected static int INTERNALalgebraicSign(long a0,
 long a1)

INTERNALalgebraicAdd

protected static long INTERNALalgebraicAdd(long a0,
 long a1,
 long a2)

INTERNALalgebraicSub

protected static long INTERNALalgebraicSub(long a0,
 long a1,
 long a2)

INTERNALalgebraicMul

protected static long INTERNALalgebraicMul(long a0,
 long a1,
 long a2)

INTERNALalgebraicDiv

protected static long INTERNALalgebraicDiv(long a0,
 long a1,
 long a2)

INTERNALalgebraicRoot

protected static long INTERNALalgebraicRoot(long a0,
 long a1,
 int a2)

INTERNALalgebraicPower

protected static long INTERNALalgebraicPower(long a0,
 long a1,
 int a2)

INTERNALalgebraicLt

protected static boolean INTERNALalgebraicLt(long a0,
 long a1,
 long a2)

INTERNALalgebraicGt

protected static boolean INTERNALalgebraicGt(long a0,
 long a1,
 long a2)

INTERNALalgebraicLe

protected static boolean INTERNALalgebraicLe(long a0,
 long a1,
 long a2)

INTERNALalgebraicGe

protected static boolean INTERNALalgebraicGe(long a0,
 long a1,
 long a2)

INTERNALalgebraicEq

protected static boolean INTERNALalgebraicEq(long a0,
 long a1,
 long a2)

INTERNALalgebraicNeq

protected static boolean INTERNALalgebraicNeq(long a0,
 long a1,
 long a2)

INTERNALalgebraicRoots

protected static long INTERNALalgebraicRoots(long a0,
 long a1,
 int a2,
 long[] a3)

INTERNALalgebraicEval

protected static int INTERNALalgebraicEval(long a0,
 long a1,
 int a2,
 long[] a3)

INTERNALalgebraicGetPoly

protected static long INTERNALalgebraicGetPoly(long a0,
 long a1)

INTERNALalgebraicGetI

protected static int INTERNALalgebraicGetI(long a0,
 long a1)

INTERNALpolynomialSubresultants

protected static long INTERNALpolynomialSubresultants(long a0,
 long a1,
 long a2,
 long a3)

INTERNALrcfDel

protected static void INTERNALrcfDel(long a0,
 long a1)

INTERNALrcfMkRational

protected static long INTERNALrcfMkRational(long a0,
 String a1)

INTERNALrcfMkSmallInt

protected static long INTERNALrcfMkSmallInt(long a0,
 int a1)

INTERNALrcfMkPi

protected static long INTERNALrcfMkPi(long a0)

INTERNALrcfMkE

protected static long INTERNALrcfMkE(long a0)

INTERNALrcfMkInfinitesimal

protected static long INTERNALrcfMkInfinitesimal(long a0)

INTERNALrcfMkRoots

protected static int INTERNALrcfMkRoots(long a0,
 int a1,
 long[] a2,
 long[] a3)

INTERNALrcfAdd

protected static long INTERNALrcfAdd(long a0,
 long a1,
 long a2)

INTERNALrcfSub

protected static long INTERNALrcfSub(long a0,
 long a1,
 long a2)

INTERNALrcfMul

protected static long INTERNALrcfMul(long a0,
 long a1,
 long a2)

INTERNALrcfDiv

protected static long INTERNALrcfDiv(long a0,
 long a1,
 long a2)

INTERNALrcfNeg

protected static long INTERNALrcfNeg(long a0,
 long a1)

INTERNALrcfInv

protected static long INTERNALrcfInv(long a0,
 long a1)

INTERNALrcfPower

protected static long INTERNALrcfPower(long a0,
 long a1,
 int a2)

INTERNALrcfLt

protected static boolean INTERNALrcfLt(long a0,
 long a1,
 long a2)

INTERNALrcfGt

protected static boolean INTERNALrcfGt(long a0,
 long a1,
 long a2)

INTERNALrcfLe

protected static boolean INTERNALrcfLe(long a0,
 long a1,
 long a2)

INTERNALrcfGe

protected static boolean INTERNALrcfGe(long a0,
 long a1,
 long a2)

INTERNALrcfEq

protected static boolean INTERNALrcfEq(long a0,
 long a1,
 long a2)

INTERNALrcfNeq

protected static boolean INTERNALrcfNeq(long a0,
 long a1,
 long a2)

INTERNALrcfNumToString

protected static String INTERNALrcfNumToString(long a0,
 long a1,
 boolean a2,
 boolean a3)

INTERNALrcfNumToDecimalString

protected static String INTERNALrcfNumToDecimalString(long a0,
 long a1,
 int a2)

INTERNALrcfGetNumeratorDenominator

protected static void INTERNALrcfGetNumeratorDenominator(long a0,
 long a1,
 Native.LongPtr a2,
 Native.LongPtr a3)

INTERNALmkFixedpoint

protected static long INTERNALmkFixedpoint(long a0)

INTERNALfixedpointIncRef

protected static void INTERNALfixedpointIncRef(long a0,
 long a1)

INTERNALfixedpointDecRef

protected static void INTERNALfixedpointDecRef(long a0,
 long a1)

INTERNALfixedpointAddRule

protected static void INTERNALfixedpointAddRule(long a0,
 long a1,
 long a2,
 long a3)

INTERNALfixedpointAddFact

protected static void INTERNALfixedpointAddFact(long a0,
 long a1,
 long a2,
 int a3,
 int[] a4)

INTERNALfixedpointAssert

protected static void INTERNALfixedpointAssert(long a0,
 long a1,
 long a2)

INTERNALfixedpointQuery

protected static int INTERNALfixedpointQuery(long a0,
 long a1,
 long a2)

INTERNALfixedpointQueryRelations

protected static int INTERNALfixedpointQueryRelations(long a0,
 long a1,
 int a2,
 long[] a3)

INTERNALfixedpointGetAnswer

protected static long INTERNALfixedpointGetAnswer(long a0,
 long a1)

INTERNALfixedpointGetReasonUnknown

protected static String INTERNALfixedpointGetReasonUnknown(long a0,
 long a1)

INTERNALfixedpointUpdateRule

protected static void INTERNALfixedpointUpdateRule(long a0,
 long a1,
 long a2,
 long a3)

INTERNALfixedpointGetNumLevels

protected static int INTERNALfixedpointGetNumLevels(long a0,
 long a1,
 long a2)

INTERNALfixedpointGetCoverDelta

protected static long INTERNALfixedpointGetCoverDelta(long a0,
 long a1,
 int a2,
 long a3)

INTERNALfixedpointAddCover

protected static void INTERNALfixedpointAddCover(long a0,
 long a1,
 int a2,
 long a3,
 long a4)

INTERNALfixedpointGetStatistics

protected static long INTERNALfixedpointGetStatistics(long a0,
 long a1)

INTERNALfixedpointRegisterRelation

protected static void INTERNALfixedpointRegisterRelation(long a0,
 long a1,
 long a2)

INTERNALfixedpointSetPredicateRepresentation

protected static void INTERNALfixedpointSetPredicateRepresentation(long a0,
 long a1,
 long a2,
 int a3,
 long[] a4)

INTERNALfixedpointGetRules

protected static long INTERNALfixedpointGetRules(long a0,
 long a1)

INTERNALfixedpointGetAssertions

protected static long INTERNALfixedpointGetAssertions(long a0,
 long a1)

INTERNALfixedpointSetParams

protected static void INTERNALfixedpointSetParams(long a0,
 long a1,
 long a2)

INTERNALfixedpointGetHelp

protected static String INTERNALfixedpointGetHelp(long a0,
 long a1)

INTERNALfixedpointGetParamDescrs

protected static long INTERNALfixedpointGetParamDescrs(long a0,
 long a1)

INTERNALfixedpointToString

protected static String INTERNALfixedpointToString(long a0,
 long a1,
 int a2,
 long[] a3)

INTERNALfixedpointFromString

protected static long INTERNALfixedpointFromString(long a0,
 long a1,
 String a2)

INTERNALfixedpointFromFile

protected static long INTERNALfixedpointFromFile(long a0,
 long a1,
 String a2)

INTERNALmkOptimize

protected static long INTERNALmkOptimize(long a0)

INTERNALoptimizeIncRef

protected static void INTERNALoptimizeIncRef(long a0,
 long a1)

INTERNALoptimizeDecRef

protected static void INTERNALoptimizeDecRef(long a0,
 long a1)

INTERNALoptimizeAssert

protected static void INTERNALoptimizeAssert(long a0,
 long a1,
 long a2)

INTERNALoptimizeAssertAndTrack

protected static void INTERNALoptimizeAssertAndTrack(long a0,
 long a1,
 long a2,
 long a3)

INTERNALoptimizeAssertSoft

protected static int INTERNALoptimizeAssertSoft(long a0,
 long a1,
 long a2,
 String a3,
 long a4)

INTERNALoptimizeMaximize

protected static int INTERNALoptimizeMaximize(long a0,
 long a1,
 long a2)

INTERNALoptimizeMinimize

protected static int INTERNALoptimizeMinimize(long a0,
 long a1,
 long a2)

INTERNALoptimizePush

protected static void INTERNALoptimizePush(long a0,
 long a1)

INTERNALoptimizePop

protected static void INTERNALoptimizePop(long a0,
 long a1)

INTERNALoptimizeCheck

protected static int INTERNALoptimizeCheck(long a0,
 long a1,
 int a2,
 long[] a3)

INTERNALoptimizeGetReasonUnknown

protected static String INTERNALoptimizeGetReasonUnknown(long a0,
 long a1)

INTERNALoptimizeGetModel

protected static long INTERNALoptimizeGetModel(long a0,
 long a1)

INTERNALoptimizeGetUnsatCore

protected static long INTERNALoptimizeGetUnsatCore(long a0,
 long a1)

INTERNALoptimizeSetParams

protected static void INTERNALoptimizeSetParams(long a0,
 long a1,
 long a2)

INTERNALoptimizeGetParamDescrs

protected static long INTERNALoptimizeGetParamDescrs(long a0,
 long a1)

INTERNALoptimizeGetLower

protected static long INTERNALoptimizeGetLower(long a0,
 long a1,
 int a2)

INTERNALoptimizeGetUpper

protected static long INTERNALoptimizeGetUpper(long a0,
 long a1,
 int a2)

INTERNALoptimizeGetLowerAsVector

protected static long INTERNALoptimizeGetLowerAsVector(long a0,
 long a1,
 int a2)

INTERNALoptimizeGetUpperAsVector

protected static long INTERNALoptimizeGetUpperAsVector(long a0,
 long a1,
 int a2)

INTERNALoptimizeToString

protected static String INTERNALoptimizeToString(long a0,
 long a1)

INTERNALoptimizeFromString

protected static void INTERNALoptimizeFromString(long a0,
 long a1,
 String a2)

INTERNALoptimizeFromFile

protected static void INTERNALoptimizeFromFile(long a0,
 long a1,
 String a2)

INTERNALoptimizeGetHelp

protected static String INTERNALoptimizeGetHelp(long a0,
 long a1)

INTERNALoptimizeGetStatistics

protected static long INTERNALoptimizeGetStatistics(long a0,
 long a1)

INTERNALoptimizeGetAssertions

protected static long INTERNALoptimizeGetAssertions(long a0,
 long a1)

INTERNALoptimizeGetObjectives

protected static long INTERNALoptimizeGetObjectives(long a0,
 long a1)

INTERNALmkFpaRoundingModeSort

protected static long INTERNALmkFpaRoundingModeSort(long a0)

INTERNALmkFpaRoundNearestTiesToEven

protected static long INTERNALmkFpaRoundNearestTiesToEven(long a0)

INTERNALmkFpaRne

protected static long INTERNALmkFpaRne(long a0)

INTERNALmkFpaRoundNearestTiesToAway

protected static long INTERNALmkFpaRoundNearestTiesToAway(long a0)

INTERNALmkFpaRna

protected static long INTERNALmkFpaRna(long a0)

INTERNALmkFpaRoundTowardPositive

protected static long INTERNALmkFpaRoundTowardPositive(long a0)

INTERNALmkFpaRtp

protected static long INTERNALmkFpaRtp(long a0)

INTERNALmkFpaRoundTowardNegative

protected static long INTERNALmkFpaRoundTowardNegative(long a0)

INTERNALmkFpaRtn

protected static long INTERNALmkFpaRtn(long a0)

INTERNALmkFpaRoundTowardZero

protected static long INTERNALmkFpaRoundTowardZero(long a0)

INTERNALmkFpaRtz

protected static long INTERNALmkFpaRtz(long a0)

INTERNALmkFpaSort

protected static long INTERNALmkFpaSort(long a0,
 int a1,
 int a2)

INTERNALmkFpaSortHalf

protected static long INTERNALmkFpaSortHalf(long a0)

INTERNALmkFpaSort16

protected static long INTERNALmkFpaSort16(long a0)

INTERNALmkFpaSortSingle

protected static long INTERNALmkFpaSortSingle(long a0)

INTERNALmkFpaSort32

protected static long INTERNALmkFpaSort32(long a0)

INTERNALmkFpaSortDouble

protected static long INTERNALmkFpaSortDouble(long a0)

INTERNALmkFpaSort64

protected static long INTERNALmkFpaSort64(long a0)

INTERNALmkFpaSortQuadruple

protected static long INTERNALmkFpaSortQuadruple(long a0)

INTERNALmkFpaSort128

protected static long INTERNALmkFpaSort128(long a0)

INTERNALmkFpaNan

protected static long INTERNALmkFpaNan(long a0,
 long a1)

INTERNALmkFpaInf

protected static long INTERNALmkFpaInf(long a0,
 long a1,
 boolean a2)

INTERNALmkFpaZero

protected static long INTERNALmkFpaZero(long a0,
 long a1,
 boolean a2)

INTERNALmkFpaFp

protected static long INTERNALmkFpaFp(long a0,
 long a1,
 long a2,
 long a3)

INTERNALmkFpaNumeralFloat

protected static long INTERNALmkFpaNumeralFloat(long a0,
 float a1,
 long a2)

INTERNALmkFpaNumeralDouble

protected static long INTERNALmkFpaNumeralDouble(long a0,
 double a1,
 long a2)

INTERNALmkFpaNumeralInt

protected static long INTERNALmkFpaNumeralInt(long a0,
 int a1,
 long a2)

INTERNALmkFpaNumeralIntUint

protected static long INTERNALmkFpaNumeralIntUint(long a0,
 boolean a1,
 int a2,
 int a3,
 long a4)

INTERNALmkFpaNumeralInt64Uint64

protected static long INTERNALmkFpaNumeralInt64Uint64(long a0,
 boolean a1,
 long a2,
 long a3,
 long a4)

INTERNALmkFpaAbs

protected static long INTERNALmkFpaAbs(long a0,
 long a1)

INTERNALmkFpaNeg

protected static long INTERNALmkFpaNeg(long a0,
 long a1)

INTERNALmkFpaAdd

protected static long INTERNALmkFpaAdd(long a0,
 long a1,
 long a2,
 long a3)

INTERNALmkFpaSub

protected static long INTERNALmkFpaSub(long a0,
 long a1,
 long a2,
 long a3)

INTERNALmkFpaMul

protected static long INTERNALmkFpaMul(long a0,
 long a1,
 long a2,
 long a3)

INTERNALmkFpaDiv

protected static long INTERNALmkFpaDiv(long a0,
 long a1,
 long a2,
 long a3)

INTERNALmkFpaFma

protected static long INTERNALmkFpaFma(long a0,
 long a1,
 long a2,
 long a3,
 long a4)

INTERNALmkFpaSqrt

protected static long INTERNALmkFpaSqrt(long a0,
 long a1,
 long a2)

INTERNALmkFpaRem

protected static long INTERNALmkFpaRem(long a0,
 long a1,
 long a2)

INTERNALmkFpaRoundToIntegral

protected static long INTERNALmkFpaRoundToIntegral(long a0,
 long a1,
 long a2)

INTERNALmkFpaMin

protected static long INTERNALmkFpaMin(long a0,
 long a1,
 long a2)

INTERNALmkFpaMax

protected static long INTERNALmkFpaMax(long a0,
 long a1,
 long a2)

INTERNALmkFpaLeq

protected static long INTERNALmkFpaLeq(long a0,
 long a1,
 long a2)

INTERNALmkFpaLt

protected static long INTERNALmkFpaLt(long a0,
 long a1,
 long a2)

INTERNALmkFpaGeq

protected static long INTERNALmkFpaGeq(long a0,
 long a1,
 long a2)

INTERNALmkFpaGt

protected static long INTERNALmkFpaGt(long a0,
 long a1,
 long a2)

INTERNALmkFpaEq

protected static long INTERNALmkFpaEq(long a0,
 long a1,
 long a2)

INTERNALmkFpaIsNormal

protected static long INTERNALmkFpaIsNormal(long a0,
 long a1)

INTERNALmkFpaIsSubnormal

protected static long INTERNALmkFpaIsSubnormal(long a0,
 long a1)

INTERNALmkFpaIsZero

protected static long INTERNALmkFpaIsZero(long a0,
 long a1)

INTERNALmkFpaIsInfinite

protected static long INTERNALmkFpaIsInfinite(long a0,
 long a1)

INTERNALmkFpaIsNan

protected static long INTERNALmkFpaIsNan(long a0,
 long a1)

INTERNALmkFpaIsNegative

protected static long INTERNALmkFpaIsNegative(long a0,
 long a1)

INTERNALmkFpaIsPositive

protected static long INTERNALmkFpaIsPositive(long a0,
 long a1)

INTERNALmkFpaToFpBv

protected static long INTERNALmkFpaToFpBv(long a0,
 long a1,
 long a2)

INTERNALmkFpaToFpFloat

protected static long INTERNALmkFpaToFpFloat(long a0,
 long a1,
 long a2,
 long a3)

INTERNALmkFpaToFpReal

protected static long INTERNALmkFpaToFpReal(long a0,
 long a1,
 long a2,
 long a3)

INTERNALmkFpaToFpSigned

protected static long INTERNALmkFpaToFpSigned(long a0,
 long a1,
 long a2,
 long a3)

INTERNALmkFpaToFpUnsigned

protected static long INTERNALmkFpaToFpUnsigned(long a0,
 long a1,
 long a2,
 long a3)

INTERNALmkFpaToUbv

protected static long INTERNALmkFpaToUbv(long a0,
 long a1,
 long a2,
 int a3)

INTERNALmkFpaToSbv

protected static long INTERNALmkFpaToSbv(long a0,
 long a1,
 long a2,
 int a3)

INTERNALmkFpaToReal

protected static long INTERNALmkFpaToReal(long a0,
 long a1)

INTERNALfpaGetEbits

protected static int INTERNALfpaGetEbits(long a0,
 long a1)

INTERNALfpaGetSbits

protected static int INTERNALfpaGetSbits(long a0,
 long a1)

INTERNALfpaIsNumeralNan

protected static boolean INTERNALfpaIsNumeralNan(long a0,
 long a1)

INTERNALfpaIsNumeralInf

protected static boolean INTERNALfpaIsNumeralInf(long a0,
 long a1)

INTERNALfpaIsNumeralZero

protected static boolean INTERNALfpaIsNumeralZero(long a0,
 long a1)

INTERNALfpaIsNumeralNormal

protected static boolean INTERNALfpaIsNumeralNormal(long a0,
 long a1)

INTERNALfpaIsNumeralSubnormal

protected static boolean INTERNALfpaIsNumeralSubnormal(long a0,
 long a1)

INTERNALfpaIsNumeralPositive

protected static boolean INTERNALfpaIsNumeralPositive(long a0,
 long a1)

INTERNALfpaIsNumeralNegative

protected static boolean INTERNALfpaIsNumeralNegative(long a0,
 long a1)

INTERNALfpaGetNumeralSignBv

protected static long INTERNALfpaGetNumeralSignBv(long a0,
 long a1)

INTERNALfpaGetNumeralSignificandBv

protected static long INTERNALfpaGetNumeralSignificandBv(long a0,
 long a1)

INTERNALfpaGetNumeralSign

protected static boolean INTERNALfpaGetNumeralSign(long a0,
 long a1,
 Native.IntPtr a2)

INTERNALfpaGetNumeralSignificandString

protected static String INTERNALfpaGetNumeralSignificandString(long a0,
 long a1)

INTERNALfpaGetNumeralSignificandUint64

protected static boolean INTERNALfpaGetNumeralSignificandUint64(long a0,
 long a1,
 Native.LongPtr a2)

INTERNALfpaGetNumeralExponentString

protected static String INTERNALfpaGetNumeralExponentString(long a0,
 long a1,
 boolean a2)

INTERNALfpaGetNumeralExponentInt64

protected static boolean INTERNALfpaGetNumeralExponentInt64(long a0,
 long a1,
 Native.LongPtr a2,
 boolean a3)

INTERNALfpaGetNumeralExponentBv

protected static long INTERNALfpaGetNumeralExponentBv(long a0,
 long a1,
 boolean a2)

INTERNALmkFpaToIeeeBv

protected static long INTERNALmkFpaToIeeeBv(long a0,
 long a1)

INTERNALmkFpaToFpIntReal

protected static long INTERNALmkFpaToFpIntReal(long a0,
 long a1,
 long a2,
 long a3,
 long a4)

INTERNALfixedpointQueryFromLvl

protected static int INTERNALfixedpointQueryFromLvl(long a0,
 long a1,
 long a2,
 int a3)

INTERNALfixedpointGetGroundSatAnswer

protected static long INTERNALfixedpointGetGroundSatAnswer(long a0,
 long a1)

INTERNALfixedpointGetRulesAlongTrace

protected static long INTERNALfixedpointGetRulesAlongTrace(long a0,
 long a1)

INTERNALfixedpointGetRuleNamesAlongTrace

protected static long INTERNALfixedpointGetRuleNamesAlongTrace(long a0,
 long a1)

INTERNALfixedpointAddInvariant

protected static void INTERNALfixedpointAddInvariant(long a0,
 long a1,
 long a2,
 long a3)

INTERNALfixedpointGetReachable

protected static long INTERNALfixedpointGetReachable(long a0,
 long a1,
 long a2)

INTERNALqeModelProject

protected static long INTERNALqeModelProject(long a0,
 long a1,
 int a2,
 long[] a3,
 long a4)

INTERNALqeModelProjectSkolem

protected static long INTERNALqeModelProjectSkolem(long a0,
 long a1,
 int a2,
 long[] a3,
 long a4,
 long a5)

INTERNALmodelExtrapolate

protected static long INTERNALmodelExtrapolate(long a0,
 long a1,
 long a2)

INTERNALqeLite

protected static long INTERNALqeLite(long a0,
 long a1,
 long a2)

globalParamSet

public static void globalParamSet(String a0,
 String a1)

globalParamResetAll

public static void globalParamResetAll()

globalParamGet

public static boolean globalParamGet(String a0,
 Native.StringPtr a1)

mkConfig

public static long mkConfig()

delConfig

public static void delConfig(long a0)

setParamValue

public static void setParamValue(long a0,
 String a1,
 String a2)

mkContext

public static long mkContext(long a0)
                      throws Z3Exception

Throws:

Z3Exception

mkContextRc

public static long mkContextRc(long a0)
                        throws Z3Exception

Throws:

Z3Exception

delContext

public static void delContext(long a0)
                       throws Z3Exception

Throws:

Z3Exception

incRef

public static void incRef(long a0,
 long a1)
                   throws Z3Exception

Throws:

Z3Exception

decRef

public static void decRef(long a0,
 long a1)
                   throws Z3Exception

Throws:

Z3Exception

updateParamValue

public static void updateParamValue(long a0,
 String a1,
 String a2)
                             throws Z3Exception

Throws:

Z3Exception

interrupt

public static void interrupt(long a0)
                      throws Z3Exception

Throws:

Z3Exception

mkParams

public static long mkParams(long a0)
                     throws Z3Exception

Throws:

Z3Exception

paramsIncRef

public static void paramsIncRef(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

paramsDecRef

public static void paramsDecRef(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

paramsSetBool

public static void paramsSetBool(long a0,
 long a1,
 long a2,
 boolean a3)
                          throws Z3Exception

Throws:

Z3Exception

paramsSetUint

public static void paramsSetUint(long a0,
 long a1,
 long a2,
 int a3)
                          throws Z3Exception

Throws:

Z3Exception

paramsSetDouble

public static void paramsSetDouble(long a0,
 long a1,
 long a2,
 double a3)
                            throws Z3Exception

Throws:

Z3Exception

paramsSetSymbol

public static void paramsSetSymbol(long a0,
 long a1,
 long a2,
 long a3)
                            throws Z3Exception

Throws:

Z3Exception

paramsToString

public static String paramsToString(long a0,
 long a1)
                             throws Z3Exception

Throws:

Z3Exception

paramsValidate

public static void paramsValidate(long a0,
 long a1,
 long a2)
                           throws Z3Exception

Throws:

Z3Exception

paramDescrsIncRef

public static void paramDescrsIncRef(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

paramDescrsDecRef

public static void paramDescrsDecRef(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

paramDescrsGetKind

public static int paramDescrsGetKind(long a0,
 long a1,
 long a2)
                              throws Z3Exception

Throws:

Z3Exception

paramDescrsSize

public static int paramDescrsSize(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

paramDescrsGetName

public static long paramDescrsGetName(long a0,
 long a1,
 int a2)
                               throws Z3Exception

Throws:

Z3Exception

paramDescrsGetDocumentation

public static String paramDescrsGetDocumentation(long a0,
 long a1,
 long a2)
                                          throws Z3Exception

Throws:

Z3Exception

paramDescrsToString

public static String paramDescrsToString(long a0,
 long a1)
                                  throws Z3Exception

Throws:

Z3Exception

mkIntSymbol

public static long mkIntSymbol(long a0,
 int a1)
                        throws Z3Exception

Throws:

Z3Exception

mkStringSymbol

public static long mkStringSymbol(long a0,
 String a1)
                           throws Z3Exception

Throws:

Z3Exception

mkUninterpretedSort

public static long mkUninterpretedSort(long a0,
 long a1)
                                throws Z3Exception

Throws:

Z3Exception

mkBoolSort

public static long mkBoolSort(long a0)
                       throws Z3Exception

Throws:

Z3Exception

mkIntSort

public static long mkIntSort(long a0)
                      throws Z3Exception

Throws:

Z3Exception

mkRealSort

public static long mkRealSort(long a0)
                       throws Z3Exception

Throws:

Z3Exception

mkBvSort

public static long mkBvSort(long a0,
 int a1)
                     throws Z3Exception

Throws:

Z3Exception

mkFiniteDomainSort

public static long mkFiniteDomainSort(long a0,
 long a1,
 long a2)
                               throws Z3Exception

Throws:

Z3Exception

mkArraySort

public static long mkArraySort(long a0,
 long a1,
 long a2)
                        throws Z3Exception

Throws:

Z3Exception

mkArraySortN

public static long mkArraySortN(long a0,
 int a1,
 long[] a2,
 long a3)
                         throws Z3Exception

Throws:

Z3Exception

mkTupleSort

public static long mkTupleSort(long a0,
 long a1,
 int a2,
 long[] a3,
 long[] a4,
 Native.LongPtr a5,
 long[] a6)
                        throws Z3Exception

Throws:

Z3Exception

mkEnumerationSort

public static long mkEnumerationSort(long a0,
 long a1,
 int a2,
 long[] a3,
 long[] a4,
 long[] a5)
                              throws Z3Exception

Throws:

Z3Exception

mkListSort

public static long mkListSort(long a0,
 long a1,
 long a2,
 Native.LongPtr a3,
 Native.LongPtr a4,
 Native.LongPtr a5,
 Native.LongPtr a6,
 Native.LongPtr a7,
 Native.LongPtr a8)
                       throws Z3Exception

Throws:

Z3Exception

mkConstructor

public static long mkConstructor(long a0,
 long a1,
 long a2,
 int a3,
 long[] a4,
 long[] a5,
 int[] a6)
                          throws Z3Exception

Throws:

Z3Exception

delConstructor

public static void delConstructor(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

mkDatatype

public static long mkDatatype(long a0,
 long a1,
 int a2,
 long[] a3)
                       throws Z3Exception

Throws:

Z3Exception

mkConstructorList

public static long mkConstructorList(long a0,
 int a1,
 long[] a2)
                              throws Z3Exception

Throws:

Z3Exception

delConstructorList

public static void delConstructorList(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

mkDatatypes

public static void mkDatatypes(long a0,
 int a1,
 long[] a2,
 long[] a3,
 long[] a4)
                        throws Z3Exception

Throws:

Z3Exception

queryConstructor

public static void queryConstructor(long a0,
 long a1,
 int a2,
 Native.LongPtr a3,
 Native.LongPtr a4,
 long[] a5)
                             throws Z3Exception

Throws:

Z3Exception

mkFuncDecl

public static long mkFuncDecl(long a0,
 long a1,
 int a2,
 long[] a3,
 long a4)
                       throws Z3Exception

Throws:

Z3Exception

mkApp

public static long mkApp(long a0,
 long a1,
 int a2,
 long[] a3)
                  throws Z3Exception

Throws:

Z3Exception

mkConst

public static long mkConst(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkFreshFuncDecl

public static long mkFreshFuncDecl(long a0,
 String a1,
 int a2,
 long[] a3,
 long a4)
                            throws Z3Exception

Throws:

Z3Exception

mkFreshConst

public static long mkFreshConst(long a0,
 String a1,
 long a2)
                         throws Z3Exception

Throws:

Z3Exception

mkRecFuncDecl

public static long mkRecFuncDecl(long a0,
 long a1,
 int a2,
 long[] a3,
 long a4)
                          throws Z3Exception

Throws:

Z3Exception

addRecDef

public static void addRecDef(long a0,
 long a1,
 int a2,
 long[] a3,
 long a4)
                      throws Z3Exception

Throws:

Z3Exception

mkTrue

public static long mkTrue(long a0)
                   throws Z3Exception

Throws:

Z3Exception

mkFalse

public static long mkFalse(long a0)
                    throws Z3Exception

Throws:

Z3Exception

mkEq

public static long mkEq(long a0,
 long a1,
 long a2)
                 throws Z3Exception

Throws:

Z3Exception

mkDistinct

public static long mkDistinct(long a0,
 int a1,
 long[] a2)
                       throws Z3Exception

Throws:

Z3Exception

mkNot

public static long mkNot(long a0,
 long a1)
                  throws Z3Exception

Throws:

Z3Exception

mkIte

public static long mkIte(long a0,
 long a1,
 long a2,
 long a3)
                  throws Z3Exception

Throws:

Z3Exception

mkIff

public static long mkIff(long a0,
 long a1,
 long a2)
                  throws Z3Exception

Throws:

Z3Exception

mkImplies

public static long mkImplies(long a0,
 long a1,
 long a2)
                      throws Z3Exception

Throws:

Z3Exception

mkXor

public static long mkXor(long a0,
 long a1,
 long a2)
                  throws Z3Exception

Throws:

Z3Exception

mkAnd

public static long mkAnd(long a0,
 int a1,
 long[] a2)
                  throws Z3Exception

Throws:

Z3Exception

mkOr

public static long mkOr(long a0,
 int a1,
 long[] a2)
                 throws Z3Exception

Throws:

Z3Exception

mkAdd

public static long mkAdd(long a0,
 int a1,
 long[] a2)
                  throws Z3Exception

Throws:

Z3Exception

mkMul

public static long mkMul(long a0,
 int a1,
 long[] a2)
                  throws Z3Exception

Throws:

Z3Exception

mkSub

public static long mkSub(long a0,
 int a1,
 long[] a2)
                  throws Z3Exception

Throws:

Z3Exception

mkUnaryMinus

public static long mkUnaryMinus(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

mkDiv

public static long mkDiv(long a0,
 long a1,
 long a2)
                  throws Z3Exception

Throws:

Z3Exception

mkMod

public static long mkMod(long a0,
 long a1,
 long a2)
                  throws Z3Exception

Throws:

Z3Exception

mkRem

public static long mkRem(long a0,
 long a1,
 long a2)
                  throws Z3Exception

Throws:

Z3Exception

mkPower

public static long mkPower(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkLt

public static long mkLt(long a0,
 long a1,
 long a2)
                 throws Z3Exception

Throws:

Z3Exception

mkLe

public static long mkLe(long a0,
 long a1,
 long a2)
                 throws Z3Exception

Throws:

Z3Exception

mkGt

public static long mkGt(long a0,
 long a1,
 long a2)
                 throws Z3Exception

Throws:

Z3Exception

mkGe

public static long mkGe(long a0,
 long a1,
 long a2)
                 throws Z3Exception

Throws:

Z3Exception

mkDivides

public static long mkDivides(long a0,
 long a1,
 long a2)
                      throws Z3Exception

Throws:

Z3Exception

mkInt2real

public static long mkInt2real(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

mkReal2int

public static long mkReal2int(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

mkIsInt

public static long mkIsInt(long a0,
 long a1)
                    throws Z3Exception

Throws:

Z3Exception

mkBvnot

public static long mkBvnot(long a0,
 long a1)
                    throws Z3Exception

Throws:

Z3Exception

mkBvredand

public static long mkBvredand(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

mkBvredor

public static long mkBvredor(long a0,
 long a1)
                      throws Z3Exception

Throws:

Z3Exception

mkBvand

public static long mkBvand(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkBvor

public static long mkBvor(long a0,
 long a1,
 long a2)
                   throws Z3Exception

Throws:

Z3Exception

mkBvxor

public static long mkBvxor(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkBvnand

public static long mkBvnand(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkBvnor

public static long mkBvnor(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkBvxnor

public static long mkBvxnor(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkBvneg

public static long mkBvneg(long a0,
 long a1)
                    throws Z3Exception

Throws:

Z3Exception

mkBvadd

public static long mkBvadd(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkBvsub

public static long mkBvsub(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkBvmul

public static long mkBvmul(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkBvudiv

public static long mkBvudiv(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkBvsdiv

public static long mkBvsdiv(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkBvurem

public static long mkBvurem(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkBvsrem

public static long mkBvsrem(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkBvsmod

public static long mkBvsmod(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkBvult

public static long mkBvult(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkBvslt

public static long mkBvslt(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkBvule

public static long mkBvule(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkBvsle

public static long mkBvsle(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkBvuge

public static long mkBvuge(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkBvsge

public static long mkBvsge(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkBvugt

public static long mkBvugt(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkBvsgt

public static long mkBvsgt(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkConcat

public static long mkConcat(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkExtract

public static long mkExtract(long a0,
 int a1,
 int a2,
 long a3)
                      throws Z3Exception

Throws:

Z3Exception

mkSignExt

public static long mkSignExt(long a0,
 int a1,
 long a2)
                      throws Z3Exception

Throws:

Z3Exception

mkZeroExt

public static long mkZeroExt(long a0,
 int a1,
 long a2)
                      throws Z3Exception

Throws:

Z3Exception

mkRepeat

public static long mkRepeat(long a0,
 int a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkBvshl

public static long mkBvshl(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkBvlshr

public static long mkBvlshr(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkBvashr

public static long mkBvashr(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkRotateLeft

public static long mkRotateLeft(long a0,
 int a1,
 long a2)
                         throws Z3Exception

Throws:

Z3Exception

mkRotateRight

public static long mkRotateRight(long a0,
 int a1,
 long a2)
                          throws Z3Exception

Throws:

Z3Exception

mkExtRotateLeft

public static long mkExtRotateLeft(long a0,
 long a1,
 long a2)
                            throws Z3Exception

Throws:

Z3Exception

mkExtRotateRight

public static long mkExtRotateRight(long a0,
 long a1,
 long a2)
                             throws Z3Exception

Throws:

Z3Exception

mkInt2bv

public static long mkInt2bv(long a0,
 int a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkBv2int

public static long mkBv2int(long a0,
 long a1,
 boolean a2)
                     throws Z3Exception

Throws:

Z3Exception

mkBvaddNoOverflow

public static long mkBvaddNoOverflow(long a0,
 long a1,
 long a2,
 boolean a3)
                              throws Z3Exception

Throws:

Z3Exception

mkBvaddNoUnderflow

public static long mkBvaddNoUnderflow(long a0,
 long a1,
 long a2)
                               throws Z3Exception

Throws:

Z3Exception

mkBvsubNoOverflow

public static long mkBvsubNoOverflow(long a0,
 long a1,
 long a2)
                              throws Z3Exception

Throws:

Z3Exception

mkBvsubNoUnderflow

public static long mkBvsubNoUnderflow(long a0,
 long a1,
 long a2,
 boolean a3)
                               throws Z3Exception

Throws:

Z3Exception

mkBvsdivNoOverflow

public static long mkBvsdivNoOverflow(long a0,
 long a1,
 long a2)
                               throws Z3Exception

Throws:

Z3Exception

mkBvnegNoOverflow

public static long mkBvnegNoOverflow(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

mkBvmulNoOverflow

public static long mkBvmulNoOverflow(long a0,
 long a1,
 long a2,
 boolean a3)
                              throws Z3Exception

Throws:

Z3Exception

mkBvmulNoUnderflow

public static long mkBvmulNoUnderflow(long a0,
 long a1,
 long a2)
                               throws Z3Exception

Throws:

Z3Exception

mkSelect

public static long mkSelect(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkSelectN

public static long mkSelectN(long a0,
 long a1,
 int a2,
 long[] a3)
                      throws Z3Exception

Throws:

Z3Exception

mkStore

public static long mkStore(long a0,
 long a1,
 long a2,
 long a3)
                    throws Z3Exception

Throws:

Z3Exception

mkStoreN

public static long mkStoreN(long a0,
 long a1,
 int a2,
 long[] a3,
 long a4)
                     throws Z3Exception

Throws:

Z3Exception

mkConstArray

public static long mkConstArray(long a0,
 long a1,
 long a2)
                         throws Z3Exception

Throws:

Z3Exception

mkMap

public static long mkMap(long a0,
 long a1,
 int a2,
 long[] a3)
                  throws Z3Exception

Throws:

Z3Exception

mkArrayDefault

public static long mkArrayDefault(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

mkAsArray

public static long mkAsArray(long a0,
 long a1)
                      throws Z3Exception

Throws:

Z3Exception

mkSetHasSize

public static long mkSetHasSize(long a0,
 long a1,
 long a2)
                         throws Z3Exception

Throws:

Z3Exception

mkSetSort

public static long mkSetSort(long a0,
 long a1)
                      throws Z3Exception

Throws:

Z3Exception

mkEmptySet

public static long mkEmptySet(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

mkFullSet

public static long mkFullSet(long a0,
 long a1)
                      throws Z3Exception

Throws:

Z3Exception

mkSetAdd

public static long mkSetAdd(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkSetDel

public static long mkSetDel(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkSetUnion

public static long mkSetUnion(long a0,
 int a1,
 long[] a2)
                       throws Z3Exception

Throws:

Z3Exception

mkSetIntersect

public static long mkSetIntersect(long a0,
 int a1,
 long[] a2)
                           throws Z3Exception

Throws:

Z3Exception

mkSetDifference

public static long mkSetDifference(long a0,
 long a1,
 long a2)
                            throws Z3Exception

Throws:

Z3Exception

mkSetComplement

public static long mkSetComplement(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

mkSetMember

public static long mkSetMember(long a0,
 long a1,
 long a2)
                        throws Z3Exception

Throws:

Z3Exception

mkSetSubset

public static long mkSetSubset(long a0,
 long a1,
 long a2)
                        throws Z3Exception

Throws:

Z3Exception

mkArrayExt

public static long mkArrayExt(long a0,
 long a1,
 long a2)
                       throws Z3Exception

Throws:

Z3Exception

mkNumeral

public static long mkNumeral(long a0,
 String a1,
 long a2)
                      throws Z3Exception

Throws:

Z3Exception

mkReal

public static long mkReal(long a0,
 int a1,
 int a2)
                   throws Z3Exception

Throws:

Z3Exception

mkInt

public static long mkInt(long a0,
 int a1,
 long a2)
                  throws Z3Exception

Throws:

Z3Exception

mkUnsignedInt

public static long mkUnsignedInt(long a0,
 int a1,
 long a2)
                          throws Z3Exception

Throws:

Z3Exception

mkInt64

public static long mkInt64(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkUnsignedInt64

public static long mkUnsignedInt64(long a0,
 long a1,
 long a2)
                            throws Z3Exception

Throws:

Z3Exception

mkBvNumeral

public static long mkBvNumeral(long a0,
 int a1,
 boolean[] a2)
                        throws Z3Exception

Throws:

Z3Exception

mkSeqSort

public static long mkSeqSort(long a0,
 long a1)
                      throws Z3Exception

Throws:

Z3Exception

isSeqSort

public static boolean isSeqSort(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

getSeqSortBasis

public static long getSeqSortBasis(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

mkReSort

public static long mkReSort(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

isReSort

public static boolean isReSort(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

getReSortBasis

public static long getReSortBasis(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

mkStringSort

public static long mkStringSort(long a0)
                         throws Z3Exception

Throws:

Z3Exception

mkCharSort

public static long mkCharSort(long a0)
                       throws Z3Exception

Throws:

Z3Exception

isStringSort

public static boolean isStringSort(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

isCharSort

public static boolean isCharSort(long a0,
 long a1)
                          throws Z3Exception

Throws:

Z3Exception

mkString

public static long mkString(long a0,
 String a1)
                     throws Z3Exception

Throws:

Z3Exception

mkLstring

public static long mkLstring(long a0,
 int a1,
 String a2)
                      throws Z3Exception

Throws:

Z3Exception

mkU32string

public static long mkU32string(long a0,
 int a1,
 int[] a2)
                        throws Z3Exception

Throws:

Z3Exception

isString

public static boolean isString(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

getString

public static String getString(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

getLstring

public static long getLstring(long a0,
 long a1,
 Native.IntPtr a2)
                       throws Z3Exception

Throws:

Z3Exception

getStringLength

public static int getStringLength(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

getStringContents

public static void getStringContents(long a0,
 long a1,
 int a2,
 int[] a3)
                              throws Z3Exception

Throws:

Z3Exception

mkSeqEmpty

public static long mkSeqEmpty(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

mkSeqUnit

public static long mkSeqUnit(long a0,
 long a1)
                      throws Z3Exception

Throws:

Z3Exception

mkSeqConcat

public static long mkSeqConcat(long a0,
 int a1,
 long[] a2)
                        throws Z3Exception

Throws:

Z3Exception

mkSeqPrefix

public static long mkSeqPrefix(long a0,
 long a1,
 long a2)
                        throws Z3Exception

Throws:

Z3Exception

mkSeqSuffix

public static long mkSeqSuffix(long a0,
 long a1,
 long a2)
                        throws Z3Exception

Throws:

Z3Exception

mkSeqContains

public static long mkSeqContains(long a0,
 long a1,
 long a2)
                          throws Z3Exception

Throws:

Z3Exception

mkStrLt

public static long mkStrLt(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkStrLe

public static long mkStrLe(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkSeqExtract

public static long mkSeqExtract(long a0,
 long a1,
 long a2,
 long a3)
                         throws Z3Exception

Throws:

Z3Exception

mkSeqReplace

public static long mkSeqReplace(long a0,
 long a1,
 long a2,
 long a3)
                         throws Z3Exception

Throws:

Z3Exception

mkSeqAt

public static long mkSeqAt(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkSeqNth

public static long mkSeqNth(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkSeqLength

public static long mkSeqLength(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

mkSeqIndex

public static long mkSeqIndex(long a0,
 long a1,
 long a2,
 long a3)
                       throws Z3Exception

Throws:

Z3Exception

mkSeqLastIndex

public static long mkSeqLastIndex(long a0,
 long a1,
 long a2)
                           throws Z3Exception

Throws:

Z3Exception

mkStrToInt

public static long mkStrToInt(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

mkIntToStr

public static long mkIntToStr(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

mkStringToCode

public static long mkStringToCode(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

mkStringFromCode

public static long mkStringFromCode(long a0,
 long a1)
                             throws Z3Exception

Throws:

Z3Exception

mkUbvToStr

public static long mkUbvToStr(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

mkSbvToStr

public static long mkSbvToStr(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

mkSeqToRe

public static long mkSeqToRe(long a0,
 long a1)
                      throws Z3Exception

Throws:

Z3Exception

mkSeqInRe

public static long mkSeqInRe(long a0,
 long a1,
 long a2)
                      throws Z3Exception

Throws:

Z3Exception

mkRePlus

public static long mkRePlus(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

mkReStar

public static long mkReStar(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

mkReOption

public static long mkReOption(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

mkReUnion

public static long mkReUnion(long a0,
 int a1,
 long[] a2)
                      throws Z3Exception

Throws:

Z3Exception

mkReConcat

public static long mkReConcat(long a0,
 int a1,
 long[] a2)
                       throws Z3Exception

Throws:

Z3Exception

mkReRange

public static long mkReRange(long a0,
 long a1,
 long a2)
                      throws Z3Exception

Throws:

Z3Exception

mkReAllchar

public static long mkReAllchar(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

mkReLoop

public static long mkReLoop(long a0,
 long a1,
 int a2,
 int a3)
                     throws Z3Exception

Throws:

Z3Exception

mkRePower

public static long mkRePower(long a0,
 long a1,
 int a2)
                      throws Z3Exception

Throws:

Z3Exception

mkReIntersect

public static long mkReIntersect(long a0,
 int a1,
 long[] a2)
                          throws Z3Exception

Throws:

Z3Exception

mkReComplement

public static long mkReComplement(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

mkReDiff

public static long mkReDiff(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkReEmpty

public static long mkReEmpty(long a0,
 long a1)
                      throws Z3Exception

Throws:

Z3Exception

mkReFull

public static long mkReFull(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

mkChar

public static long mkChar(long a0,
 int a1)
                   throws Z3Exception

Throws:

Z3Exception

mkCharLe

public static long mkCharLe(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkCharToInt

public static long mkCharToInt(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

mkCharToBv

public static long mkCharToBv(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

mkCharFromBv

public static long mkCharFromBv(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

mkCharIsDigit

public static long mkCharIsDigit(long a0,
 long a1)
                          throws Z3Exception

Throws:

Z3Exception

mkLinearOrder

public static long mkLinearOrder(long a0,
 long a1,
 int a2)
                          throws Z3Exception

Throws:

Z3Exception

mkPartialOrder

public static long mkPartialOrder(long a0,
 long a1,
 int a2)
                           throws Z3Exception

Throws:

Z3Exception

mkPiecewiseLinearOrder

public static long mkPiecewiseLinearOrder(long a0,
 long a1,
 int a2)
                                   throws Z3Exception

Throws:

Z3Exception

mkTreeOrder

public static long mkTreeOrder(long a0,
 long a1,
 int a2)
                        throws Z3Exception

Throws:

Z3Exception

mkTransitiveClosure

public static long mkTransitiveClosure(long a0,
 long a1)
                                throws Z3Exception

Throws:

Z3Exception

mkPattern

public static long mkPattern(long a0,
 int a1,
 long[] a2)
                      throws Z3Exception

Throws:

Z3Exception

mkBound

public static long mkBound(long a0,
 int a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkForall

public static long mkForall(long a0,
 int a1,
 int a2,
 long[] a3,
 int a4,
 long[] a5,
 long[] a6,
 long a7)
                     throws Z3Exception

Throws:

Z3Exception

mkExists

public static long mkExists(long a0,
 int a1,
 int a2,
 long[] a3,
 int a4,
 long[] a5,
 long[] a6,
 long a7)
                     throws Z3Exception

Throws:

Z3Exception

mkQuantifier

public static long mkQuantifier(long a0,
 boolean a1,
 int a2,
 int a3,
 long[] a4,
 int a5,
 long[] a6,
 long[] a7,
 long a8)
                         throws Z3Exception

Throws:

Z3Exception

mkQuantifierEx

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

Throws:

Z3Exception

mkForallConst

public static long mkForallConst(long a0,
 int a1,
 int a2,
 long[] a3,
 int a4,
 long[] a5,
 long a6)
                          throws Z3Exception

Throws:

Z3Exception

mkExistsConst

public static long mkExistsConst(long a0,
 int a1,
 int a2,
 long[] a3,
 int a4,
 long[] a5,
 long a6)
                          throws Z3Exception

Throws:

Z3Exception

mkQuantifierConst

public static long mkQuantifierConst(long a0,
 boolean a1,
 int a2,
 int a3,
 long[] a4,
 int a5,
 long[] a6,
 long a7)
                              throws Z3Exception

Throws:

Z3Exception

mkQuantifierConstEx

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

Throws:

Z3Exception

mkLambda

public static long mkLambda(long a0,
 int a1,
 long[] a2,
 long[] a3,
 long a4)
                     throws Z3Exception

Throws:

Z3Exception

mkLambdaConst

public static long mkLambdaConst(long a0,
 int a1,
 long[] a2,
 long a3)
                          throws Z3Exception

Throws:

Z3Exception

getSymbolKind

public static int getSymbolKind(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

getSymbolInt

public static int getSymbolInt(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

getSymbolString

public static String getSymbolString(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

getSortName

public static long getSortName(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

getSortId

public static int getSortId(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

sortToAst

public static long sortToAst(long a0,
 long a1)
                      throws Z3Exception

Throws:

Z3Exception

isEqSort

public static boolean isEqSort(long a0,
 long a1,
 long a2)
                        throws Z3Exception

Throws:

Z3Exception

getSortKind

public static int getSortKind(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

getBvSortSize

public static int getBvSortSize(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

getFiniteDomainSortSize

public static boolean getFiniteDomainSortSize(long a0,
 long a1,
 Native.LongPtr a2)
                                       throws Z3Exception

Throws:

Z3Exception

getArraySortDomain

public static long getArraySortDomain(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

getArraySortDomainN

public static long getArraySortDomainN(long a0,
 long a1,
 int a2)
                                throws Z3Exception

Throws:

Z3Exception

getArraySortRange

public static long getArraySortRange(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

getTupleSortMkDecl

public static long getTupleSortMkDecl(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

getTupleSortNumFields

public static int getTupleSortNumFields(long a0,
 long a1)
                                 throws Z3Exception

Throws:

Z3Exception

getTupleSortFieldDecl

public static long getTupleSortFieldDecl(long a0,
 long a1,
 int a2)
                                  throws Z3Exception

Throws:

Z3Exception

getDatatypeSortNumConstructors

public static int getDatatypeSortNumConstructors(long a0,
 long a1)
                                          throws Z3Exception

Throws:

Z3Exception

getDatatypeSortConstructor

public static long getDatatypeSortConstructor(long a0,
 long a1,
 int a2)
                                       throws Z3Exception

Throws:

Z3Exception

getDatatypeSortRecognizer

public static long getDatatypeSortRecognizer(long a0,
 long a1,
 int a2)
                                      throws Z3Exception

Throws:

Z3Exception

getDatatypeSortConstructorAccessor

public static long getDatatypeSortConstructorAccessor(long a0,
 long a1,
 int a2,
 int a3)
                                               throws Z3Exception

Throws:

Z3Exception

datatypeUpdateField

public static long datatypeUpdateField(long a0,
 long a1,
 long a2,
 long a3)
                                throws Z3Exception

Throws:

Z3Exception

getRelationArity

public static int getRelationArity(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

getRelationColumn

public static long getRelationColumn(long a0,
 long a1,
 int a2)
                              throws Z3Exception

Throws:

Z3Exception

mkAtmost

public static long mkAtmost(long a0,
 int a1,
 long[] a2,
 int a3)
                     throws Z3Exception

Throws:

Z3Exception

mkAtleast

public static long mkAtleast(long a0,
 int a1,
 long[] a2,
 int a3)
                      throws Z3Exception

Throws:

Z3Exception

mkPble

public static long mkPble(long a0,
 int a1,
 long[] a2,
 int[] a3,
 int a4)
                   throws Z3Exception

Throws:

Z3Exception

mkPbge

public static long mkPbge(long a0,
 int a1,
 long[] a2,
 int[] a3,
 int a4)
                   throws Z3Exception

Throws:

Z3Exception

mkPbeq

public static long mkPbeq(long a0,
 int a1,
 long[] a2,
 int[] a3,
 int a4)
                   throws Z3Exception

Throws:

Z3Exception

funcDeclToAst

public static long funcDeclToAst(long a0,
 long a1)
                          throws Z3Exception

Throws:

Z3Exception

isEqFuncDecl

public static boolean isEqFuncDecl(long a0,
 long a1,
 long a2)
                            throws Z3Exception

Throws:

Z3Exception

getFuncDeclId

public static int getFuncDeclId(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

getDeclName

public static long getDeclName(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

getDeclKind

public static int getDeclKind(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

getDomainSize

public static int getDomainSize(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

getArity

public static int getArity(long a0,
 long a1)
                    throws Z3Exception

Throws:

Z3Exception

getDomain

public static long getDomain(long a0,
 long a1,
 int a2)
                      throws Z3Exception

Throws:

Z3Exception

getRange

public static long getRange(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

getDeclNumParameters

public static int getDeclNumParameters(long a0,
 long a1)
                                throws Z3Exception

Throws:

Z3Exception

getDeclParameterKind

public static int getDeclParameterKind(long a0,
 long a1,
 int a2)
                                throws Z3Exception

Throws:

Z3Exception

getDeclIntParameter

public static int getDeclIntParameter(long a0,
 long a1,
 int a2)
                               throws Z3Exception

Throws:

Z3Exception

getDeclDoubleParameter

public static double getDeclDoubleParameter(long a0,
 long a1,
 int a2)
                                     throws Z3Exception

Throws:

Z3Exception

getDeclSymbolParameter

public static long getDeclSymbolParameter(long a0,
 long a1,
 int a2)
                                   throws Z3Exception

Throws:

Z3Exception

getDeclSortParameter

public static long getDeclSortParameter(long a0,
 long a1,
 int a2)
                                 throws Z3Exception

Throws:

Z3Exception

getDeclAstParameter

public static long getDeclAstParameter(long a0,
 long a1,
 int a2)
                                throws Z3Exception

Throws:

Z3Exception

getDeclFuncDeclParameter

public static long getDeclFuncDeclParameter(long a0,
 long a1,
 int a2)
                                     throws Z3Exception

Throws:

Z3Exception

getDeclRationalParameter

public static String getDeclRationalParameter(long a0,
 long a1,
 int a2)
                                       throws Z3Exception

Throws:

Z3Exception

appToAst

public static long appToAst(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

getAppDecl

public static long getAppDecl(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

getAppNumArgs

public static int getAppNumArgs(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

getAppArg

public static long getAppArg(long a0,
 long a1,
 int a2)
                      throws Z3Exception

Throws:

Z3Exception

isEqAst

public static boolean isEqAst(long a0,
 long a1,
 long a2)
                       throws Z3Exception

Throws:

Z3Exception

getAstId

public static int getAstId(long a0,
 long a1)
                    throws Z3Exception

Throws:

Z3Exception

getAstHash

public static int getAstHash(long a0,
 long a1)
                      throws Z3Exception

Throws:

Z3Exception

getSort

public static long getSort(long a0,
 long a1)
                    throws Z3Exception

Throws:

Z3Exception

isWellSorted

public static boolean isWellSorted(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

getBoolValue

public static int getBoolValue(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

getAstKind

public static int getAstKind(long a0,
 long a1)
                      throws Z3Exception

Throws:

Z3Exception

isApp

public static boolean isApp(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

isNumeralAst

public static boolean isNumeralAst(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

isAlgebraicNumber

public static boolean isAlgebraicNumber(long a0,
 long a1)
                                 throws Z3Exception

Throws:

Z3Exception

toApp

public static long toApp(long a0,
 long a1)
                  throws Z3Exception

Throws:

Z3Exception

toFuncDecl

public static long toFuncDecl(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

getNumeralString

public static String getNumeralString(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

getNumeralBinaryString

public static String getNumeralBinaryString(long a0,
 long a1)
                                     throws Z3Exception

Throws:

Z3Exception

getNumeralDecimalString

public static String getNumeralDecimalString(long a0,
 long a1,
 int a2)
                                      throws Z3Exception

Throws:

Z3Exception

getNumeralDouble

public static double getNumeralDouble(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

getNumerator

public static long getNumerator(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

getDenominator

public static long getDenominator(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

getNumeralSmall

public static boolean getNumeralSmall(long a0,
 long a1,
 Native.LongPtr a2,
 Native.LongPtr a3)
                               throws Z3Exception

Throws:

Z3Exception

getNumeralInt

public static boolean getNumeralInt(long a0,
 long a1,
 Native.IntPtr a2)
                             throws Z3Exception

Throws:

Z3Exception

getNumeralUint

public static boolean getNumeralUint(long a0,
 long a1,
 Native.IntPtr a2)
                              throws Z3Exception

Throws:

Z3Exception

getNumeralUint64

public static boolean getNumeralUint64(long a0,
 long a1,
 Native.LongPtr a2)
                                throws Z3Exception

Throws:

Z3Exception

getNumeralInt64

public static boolean getNumeralInt64(long a0,
 long a1,
 Native.LongPtr a2)
                               throws Z3Exception

Throws:

Z3Exception

getNumeralRationalInt64

public static boolean getNumeralRationalInt64(long a0,
 long a1,
 Native.LongPtr a2,
 Native.LongPtr a3)
                                       throws Z3Exception

Throws:

Z3Exception

getAlgebraicNumberLower

public static long getAlgebraicNumberLower(long a0,
 long a1,
 int a2)
                                    throws Z3Exception

Throws:

Z3Exception

getAlgebraicNumberUpper

public static long getAlgebraicNumberUpper(long a0,
 long a1,
 int a2)
                                    throws Z3Exception

Throws:

Z3Exception

patternToAst

public static long patternToAst(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

getPatternNumTerms

public static int getPatternNumTerms(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

getPattern

public static long getPattern(long a0,
 long a1,
 int a2)
                       throws Z3Exception

Throws:

Z3Exception

getIndexValue

public static int getIndexValue(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

isQuantifierForall

public static boolean isQuantifierForall(long a0,
 long a1)
                                  throws Z3Exception

Throws:

Z3Exception

isQuantifierExists

public static boolean isQuantifierExists(long a0,
 long a1)
                                  throws Z3Exception

Throws:

Z3Exception

isLambda

public static boolean isLambda(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

getQuantifierWeight

public static int getQuantifierWeight(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

getQuantifierNumPatterns

public static int getQuantifierNumPatterns(long a0,
 long a1)
                                    throws Z3Exception

Throws:

Z3Exception

getQuantifierPatternAst

public static long getQuantifierPatternAst(long a0,
 long a1,
 int a2)
                                    throws Z3Exception

Throws:

Z3Exception

getQuantifierNumNoPatterns

public static int getQuantifierNumNoPatterns(long a0,
 long a1)
                                      throws Z3Exception

Throws:

Z3Exception

getQuantifierNoPatternAst

public static long getQuantifierNoPatternAst(long a0,
 long a1,
 int a2)
                                      throws Z3Exception

Throws:

Z3Exception

getQuantifierNumBound

public static int getQuantifierNumBound(long a0,
 long a1)
                                 throws Z3Exception

Throws:

Z3Exception

getQuantifierBoundName

public static long getQuantifierBoundName(long a0,
 long a1,
 int a2)
                                   throws Z3Exception

Throws:

Z3Exception

getQuantifierBoundSort

public static long getQuantifierBoundSort(long a0,
 long a1,
 int a2)
                                   throws Z3Exception

Throws:

Z3Exception

getQuantifierBody

public static long getQuantifierBody(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

simplify

public static long simplify(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

simplifyEx

public static long simplifyEx(long a0,
 long a1,
 long a2)
                       throws Z3Exception

Throws:

Z3Exception

simplifyGetHelp

public static String simplifyGetHelp(long a0)
                              throws Z3Exception

Throws:

Z3Exception

simplifyGetParamDescrs

public static long simplifyGetParamDescrs(long a0)
                                   throws Z3Exception

Throws:

Z3Exception

updateTerm

public static long updateTerm(long a0,
 long a1,
 int a2,
 long[] a3)
                       throws Z3Exception

Throws:

Z3Exception

substitute

public static long substitute(long a0,
 long a1,
 int a2,
 long[] a3,
 long[] a4)
                       throws Z3Exception

Throws:

Z3Exception

substituteVars

public static long substituteVars(long a0,
 long a1,
 int a2,
 long[] a3)
                           throws Z3Exception

Throws:

Z3Exception

translate

public static long translate(long a0,
 long a1,
 long a2)
                      throws Z3Exception

Throws:

Z3Exception

mkModel

public static long mkModel(long a0)
                    throws Z3Exception

Throws:

Z3Exception

modelIncRef

public static void modelIncRef(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

modelDecRef

public static void modelDecRef(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

modelEval

public static boolean modelEval(long a0,
 long a1,
 long a2,
 boolean a3,
 Native.LongPtr a4)
                         throws Z3Exception

Throws:

Z3Exception

modelGetConstInterp

public static long modelGetConstInterp(long a0,
 long a1,
 long a2)
                                throws Z3Exception

Throws:

Z3Exception

modelHasInterp

public static boolean modelHasInterp(long a0,
 long a1,
 long a2)
                              throws Z3Exception

Throws:

Z3Exception

modelGetFuncInterp

public static long modelGetFuncInterp(long a0,
 long a1,
 long a2)
                               throws Z3Exception

Throws:

Z3Exception

modelGetNumConsts

public static int modelGetNumConsts(long a0,
 long a1)
                             throws Z3Exception

Throws:

Z3Exception

modelGetConstDecl

public static long modelGetConstDecl(long a0,
 long a1,
 int a2)
                              throws Z3Exception

Throws:

Z3Exception

modelGetNumFuncs

public static int modelGetNumFuncs(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

modelGetFuncDecl

public static long modelGetFuncDecl(long a0,
 long a1,
 int a2)
                             throws Z3Exception

Throws:

Z3Exception

modelGetNumSorts

public static int modelGetNumSorts(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

modelGetSort

public static long modelGetSort(long a0,
 long a1,
 int a2)
                         throws Z3Exception

Throws:

Z3Exception

modelGetSortUniverse

public static long modelGetSortUniverse(long a0,
 long a1,
 long a2)
                                 throws Z3Exception

Throws:

Z3Exception

modelTranslate

public static long modelTranslate(long a0,
 long a1,
 long a2)
                           throws Z3Exception

Throws:

Z3Exception

isAsArray

public static boolean isAsArray(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

getAsArrayFuncDecl

public static long getAsArrayFuncDecl(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

addFuncInterp

public static long addFuncInterp(long a0,
 long a1,
 long a2,
 long a3)
                          throws Z3Exception

Throws:

Z3Exception

addConstInterp

public static void addConstInterp(long a0,
 long a1,
 long a2,
 long a3)
                           throws Z3Exception

Throws:

Z3Exception

funcInterpIncRef

public static void funcInterpIncRef(long a0,
 long a1)
                             throws Z3Exception

Throws:

Z3Exception

funcInterpDecRef

public static void funcInterpDecRef(long a0,
 long a1)
                             throws Z3Exception

Throws:

Z3Exception

funcInterpGetNumEntries

public static int funcInterpGetNumEntries(long a0,
 long a1)
                                   throws Z3Exception

Throws:

Z3Exception

funcInterpGetEntry

public static long funcInterpGetEntry(long a0,
 long a1,
 int a2)
                               throws Z3Exception

Throws:

Z3Exception

funcInterpGetElse

public static long funcInterpGetElse(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

funcInterpSetElse

public static void funcInterpSetElse(long a0,
 long a1,
 long a2)
                              throws Z3Exception

Throws:

Z3Exception

funcInterpGetArity

public static int funcInterpGetArity(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

funcInterpAddEntry

public static void funcInterpAddEntry(long a0,
 long a1,
 long a2,
 long a3)
                               throws Z3Exception

Throws:

Z3Exception

funcEntryIncRef

public static void funcEntryIncRef(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

funcEntryDecRef

public static void funcEntryDecRef(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

funcEntryGetValue

public static long funcEntryGetValue(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

funcEntryGetNumArgs

public static int funcEntryGetNumArgs(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

funcEntryGetArg

public static long funcEntryGetArg(long a0,
 long a1,
 int a2)
                            throws Z3Exception

Throws:

Z3Exception

openLog

public static int openLog(String a0)

appendLog

public static void appendLog(String a0)

closeLog

public static void closeLog()

toggleWarningMessages

public static void toggleWarningMessages(boolean a0)

setAstPrintMode

public static void setAstPrintMode(long a0,
 int a1)
                            throws Z3Exception

Throws:

Z3Exception

astToString

public static String astToString(long a0,
 long a1)
                          throws Z3Exception

Throws:

Z3Exception

patternToString

public static String patternToString(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

sortToString

public static String sortToString(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

funcDeclToString

public static String funcDeclToString(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

modelToString

public static String modelToString(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

benchmarkToSmtlibString

public static String benchmarkToSmtlibString(long a0,
 String a1,
 String a2,
 String a3,
 String a4,
 int a5,
 long[] a6,
 long a7)
                                      throws Z3Exception

Throws:

Z3Exception

parseSmtlib2String

public static long parseSmtlib2String(long a0,
 String a1,
 int a2,
 long[] a3,
 long[] a4,
 int a5,
 long[] a6,
 long[] a7)
                               throws Z3Exception

Throws:

Z3Exception

parseSmtlib2File

public static long parseSmtlib2File(long a0,
 String a1,
 int a2,
 long[] a3,
 long[] a4,
 int a5,
 long[] a6,
 long[] a7)
                             throws Z3Exception

Throws:

Z3Exception

evalSmtlib2String

public static String evalSmtlib2String(long a0,
 String a1)
                                throws Z3Exception

Throws:

Z3Exception

getErrorCode

public static int getErrorCode(long a0)
                        throws Z3Exception

Throws:

Z3Exception

setError

public static void setError(long a0,
 int a1)
                     throws Z3Exception

Throws:

Z3Exception

getErrorMsg

public static String getErrorMsg(long a0,
 int a1)
                          throws Z3Exception

Throws:

Z3Exception

getVersion

public static void getVersion(Native.IntPtr a0,
 Native.IntPtr a1,
 Native.IntPtr a2,
 Native.IntPtr a3)

getFullVersion

public static String getFullVersion()

enableTrace

public static void enableTrace(String a0)

disableTrace

public static void disableTrace(String a0)

resetMemory

public static void resetMemory()

finalizeMemory

public static void finalizeMemory()

mkGoal

public static long mkGoal(long a0,
 boolean a1,
 boolean a2,
 boolean a3)
                   throws Z3Exception

Throws:

Z3Exception

goalIncRef

public static void goalIncRef(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

goalDecRef

public static void goalDecRef(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

goalPrecision

public static int goalPrecision(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

goalAssert

public static void goalAssert(long a0,
 long a1,
 long a2)
                       throws Z3Exception

Throws:

Z3Exception

goalInconsistent

public static boolean goalInconsistent(long a0,
 long a1)
                                throws Z3Exception

Throws:

Z3Exception

goalDepth

public static int goalDepth(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

goalReset

public static void goalReset(long a0,
 long a1)
                      throws Z3Exception

Throws:

Z3Exception

goalSize

public static int goalSize(long a0,
 long a1)
                    throws Z3Exception

Throws:

Z3Exception

goalFormula

public static long goalFormula(long a0,
 long a1,
 int a2)
                        throws Z3Exception

Throws:

Z3Exception

goalNumExprs

public static int goalNumExprs(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

goalIsDecidedSat

public static boolean goalIsDecidedSat(long a0,
 long a1)
                                throws Z3Exception

Throws:

Z3Exception

goalIsDecidedUnsat

public static boolean goalIsDecidedUnsat(long a0,
 long a1)
                                  throws Z3Exception

Throws:

Z3Exception

goalTranslate

public static long goalTranslate(long a0,
 long a1,
 long a2)
                          throws Z3Exception

Throws:

Z3Exception

goalConvertModel

public static long goalConvertModel(long a0,
 long a1,
 long a2)
                             throws Z3Exception

Throws:

Z3Exception

goalToString

public static String goalToString(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

goalToDimacsString

public static String goalToDimacsString(long a0,
 long a1,
 boolean a2)
                                 throws Z3Exception

Throws:

Z3Exception

mkTactic

public static long mkTactic(long a0,
 String a1)
                     throws Z3Exception

Throws:

Z3Exception

tacticIncRef

public static void tacticIncRef(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

tacticDecRef

public static void tacticDecRef(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

mkProbe

public static long mkProbe(long a0,
 String a1)
                    throws Z3Exception

Throws:

Z3Exception

probeIncRef

public static void probeIncRef(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

probeDecRef

public static void probeDecRef(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

tacticAndThen

public static long tacticAndThen(long a0,
 long a1,
 long a2)
                          throws Z3Exception

Throws:

Z3Exception

tacticOrElse

public static long tacticOrElse(long a0,
 long a1,
 long a2)
                         throws Z3Exception

Throws:

Z3Exception

tacticParOr

public static long tacticParOr(long a0,
 int a1,
 long[] a2)
                        throws Z3Exception

Throws:

Z3Exception

tacticParAndThen

public static long tacticParAndThen(long a0,
 long a1,
 long a2)
                             throws Z3Exception

Throws:

Z3Exception

tacticTryFor

public static long tacticTryFor(long a0,
 long a1,
 int a2)
                         throws Z3Exception

Throws:

Z3Exception

tacticWhen

public static long tacticWhen(long a0,
 long a1,
 long a2)
                       throws Z3Exception

Throws:

Z3Exception

tacticCond

public static long tacticCond(long a0,
 long a1,
 long a2,
 long a3)
                       throws Z3Exception

Throws:

Z3Exception

tacticRepeat

public static long tacticRepeat(long a0,
 long a1,
 int a2)
                         throws Z3Exception

Throws:

Z3Exception

tacticSkip

public static long tacticSkip(long a0)
                       throws Z3Exception

Throws:

Z3Exception

tacticFail

public static long tacticFail(long a0)
                       throws Z3Exception

Throws:

Z3Exception

tacticFailIf

public static long tacticFailIf(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

tacticFailIfNotDecided

public static long tacticFailIfNotDecided(long a0)
                                   throws Z3Exception

Throws:

Z3Exception

tacticUsingParams

public static long tacticUsingParams(long a0,
 long a1,
 long a2)
                              throws Z3Exception

Throws:

Z3Exception

probeConst

public static long probeConst(long a0,
 double a1)
                       throws Z3Exception

Throws:

Z3Exception

probeLt

public static long probeLt(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

probeGt

public static long probeGt(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

probeLe

public static long probeLe(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

probeGe

public static long probeGe(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

probeEq

public static long probeEq(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

probeAnd

public static long probeAnd(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

probeOr

public static long probeOr(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

probeNot

public static long probeNot(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

getNumTactics

public static int getNumTactics(long a0)
                         throws Z3Exception

Throws:

Z3Exception

getTacticName

public static String getTacticName(long a0,
 int a1)
                            throws Z3Exception

Throws:

Z3Exception

getNumProbes

public static int getNumProbes(long a0)
                        throws Z3Exception

Throws:

Z3Exception

getProbeName

public static String getProbeName(long a0,
 int a1)
                           throws Z3Exception

Throws:

Z3Exception

tacticGetHelp

public static String tacticGetHelp(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

tacticGetParamDescrs

public static long tacticGetParamDescrs(long a0,
 long a1)
                                 throws Z3Exception

Throws:

Z3Exception

tacticGetDescr

public static String tacticGetDescr(long a0,
 String a1)
                             throws Z3Exception

Throws:

Z3Exception

probeGetDescr

public static String probeGetDescr(long a0,
 String a1)
                            throws Z3Exception

Throws:

Z3Exception

probeApply

public static double probeApply(long a0,
 long a1,
 long a2)
                         throws Z3Exception

Throws:

Z3Exception

tacticApply

public static long tacticApply(long a0,
 long a1,
 long a2)
                        throws Z3Exception

Throws:

Z3Exception

tacticApplyEx

public static long tacticApplyEx(long a0,
 long a1,
 long a2,
 long a3)
                          throws Z3Exception

Throws:

Z3Exception

applyResultIncRef

public static void applyResultIncRef(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

applyResultDecRef

public static void applyResultDecRef(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

applyResultToString

public static String applyResultToString(long a0,
 long a1)
                                  throws Z3Exception

Throws:

Z3Exception

applyResultGetNumSubgoals

public static int applyResultGetNumSubgoals(long a0,
 long a1)
                                     throws Z3Exception

Throws:

Z3Exception

applyResultGetSubgoal

public static long applyResultGetSubgoal(long a0,
 long a1,
 int a2)
                                  throws Z3Exception

Throws:

Z3Exception

mkSolver

public static long mkSolver(long a0)
                     throws Z3Exception

Throws:

Z3Exception

mkSimpleSolver

public static long mkSimpleSolver(long a0)
                           throws Z3Exception

Throws:

Z3Exception

mkSolverForLogic

public static long mkSolverForLogic(long a0,
 long a1)
                             throws Z3Exception

Throws:

Z3Exception

mkSolverFromTactic

public static long mkSolverFromTactic(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

solverTranslate

public static long solverTranslate(long a0,
 long a1,
 long a2)
                            throws Z3Exception

Throws:

Z3Exception

solverImportModelConverter

public static void solverImportModelConverter(long a0,
 long a1,
 long a2)
                                       throws Z3Exception

Throws:

Z3Exception

solverGetHelp

public static String solverGetHelp(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

solverGetParamDescrs

public static long solverGetParamDescrs(long a0,
 long a1)
                                 throws Z3Exception

Throws:

Z3Exception

solverSetParams

public static void solverSetParams(long a0,
 long a1,
 long a2)
                            throws Z3Exception

Throws:

Z3Exception

solverIncRef

public static void solverIncRef(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

solverDecRef

public static void solverDecRef(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

solverInterrupt

public static void solverInterrupt(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

solverPush

public static void solverPush(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

solverPop

public static void solverPop(long a0,
 long a1,
 int a2)
                      throws Z3Exception

Throws:

Z3Exception

solverReset

public static void solverReset(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

solverGetNumScopes

public static int solverGetNumScopes(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

solverAssert

public static void solverAssert(long a0,
 long a1,
 long a2)
                         throws Z3Exception

Throws:

Z3Exception

solverAssertAndTrack

public static void solverAssertAndTrack(long a0,
 long a1,
 long a2,
 long a3)
                                 throws Z3Exception

Throws:

Z3Exception

solverFromFile

public static void solverFromFile(long a0,
 long a1,
 String a2)
                           throws Z3Exception

Throws:

Z3Exception

solverFromString

public static void solverFromString(long a0,
 long a1,
 String a2)
                             throws Z3Exception

Throws:

Z3Exception

solverGetAssertions

public static long solverGetAssertions(long a0,
 long a1)
                                throws Z3Exception

Throws:

Z3Exception

solverGetUnits

public static long solverGetUnits(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

solverGetTrail

public static long solverGetTrail(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

solverGetNonUnits

public static long solverGetNonUnits(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

solverGetLevels

public static void solverGetLevels(long a0,
 long a1,
 long a2,
 int a3,
 int[] a4)
                            throws Z3Exception

Throws:

Z3Exception

solverPropagateDeclare

public static long solverPropagateDeclare(long a0,
 long a1,
 int a2,
 long[] a3,
 long a4)
                                   throws Z3Exception

Throws:

Z3Exception

solverPropagateRegister

public static void solverPropagateRegister(long a0,
 long a1,
 long a2)
                                    throws Z3Exception

Throws:

Z3Exception

solverPropagateRegisterCb

public static void solverPropagateRegisterCb(long a0,
 long a1,
 long a2)
                                      throws Z3Exception

Throws:

Z3Exception

solverPropagateConsequence

public static void solverPropagateConsequence(long a0,
 long a1,
 int a2,
 long[] a3,
 int a4,
 long[] a5,
 long[] a6,
 long a7)
                                       throws Z3Exception

Throws:

Z3Exception

solverCheck

public static int solverCheck(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

solverCheckAssumptions

public static int solverCheckAssumptions(long a0,
 long a1,
 int a2,
 long[] a3)
                                  throws Z3Exception

Throws:

Z3Exception

getImpliedEqualities

public static int getImpliedEqualities(long a0,
 long a1,
 int a2,
 long[] a3,
 int[] a4)
                                throws Z3Exception

Throws:

Z3Exception

solverGetConsequences

public static int solverGetConsequences(long a0,
 long a1,
 long a2,
 long a3,
 long a4)
                                 throws Z3Exception

Throws:

Z3Exception

solverCube

public static long solverCube(long a0,
 long a1,
 long a2,
 int a3)
                       throws Z3Exception

Throws:

Z3Exception

solverGetModel

public static long solverGetModel(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

solverGetProof

public static long solverGetProof(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

solverGetUnsatCore

public static long solverGetUnsatCore(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

solverGetReasonUnknown

public static String solverGetReasonUnknown(long a0,
 long a1)
                                     throws Z3Exception

Throws:

Z3Exception

solverGetStatistics

public static long solverGetStatistics(long a0,
 long a1)
                                throws Z3Exception

Throws:

Z3Exception

solverToString

public static String solverToString(long a0,
 long a1)
                             throws Z3Exception

Throws:

Z3Exception

solverToDimacsString

public static String solverToDimacsString(long a0,
 long a1,
 boolean a2)
                                   throws Z3Exception

Throws:

Z3Exception

statsToString

public static String statsToString(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

statsIncRef

public static void statsIncRef(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

statsDecRef

public static void statsDecRef(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

statsSize

public static int statsSize(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

statsGetKey

public static String statsGetKey(long a0,
 long a1,
 int a2)
                          throws Z3Exception

Throws:

Z3Exception

statsIsUint

public static boolean statsIsUint(long a0,
 long a1,
 int a2)
                           throws Z3Exception

Throws:

Z3Exception

statsIsDouble

public static boolean statsIsDouble(long a0,
 long a1,
 int a2)
                             throws Z3Exception

Throws:

Z3Exception

statsGetUintValue

public static int statsGetUintValue(long a0,
 long a1,
 int a2)
                             throws Z3Exception

Throws:

Z3Exception

statsGetDoubleValue

public static double statsGetDoubleValue(long a0,
 long a1,
 int a2)
                                  throws Z3Exception

Throws:

Z3Exception

getEstimatedAllocSize

public static long getEstimatedAllocSize()

mkAstVector

public static long mkAstVector(long a0)
                        throws Z3Exception

Throws:

Z3Exception

astVectorIncRef

public static void astVectorIncRef(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

astVectorDecRef

public static void astVectorDecRef(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

astVectorSize

public static int astVectorSize(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

astVectorGet

public static long astVectorGet(long a0,
 long a1,
 int a2)
                         throws Z3Exception

Throws:

Z3Exception

astVectorSet

public static void astVectorSet(long a0,
 long a1,
 int a2,
 long a3)
                         throws Z3Exception

Throws:

Z3Exception

astVectorResize

public static void astVectorResize(long a0,
 long a1,
 int a2)
                            throws Z3Exception

Throws:

Z3Exception

astVectorPush

public static void astVectorPush(long a0,
 long a1,
 long a2)
                          throws Z3Exception

Throws:

Z3Exception

astVectorTranslate

public static long astVectorTranslate(long a0,
 long a1,
 long a2)
                               throws Z3Exception

Throws:

Z3Exception

astVectorToString

public static String astVectorToString(long a0,
 long a1)
                                throws Z3Exception

Throws:

Z3Exception

mkAstMap

public static long mkAstMap(long a0)
                     throws Z3Exception

Throws:

Z3Exception

astMapIncRef

public static void astMapIncRef(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

astMapDecRef

public static void astMapDecRef(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

astMapContains

public static boolean astMapContains(long a0,
 long a1,
 long a2)
                              throws Z3Exception

Throws:

Z3Exception

astMapFind

public static long astMapFind(long a0,
 long a1,
 long a2)
                       throws Z3Exception

Throws:

Z3Exception

astMapInsert

public static void astMapInsert(long a0,
 long a1,
 long a2,
 long a3)
                         throws Z3Exception

Throws:

Z3Exception

astMapErase

public static void astMapErase(long a0,
 long a1,
 long a2)
                        throws Z3Exception

Throws:

Z3Exception

astMapReset

public static void astMapReset(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

astMapSize

public static int astMapSize(long a0,
 long a1)
                      throws Z3Exception

Throws:

Z3Exception

astMapKeys

public static long astMapKeys(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

astMapToString

public static String astMapToString(long a0,
 long a1)
                             throws Z3Exception

Throws:

Z3Exception

algebraicIsValue

public static boolean algebraicIsValue(long a0,
 long a1)
                                throws Z3Exception

Throws:

Z3Exception

algebraicIsPos

public static boolean algebraicIsPos(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

algebraicIsNeg

public static boolean algebraicIsNeg(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

algebraicIsZero

public static boolean algebraicIsZero(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

algebraicSign

public static int algebraicSign(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

algebraicAdd

public static long algebraicAdd(long a0,
 long a1,
 long a2)
                         throws Z3Exception

Throws:

Z3Exception

algebraicSub

public static long algebraicSub(long a0,
 long a1,
 long a2)
                         throws Z3Exception

Throws:

Z3Exception

algebraicMul

public static long algebraicMul(long a0,
 long a1,
 long a2)
                         throws Z3Exception

Throws:

Z3Exception

algebraicDiv

public static long algebraicDiv(long a0,
 long a1,
 long a2)
                         throws Z3Exception

Throws:

Z3Exception

algebraicRoot

public static long algebraicRoot(long a0,
 long a1,
 int a2)
                          throws Z3Exception

Throws:

Z3Exception

algebraicPower

public static long algebraicPower(long a0,
 long a1,
 int a2)
                           throws Z3Exception

Throws:

Z3Exception

algebraicLt

public static boolean algebraicLt(long a0,
 long a1,
 long a2)
                           throws Z3Exception

Throws:

Z3Exception

algebraicGt

public static boolean algebraicGt(long a0,
 long a1,
 long a2)
                           throws Z3Exception

Throws:

Z3Exception

algebraicLe

public static boolean algebraicLe(long a0,
 long a1,
 long a2)
                           throws Z3Exception

Throws:

Z3Exception

algebraicGe

public static boolean algebraicGe(long a0,
 long a1,
 long a2)
                           throws Z3Exception

Throws:

Z3Exception

algebraicEq

public static boolean algebraicEq(long a0,
 long a1,
 long a2)
                           throws Z3Exception

Throws:

Z3Exception

algebraicNeq

public static boolean algebraicNeq(long a0,
 long a1,
 long a2)
                            throws Z3Exception

Throws:

Z3Exception

algebraicRoots

public static long algebraicRoots(long a0,
 long a1,
 int a2,
 long[] a3)
                           throws Z3Exception

Throws:

Z3Exception

algebraicEval

public static int algebraicEval(long a0,
 long a1,
 int a2,
 long[] a3)
                         throws Z3Exception

Throws:

Z3Exception

algebraicGetPoly

public static long algebraicGetPoly(long a0,
 long a1)
                             throws Z3Exception

Throws:

Z3Exception

algebraicGetI

public static int algebraicGetI(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

polynomialSubresultants

public static long polynomialSubresultants(long a0,
 long a1,
 long a2,
 long a3)
                                    throws Z3Exception

Throws:

Z3Exception

rcfDel

public static void rcfDel(long a0,
 long a1)
                   throws Z3Exception

Throws:

Z3Exception

rcfMkRational

public static long rcfMkRational(long a0,
 String a1)
                          throws Z3Exception

Throws:

Z3Exception

rcfMkSmallInt

public static long rcfMkSmallInt(long a0,
 int a1)
                          throws Z3Exception

Throws:

Z3Exception

rcfMkPi

public static long rcfMkPi(long a0)
                    throws Z3Exception

Throws:

Z3Exception

rcfMkE

public static long rcfMkE(long a0)
                   throws Z3Exception

Throws:

Z3Exception

rcfMkInfinitesimal

public static long rcfMkInfinitesimal(long a0)
                               throws Z3Exception

Throws:

Z3Exception

rcfMkRoots

public static int rcfMkRoots(long a0,
 int a1,
 long[] a2,
 long[] a3)
                      throws Z3Exception

Throws:

Z3Exception

rcfAdd

public static long rcfAdd(long a0,
 long a1,
 long a2)
                   throws Z3Exception

Throws:

Z3Exception

rcfSub

public static long rcfSub(long a0,
 long a1,
 long a2)
                   throws Z3Exception

Throws:

Z3Exception

rcfMul

public static long rcfMul(long a0,
 long a1,
 long a2)
                   throws Z3Exception

Throws:

Z3Exception

rcfDiv

public static long rcfDiv(long a0,
 long a1,
 long a2)
                   throws Z3Exception

Throws:

Z3Exception

rcfNeg

public static long rcfNeg(long a0,
 long a1)
                   throws Z3Exception

Throws:

Z3Exception

rcfInv

public static long rcfInv(long a0,
 long a1)
                   throws Z3Exception

Throws:

Z3Exception

rcfPower

public static long rcfPower(long a0,
 long a1,
 int a2)
                     throws Z3Exception

Throws:

Z3Exception

rcfLt

public static boolean rcfLt(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

rcfGt

public static boolean rcfGt(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

rcfLe

public static boolean rcfLe(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

rcfGe

public static boolean rcfGe(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

rcfEq

public static boolean rcfEq(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

rcfNeq

public static boolean rcfNeq(long a0,
 long a1,
 long a2)
                      throws Z3Exception

Throws:

Z3Exception

rcfNumToString

public static String rcfNumToString(long a0,
 long a1,
 boolean a2,
 boolean a3)
                             throws Z3Exception

Throws:

Z3Exception

rcfNumToDecimalString

public static String rcfNumToDecimalString(long a0,
 long a1,
 int a2)
                                    throws Z3Exception

Throws:

Z3Exception

rcfGetNumeratorDenominator

public static void rcfGetNumeratorDenominator(long a0,
 long a1,
 Native.LongPtr a2,
 Native.LongPtr a3)
                                       throws Z3Exception

Throws:

Z3Exception

mkFixedpoint

public static long mkFixedpoint(long a0)
                         throws Z3Exception

Throws:

Z3Exception

fixedpointIncRef

public static void fixedpointIncRef(long a0,
 long a1)
                             throws Z3Exception

Throws:

Z3Exception

fixedpointDecRef

public static void fixedpointDecRef(long a0,
 long a1)
                             throws Z3Exception

Throws:

Z3Exception

fixedpointAddRule

public static void fixedpointAddRule(long a0,
 long a1,
 long a2,
 long a3)
                              throws Z3Exception

Throws:

Z3Exception

fixedpointAddFact

public static void fixedpointAddFact(long a0,
 long a1,
 long a2,
 int a3,
 int[] a4)
                              throws Z3Exception

Throws:

Z3Exception

fixedpointAssert

public static void fixedpointAssert(long a0,
 long a1,
 long a2)
                             throws Z3Exception

Throws:

Z3Exception

fixedpointQuery

public static int fixedpointQuery(long a0,
 long a1,
 long a2)
                           throws Z3Exception

Throws:

Z3Exception

fixedpointQueryRelations

public static int fixedpointQueryRelations(long a0,
 long a1,
 int a2,
 long[] a3)
                                    throws Z3Exception

Throws:

Z3Exception

fixedpointGetAnswer

public static long fixedpointGetAnswer(long a0,
 long a1)
                                throws Z3Exception

Throws:

Z3Exception

fixedpointGetReasonUnknown

public static String fixedpointGetReasonUnknown(long a0,
 long a1)
                                         throws Z3Exception

Throws:

Z3Exception

fixedpointUpdateRule

public static void fixedpointUpdateRule(long a0,
 long a1,
 long a2,
 long a3)
                                 throws Z3Exception

Throws:

Z3Exception

fixedpointGetNumLevels

public static int fixedpointGetNumLevels(long a0,
 long a1,
 long a2)
                                  throws Z3Exception

Throws:

Z3Exception

fixedpointGetCoverDelta

public static long fixedpointGetCoverDelta(long a0,
 long a1,
 int a2,
 long a3)
                                    throws Z3Exception

Throws:

Z3Exception

fixedpointAddCover

public static void fixedpointAddCover(long a0,
 long a1,
 int a2,
 long a3,
 long a4)
                               throws Z3Exception

Throws:

Z3Exception

fixedpointGetStatistics

public static long fixedpointGetStatistics(long a0,
 long a1)
                                    throws Z3Exception

Throws:

Z3Exception

fixedpointRegisterRelation

public static void fixedpointRegisterRelation(long a0,
 long a1,
 long a2)
                                       throws Z3Exception

Throws:

Z3Exception

fixedpointSetPredicateRepresentation

public static void fixedpointSetPredicateRepresentation(long a0,
 long a1,
 long a2,
 int a3,
 long[] a4)
                                                 throws Z3Exception

Throws:

Z3Exception

fixedpointGetRules

public static long fixedpointGetRules(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

fixedpointGetAssertions

public static long fixedpointGetAssertions(long a0,
 long a1)
                                    throws Z3Exception

Throws:

Z3Exception

fixedpointSetParams

public static void fixedpointSetParams(long a0,
 long a1,
 long a2)
                                throws Z3Exception

Throws:

Z3Exception

fixedpointGetHelp

public static String fixedpointGetHelp(long a0,
 long a1)
                                throws Z3Exception

Throws:

Z3Exception

fixedpointGetParamDescrs

public static long fixedpointGetParamDescrs(long a0,
 long a1)
                                     throws Z3Exception

Throws:

Z3Exception

fixedpointToString

public static String fixedpointToString(long a0,
 long a1,
 int a2,
 long[] a3)
                                 throws Z3Exception

Throws:

Z3Exception

fixedpointFromString

public static long fixedpointFromString(long a0,
 long a1,
 String a2)
                                 throws Z3Exception

Throws:

Z3Exception

fixedpointFromFile

public static long fixedpointFromFile(long a0,
 long a1,
 String a2)
                               throws Z3Exception

Throws:

Z3Exception

mkOptimize

public static long mkOptimize(long a0)
                       throws Z3Exception

Throws:

Z3Exception

optimizeIncRef

public static void optimizeIncRef(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

optimizeDecRef

public static void optimizeDecRef(long a0,
 long a1)
                           throws Z3Exception

Throws:

Z3Exception

optimizeAssert

public static void optimizeAssert(long a0,
 long a1,
 long a2)
                           throws Z3Exception

Throws:

Z3Exception

optimizeAssertAndTrack

public static void optimizeAssertAndTrack(long a0,
 long a1,
 long a2,
 long a3)
                                   throws Z3Exception

Throws:

Z3Exception

optimizeAssertSoft

public static int optimizeAssertSoft(long a0,
 long a1,
 long a2,
 String a3,
 long a4)
                              throws Z3Exception

Throws:

Z3Exception

optimizeMaximize

public static int optimizeMaximize(long a0,
 long a1,
 long a2)
                            throws Z3Exception

Throws:

Z3Exception

optimizeMinimize

public static int optimizeMinimize(long a0,
 long a1,
 long a2)
                            throws Z3Exception

Throws:

Z3Exception

optimizePush

public static void optimizePush(long a0,
 long a1)
                         throws Z3Exception

Throws:

Z3Exception

optimizePop

public static void optimizePop(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

optimizeCheck

public static int optimizeCheck(long a0,
 long a1,
 int a2,
 long[] a3)
                         throws Z3Exception

Throws:

Z3Exception

optimizeGetReasonUnknown

public static String optimizeGetReasonUnknown(long a0,
 long a1)
                                       throws Z3Exception

Throws:

Z3Exception

optimizeGetModel

public static long optimizeGetModel(long a0,
 long a1)
                             throws Z3Exception

Throws:

Z3Exception

optimizeGetUnsatCore

public static long optimizeGetUnsatCore(long a0,
 long a1)
                                 throws Z3Exception

Throws:

Z3Exception

optimizeSetParams

public static void optimizeSetParams(long a0,
 long a1,
 long a2)
                              throws Z3Exception

Throws:

Z3Exception

optimizeGetParamDescrs

public static long optimizeGetParamDescrs(long a0,
 long a1)
                                   throws Z3Exception

Throws:

Z3Exception

optimizeGetLower

public static long optimizeGetLower(long a0,
 long a1,
 int a2)
                             throws Z3Exception

Throws:

Z3Exception

optimizeGetUpper

public static long optimizeGetUpper(long a0,
 long a1,
 int a2)
                             throws Z3Exception

Throws:

Z3Exception

optimizeGetLowerAsVector

public static long optimizeGetLowerAsVector(long a0,
 long a1,
 int a2)
                                     throws Z3Exception

Throws:

Z3Exception

optimizeGetUpperAsVector

public static long optimizeGetUpperAsVector(long a0,
 long a1,
 int a2)
                                     throws Z3Exception

Throws:

Z3Exception

optimizeToString

public static String optimizeToString(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

optimizeFromString

public static void optimizeFromString(long a0,
 long a1,
 String a2)
                               throws Z3Exception

Throws:

Z3Exception

optimizeFromFile

public static void optimizeFromFile(long a0,
 long a1,
 String a2)
                             throws Z3Exception

Throws:

Z3Exception

optimizeGetHelp

public static String optimizeGetHelp(long a0,
 long a1)
                              throws Z3Exception

Throws:

Z3Exception

optimizeGetStatistics

public static long optimizeGetStatistics(long a0,
 long a1)
                                  throws Z3Exception

Throws:

Z3Exception

optimizeGetAssertions

public static long optimizeGetAssertions(long a0,
 long a1)
                                  throws Z3Exception

Throws:

Z3Exception

optimizeGetObjectives

public static long optimizeGetObjectives(long a0,
 long a1)
                                  throws Z3Exception

Throws:

Z3Exception

mkFpaRoundingModeSort

public static long mkFpaRoundingModeSort(long a0)
                                  throws Z3Exception

Throws:

Z3Exception

mkFpaRoundNearestTiesToEven

public static long mkFpaRoundNearestTiesToEven(long a0)
                                        throws Z3Exception

Throws:

Z3Exception

mkFpaRne

public static long mkFpaRne(long a0)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaRoundNearestTiesToAway

public static long mkFpaRoundNearestTiesToAway(long a0)
                                        throws Z3Exception

Throws:

Z3Exception

mkFpaRna

public static long mkFpaRna(long a0)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaRoundTowardPositive

public static long mkFpaRoundTowardPositive(long a0)
                                     throws Z3Exception

Throws:

Z3Exception

mkFpaRtp

public static long mkFpaRtp(long a0)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaRoundTowardNegative

public static long mkFpaRoundTowardNegative(long a0)
                                     throws Z3Exception

Throws:

Z3Exception

mkFpaRtn

public static long mkFpaRtn(long a0)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaRoundTowardZero

public static long mkFpaRoundTowardZero(long a0)
                                 throws Z3Exception

Throws:

Z3Exception

mkFpaRtz

public static long mkFpaRtz(long a0)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaSort

public static long mkFpaSort(long a0,
 int a1,
 int a2)
                      throws Z3Exception

Throws:

Z3Exception

mkFpaSortHalf

public static long mkFpaSortHalf(long a0)
                          throws Z3Exception

Throws:

Z3Exception

mkFpaSort16

public static long mkFpaSort16(long a0)
                        throws Z3Exception

Throws:

Z3Exception

mkFpaSortSingle

public static long mkFpaSortSingle(long a0)
                            throws Z3Exception

Throws:

Z3Exception

mkFpaSort32

public static long mkFpaSort32(long a0)
                        throws Z3Exception

Throws:

Z3Exception

mkFpaSortDouble

public static long mkFpaSortDouble(long a0)
                            throws Z3Exception

Throws:

Z3Exception

mkFpaSort64

public static long mkFpaSort64(long a0)
                        throws Z3Exception

Throws:

Z3Exception

mkFpaSortQuadruple

public static long mkFpaSortQuadruple(long a0)
                               throws Z3Exception

Throws:

Z3Exception

mkFpaSort128

public static long mkFpaSort128(long a0)
                         throws Z3Exception

Throws:

Z3Exception

mkFpaNan

public static long mkFpaNan(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaInf

public static long mkFpaInf(long a0,
 long a1,
 boolean a2)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaZero

public static long mkFpaZero(long a0,
 long a1,
 boolean a2)
                      throws Z3Exception

Throws:

Z3Exception

mkFpaFp

public static long mkFpaFp(long a0,
 long a1,
 long a2,
 long a3)
                    throws Z3Exception

Throws:

Z3Exception

mkFpaNumeralFloat

public static long mkFpaNumeralFloat(long a0,
 float a1,
 long a2)
                              throws Z3Exception

Throws:

Z3Exception

mkFpaNumeralDouble

public static long mkFpaNumeralDouble(long a0,
 double a1,
 long a2)
                               throws Z3Exception

Throws:

Z3Exception

mkFpaNumeralInt

public static long mkFpaNumeralInt(long a0,
 int a1,
 long a2)
                            throws Z3Exception

Throws:

Z3Exception

mkFpaNumeralIntUint

public static long mkFpaNumeralIntUint(long a0,
 boolean a1,
 int a2,
 int a3,
 long a4)
                                throws Z3Exception

Throws:

Z3Exception

mkFpaNumeralInt64Uint64

public static long mkFpaNumeralInt64Uint64(long a0,
 boolean a1,
 long a2,
 long a3,
 long a4)
                                    throws Z3Exception

Throws:

Z3Exception

mkFpaAbs

public static long mkFpaAbs(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaNeg

public static long mkFpaNeg(long a0,
 long a1)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaAdd

public static long mkFpaAdd(long a0,
 long a1,
 long a2,
 long a3)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaSub

public static long mkFpaSub(long a0,
 long a1,
 long a2,
 long a3)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaMul

public static long mkFpaMul(long a0,
 long a1,
 long a2,
 long a3)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaDiv

public static long mkFpaDiv(long a0,
 long a1,
 long a2,
 long a3)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaFma

public static long mkFpaFma(long a0,
 long a1,
 long a2,
 long a3,
 long a4)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaSqrt

public static long mkFpaSqrt(long a0,
 long a1,
 long a2)
                      throws Z3Exception

Throws:

Z3Exception

mkFpaRem

public static long mkFpaRem(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaRoundToIntegral

public static long mkFpaRoundToIntegral(long a0,
 long a1,
 long a2)
                                 throws Z3Exception

Throws:

Z3Exception

mkFpaMin

public static long mkFpaMin(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaMax

public static long mkFpaMax(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaLeq

public static long mkFpaLeq(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaLt

public static long mkFpaLt(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkFpaGeq

public static long mkFpaGeq(long a0,
 long a1,
 long a2)
                     throws Z3Exception

Throws:

Z3Exception

mkFpaGt

public static long mkFpaGt(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkFpaEq

public static long mkFpaEq(long a0,
 long a1,
 long a2)
                    throws Z3Exception

Throws:

Z3Exception

mkFpaIsNormal

public static long mkFpaIsNormal(long a0,
 long a1)
                          throws Z3Exception

Throws:

Z3Exception

mkFpaIsSubnormal

public static long mkFpaIsSubnormal(long a0,
 long a1)
                             throws Z3Exception

Throws:

Z3Exception

mkFpaIsZero

public static long mkFpaIsZero(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

mkFpaIsInfinite

public static long mkFpaIsInfinite(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

mkFpaIsNan

public static long mkFpaIsNan(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

mkFpaIsNegative

public static long mkFpaIsNegative(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

mkFpaIsPositive

public static long mkFpaIsPositive(long a0,
 long a1)
                            throws Z3Exception

Throws:

Z3Exception

mkFpaToFpBv

public static long mkFpaToFpBv(long a0,
 long a1,
 long a2)
                        throws Z3Exception

Throws:

Z3Exception

mkFpaToFpFloat

public static long mkFpaToFpFloat(long a0,
 long a1,
 long a2,
 long a3)
                           throws Z3Exception

Throws:

Z3Exception

mkFpaToFpReal

public static long mkFpaToFpReal(long a0,
 long a1,
 long a2,
 long a3)
                          throws Z3Exception

Throws:

Z3Exception

mkFpaToFpSigned

public static long mkFpaToFpSigned(long a0,
 long a1,
 long a2,
 long a3)
                            throws Z3Exception

Throws:

Z3Exception

mkFpaToFpUnsigned

public static long mkFpaToFpUnsigned(long a0,
 long a1,
 long a2,
 long a3)
                              throws Z3Exception

Throws:

Z3Exception

mkFpaToUbv

public static long mkFpaToUbv(long a0,
 long a1,
 long a2,
 int a3)
                       throws Z3Exception

Throws:

Z3Exception

mkFpaToSbv

public static long mkFpaToSbv(long a0,
 long a1,
 long a2,
 int a3)
                       throws Z3Exception

Throws:

Z3Exception

mkFpaToReal

public static long mkFpaToReal(long a0,
 long a1)
                        throws Z3Exception

Throws:

Z3Exception

fpaGetEbits

public static int fpaGetEbits(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

fpaGetSbits

public static int fpaGetSbits(long a0,
 long a1)
                       throws Z3Exception

Throws:

Z3Exception

fpaIsNumeralNan

public static boolean fpaIsNumeralNan(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

fpaIsNumeralInf

public static boolean fpaIsNumeralInf(long a0,
 long a1)
                               throws Z3Exception

Throws:

Z3Exception

fpaIsNumeralZero

public static boolean fpaIsNumeralZero(long a0,
 long a1)
                                throws Z3Exception

Throws:

Z3Exception

fpaIsNumeralNormal

public static boolean fpaIsNumeralNormal(long a0,
 long a1)
                                  throws Z3Exception

Throws:

Z3Exception

fpaIsNumeralSubnormal

public static boolean fpaIsNumeralSubnormal(long a0,
 long a1)
                                     throws Z3Exception

Throws:

Z3Exception

fpaIsNumeralPositive

public static boolean fpaIsNumeralPositive(long a0,
 long a1)
                                    throws Z3Exception

Throws:

Z3Exception

fpaIsNumeralNegative

public static boolean fpaIsNumeralNegative(long a0,
 long a1)
                                    throws Z3Exception

Throws:

Z3Exception

fpaGetNumeralSignBv

public static long fpaGetNumeralSignBv(long a0,
 long a1)
                                throws Z3Exception

Throws:

Z3Exception

fpaGetNumeralSignificandBv

public static long fpaGetNumeralSignificandBv(long a0,
 long a1)
                                       throws Z3Exception

Throws:

Z3Exception

fpaGetNumeralSign

public static boolean fpaGetNumeralSign(long a0,
 long a1,
 Native.IntPtr a2)
                                 throws Z3Exception

Throws:

Z3Exception

fpaGetNumeralSignificandString

public static String fpaGetNumeralSignificandString(long a0,
 long a1)
                                             throws Z3Exception

Throws:

Z3Exception

fpaGetNumeralSignificandUint64

public static boolean fpaGetNumeralSignificandUint64(long a0,
 long a1,
 Native.LongPtr a2)
                                              throws Z3Exception

Throws:

Z3Exception

fpaGetNumeralExponentString

public static String fpaGetNumeralExponentString(long a0,
 long a1,
 boolean a2)
                                          throws Z3Exception

Throws:

Z3Exception

fpaGetNumeralExponentInt64

public static boolean fpaGetNumeralExponentInt64(long a0,
 long a1,
 Native.LongPtr a2,
 boolean a3)
                                          throws Z3Exception

Throws:

Z3Exception

fpaGetNumeralExponentBv

public static long fpaGetNumeralExponentBv(long a0,
 long a1,
 boolean a2)
                                    throws Z3Exception

Throws:

Z3Exception

mkFpaToIeeeBv

public static long mkFpaToIeeeBv(long a0,
 long a1)
                          throws Z3Exception

Throws:

Z3Exception

mkFpaToFpIntReal

public static long mkFpaToFpIntReal(long a0,
 long a1,
 long a2,
 long a3,
 long a4)
                             throws Z3Exception

Throws:

Z3Exception

fixedpointQueryFromLvl

public static int fixedpointQueryFromLvl(long a0,
 long a1,
 long a2,
 int a3)
                                  throws Z3Exception

Throws:

Z3Exception

fixedpointGetGroundSatAnswer

public static long fixedpointGetGroundSatAnswer(long a0,
 long a1)
                                         throws Z3Exception

Throws:

Z3Exception

fixedpointGetRulesAlongTrace

public static long fixedpointGetRulesAlongTrace(long a0,
 long a1)
                                         throws Z3Exception

Throws:

Z3Exception

fixedpointGetRuleNamesAlongTrace

public static long fixedpointGetRuleNamesAlongTrace(long a0,
 long a1)
                                             throws Z3Exception

Throws:

Z3Exception

fixedpointAddInvariant

public static void fixedpointAddInvariant(long a0,
 long a1,
 long a2,
 long a3)
                                   throws Z3Exception

Throws:

Z3Exception

fixedpointGetReachable

public static long fixedpointGetReachable(long a0,
 long a1,
 long a2)
                                   throws Z3Exception

Throws:

Z3Exception

qeModelProject

public static long qeModelProject(long a0,
 long a1,
 int a2,
 long[] a3,
 long a4)
                           throws Z3Exception

Throws:

Z3Exception

qeModelProjectSkolem

public static long qeModelProjectSkolem(long a0,
 long a1,
 int a2,
 long[] a3,
 long a4,
 long a5)
                                 throws Z3Exception

Throws:

Z3Exception

modelExtrapolate

public static long modelExtrapolate(long a0,
 long a1,
 long a2)
                             throws Z3Exception

Throws:

Z3Exception

qeLite

public static long qeLite(long a0,
 long a1,
 long a2)
                   throws Z3Exception

Throws:

Z3Exception