Data Structures | |
class | IntPtr |
class | LongPtr |
class | ObjArrayPtr |
class | StringPtr |
class | UIntArrayPtr |
Static Public Member Functions | |
static native void | setInternalErrorHandler (long ctx) |
static void | globalParamSet (String a0, String a1) |
static void | globalParamResetAll () |
static boolean | globalParamGet (String a0, StringPtr a1) |
static long | mkConfig () |
static void | delConfig (long a0) |
static void | setParamValue (long a0, String a1, String a2) |
static long | mkContext (long a0) throws Z3Exception |
static long | mkContextRc (long a0) throws Z3Exception |
static void | delContext (long a0) throws Z3Exception |
static void | incRef (long a0, long a1) throws Z3Exception |
static void | decRef (long a0, long a1) throws Z3Exception |
static void | updateParamValue (long a0, String a1, String a2) throws Z3Exception |
static void | interrupt (long a0) throws Z3Exception |
static long | mkParams (long a0) throws Z3Exception |
static void | paramsIncRef (long a0, long a1) throws Z3Exception |
static void | paramsDecRef (long a0, long a1) throws Z3Exception |
static void | paramsSetBool (long a0, long a1, long a2, boolean a3) throws Z3Exception |
static void | paramsSetUint (long a0, long a1, long a2, int a3) throws Z3Exception |
static void | paramsSetDouble (long a0, long a1, long a2, double a3) throws Z3Exception |
static void | paramsSetSymbol (long a0, long a1, long a2, long a3) throws Z3Exception |
static String | paramsToString (long a0, long a1) throws Z3Exception |
static void | paramsValidate (long a0, long a1, long a2) throws Z3Exception |
static void | paramDescrsIncRef (long a0, long a1) throws Z3Exception |
static void | paramDescrsDecRef (long a0, long a1) throws Z3Exception |
static int | paramDescrsGetKind (long a0, long a1, long a2) throws Z3Exception |
static int | paramDescrsSize (long a0, long a1) throws Z3Exception |
static long | paramDescrsGetName (long a0, long a1, int a2) throws Z3Exception |
static String | paramDescrsGetDocumentation (long a0, long a1, long a2) throws Z3Exception |
static String | paramDescrsToString (long a0, long a1) throws Z3Exception |
static long | mkIntSymbol (long a0, int a1) throws Z3Exception |
static long | mkStringSymbol (long a0, String a1) throws Z3Exception |
static long | mkUninterpretedSort (long a0, long a1) throws Z3Exception |
static long | mkBoolSort (long a0) throws Z3Exception |
static long | mkIntSort (long a0) throws Z3Exception |
static long | mkRealSort (long a0) throws Z3Exception |
static long | mkBvSort (long a0, int a1) throws Z3Exception |
static long | mkFiniteDomainSort (long a0, long a1, long a2) throws Z3Exception |
static long | mkArraySort (long a0, long a1, long a2) throws Z3Exception |
static long | mkArraySortN (long a0, int a1, long[] a2, long a3) throws Z3Exception |
static long | mkTupleSort (long a0, long a1, int a2, long[] a3, long[] a4, LongPtr a5, long[] a6) throws Z3Exception |
static long | mkEnumerationSort (long a0, long a1, int a2, long[] a3, long[] a4, long[] a5) throws Z3Exception |
static long | mkListSort (long a0, long a1, long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8) throws Z3Exception |
static long | mkConstructor (long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6) throws Z3Exception |
static void | delConstructor (long a0, long a1) throws Z3Exception |
static long | mkDatatype (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | mkConstructorList (long a0, int a1, long[] a2) throws Z3Exception |
static void | delConstructorList (long a0, long a1) throws Z3Exception |
static void | mkDatatypes (long a0, int a1, long[] a2, long[] a3, long[] a4) throws Z3Exception |
static void | queryConstructor (long a0, long a1, int a2, LongPtr a3, LongPtr a4, long[] a5) throws Z3Exception |
static long | mkFuncDecl (long a0, long a1, int a2, long[] a3, long a4) throws Z3Exception |
static long | mkApp (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | mkConst (long a0, long a1, long a2) throws Z3Exception |
static long | mkFreshFuncDecl (long a0, String a1, int a2, long[] a3, long a4) throws Z3Exception |
static long | mkFreshConst (long a0, String a1, long a2) throws Z3Exception |
static long | mkRecFuncDecl (long a0, long a1, int a2, long[] a3, long a4) throws Z3Exception |
static void | addRecDef (long a0, long a1, int a2, long[] a3, long a4) throws Z3Exception |
static long | mkTrue (long a0) throws Z3Exception |
static long | mkFalse (long a0) throws Z3Exception |
static long | mkEq (long a0, long a1, long a2) throws Z3Exception |
static long | mkDistinct (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkNot (long a0, long a1) throws Z3Exception |
static long | mkIte (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkIff (long a0, long a1, long a2) throws Z3Exception |
static long | mkImplies (long a0, long a1, long a2) throws Z3Exception |
static long | mkXor (long a0, long a1, long a2) throws Z3Exception |
static long | mkAnd (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkOr (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkAdd (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkMul (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkSub (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkUnaryMinus (long a0, long a1) throws Z3Exception |
static long | mkDiv (long a0, long a1, long a2) throws Z3Exception |
static long | mkMod (long a0, long a1, long a2) throws Z3Exception |
static long | mkRem (long a0, long a1, long a2) throws Z3Exception |
static long | mkPower (long a0, long a1, long a2) throws Z3Exception |
static long | mkLt (long a0, long a1, long a2) throws Z3Exception |
static long | mkLe (long a0, long a1, long a2) throws Z3Exception |
static long | mkGt (long a0, long a1, long a2) throws Z3Exception |
static long | mkGe (long a0, long a1, long a2) throws Z3Exception |
static long | mkDivides (long a0, long a1, long a2) throws Z3Exception |
static long | mkInt2real (long a0, long a1) throws Z3Exception |
static long | mkReal2int (long a0, long a1) throws Z3Exception |
static long | mkIsInt (long a0, long a1) throws Z3Exception |
static long | mkBvnot (long a0, long a1) throws Z3Exception |
static long | mkBvredand (long a0, long a1) throws Z3Exception |
static long | mkBvredor (long a0, long a1) throws Z3Exception |
static long | mkBvand (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvor (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvxor (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvnand (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvnor (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvxnor (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvneg (long a0, long a1) throws Z3Exception |
static long | mkBvadd (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsub (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvmul (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvudiv (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsdiv (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvurem (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsrem (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsmod (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvult (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvslt (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvule (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsle (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvuge (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsge (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvugt (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsgt (long a0, long a1, long a2) throws Z3Exception |
static long | mkConcat (long a0, long a1, long a2) throws Z3Exception |
static long | mkExtract (long a0, int a1, int a2, long a3) throws Z3Exception |
static long | mkSignExt (long a0, int a1, long a2) throws Z3Exception |
static long | mkZeroExt (long a0, int a1, long a2) throws Z3Exception |
static long | mkRepeat (long a0, int a1, long a2) throws Z3Exception |
static long | mkBvshl (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvlshr (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvashr (long a0, long a1, long a2) throws Z3Exception |
static long | mkRotateLeft (long a0, int a1, long a2) throws Z3Exception |
static long | mkRotateRight (long a0, int a1, long a2) throws Z3Exception |
static long | mkExtRotateLeft (long a0, long a1, long a2) throws Z3Exception |
static long | mkExtRotateRight (long a0, long a1, long a2) throws Z3Exception |
static long | mkInt2bv (long a0, int a1, long a2) throws Z3Exception |
static long | mkBv2int (long a0, long a1, boolean a2) throws Z3Exception |
static long | mkBvaddNoOverflow (long a0, long a1, long a2, boolean a3) throws Z3Exception |
static long | mkBvaddNoUnderflow (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsubNoOverflow (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsubNoUnderflow (long a0, long a1, long a2, boolean a3) throws Z3Exception |
static long | mkBvsdivNoOverflow (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvnegNoOverflow (long a0, long a1) throws Z3Exception |
static long | mkBvmulNoOverflow (long a0, long a1, long a2, boolean a3) throws Z3Exception |
static long | mkBvmulNoUnderflow (long a0, long a1, long a2) throws Z3Exception |
static long | mkSelect (long a0, long a1, long a2) throws Z3Exception |
static long | mkSelectN (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | mkStore (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkStoreN (long a0, long a1, int a2, long[] a3, long a4) throws Z3Exception |
static long | mkConstArray (long a0, long a1, long a2) throws Z3Exception |
static long | mkMap (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | mkArrayDefault (long a0, long a1) throws Z3Exception |
static long | mkAsArray (long a0, long a1) throws Z3Exception |
static long | mkSetHasSize (long a0, long a1, long a2) throws Z3Exception |
static long | mkSetSort (long a0, long a1) throws Z3Exception |
static long | mkEmptySet (long a0, long a1) throws Z3Exception |
static long | mkFullSet (long a0, long a1) throws Z3Exception |
static long | mkSetAdd (long a0, long a1, long a2) throws Z3Exception |
static long | mkSetDel (long a0, long a1, long a2) throws Z3Exception |
static long | mkSetUnion (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkSetIntersect (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkSetDifference (long a0, long a1, long a2) throws Z3Exception |
static long | mkSetComplement (long a0, long a1) throws Z3Exception |
static long | mkSetMember (long a0, long a1, long a2) throws Z3Exception |
static long | mkSetSubset (long a0, long a1, long a2) throws Z3Exception |
static long | mkArrayExt (long a0, long a1, long a2) throws Z3Exception |
static long | mkNumeral (long a0, String a1, long a2) throws Z3Exception |
static long | mkReal (long a0, int a1, int a2) throws Z3Exception |
static long | mkInt (long a0, int a1, long a2) throws Z3Exception |
static long | mkUnsignedInt (long a0, int a1, long a2) throws Z3Exception |
static long | mkInt64 (long a0, long a1, long a2) throws Z3Exception |
static long | mkUnsignedInt64 (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvNumeral (long a0, int a1, boolean[] a2) throws Z3Exception |
static long | mkSeqSort (long a0, long a1) throws Z3Exception |
static boolean | isSeqSort (long a0, long a1) throws Z3Exception |
static long | getSeqSortBasis (long a0, long a1) throws Z3Exception |
static long | mkReSort (long a0, long a1) throws Z3Exception |
static boolean | isReSort (long a0, long a1) throws Z3Exception |
static long | getReSortBasis (long a0, long a1) throws Z3Exception |
static long | mkStringSort (long a0) throws Z3Exception |
static boolean | isStringSort (long a0, long a1) throws Z3Exception |
static long | mkString (long a0, String a1) throws Z3Exception |
static long | mkLstring (long a0, int a1, String a2) throws Z3Exception |
static boolean | isString (long a0, long a1) throws Z3Exception |
static String | getString (long a0, long a1) throws Z3Exception |
static String | getLstring (long a0, long a1, IntPtr a2) throws Z3Exception |
static long | mkSeqEmpty (long a0, long a1) throws Z3Exception |
static long | mkSeqUnit (long a0, long a1) throws Z3Exception |
static long | mkSeqConcat (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkSeqPrefix (long a0, long a1, long a2) throws Z3Exception |
static long | mkSeqSuffix (long a0, long a1, long a2) throws Z3Exception |
static long | mkSeqContains (long a0, long a1, long a2) throws Z3Exception |
static long | mkStrLt (long a0, long a1, long a2) throws Z3Exception |
static long | mkStrLe (long a0, long a1, long a2) throws Z3Exception |
static long | mkSeqExtract (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkSeqReplace (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkSeqAt (long a0, long a1, long a2) throws Z3Exception |
static long | mkSeqNth (long a0, long a1, long a2) throws Z3Exception |
static long | mkSeqLength (long a0, long a1) throws Z3Exception |
static long | mkSeqIndex (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkSeqLastIndex (long a0, long a1, long a2) throws Z3Exception |
static long | mkStrToInt (long a0, long a1) throws Z3Exception |
static long | mkIntToStr (long a0, long a1) throws Z3Exception |
static long | mkSeqToRe (long a0, long a1) throws Z3Exception |
static long | mkSeqInRe (long a0, long a1, long a2) throws Z3Exception |
static long | mkRePlus (long a0, long a1) throws Z3Exception |
static long | mkReStar (long a0, long a1) throws Z3Exception |
static long | mkReOption (long a0, long a1) throws Z3Exception |
static long | mkReUnion (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkReConcat (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkReRange (long a0, long a1, long a2) throws Z3Exception |
static long | mkReLoop (long a0, long a1, int a2, int a3) throws Z3Exception |
static long | mkReIntersect (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkReComplement (long a0, long a1) throws Z3Exception |
static long | mkReEmpty (long a0, long a1) throws Z3Exception |
static long | mkReFull (long a0, long a1) throws Z3Exception |
static long | mkLinearOrder (long a0, long a1, int a2) throws Z3Exception |
static long | mkPartialOrder (long a0, long a1, int a2) throws Z3Exception |
static long | mkPiecewiseLinearOrder (long a0, long a1, int a2) throws Z3Exception |
static long | mkTreeOrder (long a0, long a1, int a2) throws Z3Exception |
static long | mkTransitiveClosure (long a0, long a1) throws Z3Exception |
static long | mkPattern (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkBound (long a0, int a1, long a2) throws Z3Exception |
static long | mkForall (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7) throws Z3Exception |
static long | mkExists (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7) throws Z3Exception |
static long | mkQuantifier (long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8) throws Z3Exception |
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 |
static long | mkForallConst (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6) throws Z3Exception |
static long | mkExistsConst (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6) throws Z3Exception |
static long | mkQuantifierConst (long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7) throws Z3Exception |
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 |
static long | mkLambda (long a0, int a1, long[] a2, long[] a3, long a4) throws Z3Exception |
static long | mkLambdaConst (long a0, int a1, long[] a2, long a3) throws Z3Exception |
static int | getSymbolKind (long a0, long a1) throws Z3Exception |
static int | getSymbolInt (long a0, long a1) throws Z3Exception |
static String | getSymbolString (long a0, long a1) throws Z3Exception |
static long | getSortName (long a0, long a1) throws Z3Exception |
static int | getSortId (long a0, long a1) throws Z3Exception |
static long | sortToAst (long a0, long a1) throws Z3Exception |
static boolean | isEqSort (long a0, long a1, long a2) throws Z3Exception |
static int | getSortKind (long a0, long a1) throws Z3Exception |
static int | getBvSortSize (long a0, long a1) throws Z3Exception |
static boolean | getFiniteDomainSortSize (long a0, long a1, LongPtr a2) throws Z3Exception |
static long | getArraySortDomain (long a0, long a1) throws Z3Exception |
static long | getArraySortRange (long a0, long a1) throws Z3Exception |
static long | getTupleSortMkDecl (long a0, long a1) throws Z3Exception |
static int | getTupleSortNumFields (long a0, long a1) throws Z3Exception |
static long | getTupleSortFieldDecl (long a0, long a1, int a2) throws Z3Exception |
static int | getDatatypeSortNumConstructors (long a0, long a1) throws Z3Exception |
static long | getDatatypeSortConstructor (long a0, long a1, int a2) throws Z3Exception |
static long | getDatatypeSortRecognizer (long a0, long a1, int a2) throws Z3Exception |
static long | getDatatypeSortConstructorAccessor (long a0, long a1, int a2, int a3) throws Z3Exception |
static long | datatypeUpdateField (long a0, long a1, long a2, long a3) throws Z3Exception |
static int | getRelationArity (long a0, long a1) throws Z3Exception |
static long | getRelationColumn (long a0, long a1, int a2) throws Z3Exception |
static long | mkAtmost (long a0, int a1, long[] a2, int a3) throws Z3Exception |
static long | mkAtleast (long a0, int a1, long[] a2, int a3) throws Z3Exception |
static long | mkPble (long a0, int a1, long[] a2, int[] a3, int a4) throws Z3Exception |
static long | mkPbge (long a0, int a1, long[] a2, int[] a3, int a4) throws Z3Exception |
static long | mkPbeq (long a0, int a1, long[] a2, int[] a3, int a4) throws Z3Exception |
static long | funcDeclToAst (long a0, long a1) throws Z3Exception |
static boolean | isEqFuncDecl (long a0, long a1, long a2) throws Z3Exception |
static int | getFuncDeclId (long a0, long a1) throws Z3Exception |
static long | getDeclName (long a0, long a1) throws Z3Exception |
static int | getDeclKind (long a0, long a1) throws Z3Exception |
static int | getDomainSize (long a0, long a1) throws Z3Exception |
static int | getArity (long a0, long a1) throws Z3Exception |
static long | getDomain (long a0, long a1, int a2) throws Z3Exception |
static long | getRange (long a0, long a1) throws Z3Exception |
static int | getDeclNumParameters (long a0, long a1) throws Z3Exception |
static int | getDeclParameterKind (long a0, long a1, int a2) throws Z3Exception |
static int | getDeclIntParameter (long a0, long a1, int a2) throws Z3Exception |
static double | getDeclDoubleParameter (long a0, long a1, int a2) throws Z3Exception |
static long | getDeclSymbolParameter (long a0, long a1, int a2) throws Z3Exception |
static long | getDeclSortParameter (long a0, long a1, int a2) throws Z3Exception |
static long | getDeclAstParameter (long a0, long a1, int a2) throws Z3Exception |
static long | getDeclFuncDeclParameter (long a0, long a1, int a2) throws Z3Exception |
static String | getDeclRationalParameter (long a0, long a1, int a2) throws Z3Exception |
static long | appToAst (long a0, long a1) throws Z3Exception |
static long | getAppDecl (long a0, long a1) throws Z3Exception |
static int | getAppNumArgs (long a0, long a1) throws Z3Exception |
static long | getAppArg (long a0, long a1, int a2) throws Z3Exception |
static boolean | isEqAst (long a0, long a1, long a2) throws Z3Exception |
static int | getAstId (long a0, long a1) throws Z3Exception |
static int | getAstHash (long a0, long a1) throws Z3Exception |
static long | getSort (long a0, long a1) throws Z3Exception |
static boolean | isWellSorted (long a0, long a1) throws Z3Exception |
static int | getBoolValue (long a0, long a1) throws Z3Exception |
static int | getAstKind (long a0, long a1) throws Z3Exception |
static boolean | isApp (long a0, long a1) throws Z3Exception |
static boolean | isNumeralAst (long a0, long a1) throws Z3Exception |
static boolean | isAlgebraicNumber (long a0, long a1) throws Z3Exception |
static long | toApp (long a0, long a1) throws Z3Exception |
static long | toFuncDecl (long a0, long a1) throws Z3Exception |
static String | getNumeralString (long a0, long a1) throws Z3Exception |
static String | getNumeralDecimalString (long a0, long a1, int a2) throws Z3Exception |
static double | getNumeralDouble (long a0, long a1) throws Z3Exception |
static long | getNumerator (long a0, long a1) throws Z3Exception |
static long | getDenominator (long a0, long a1) throws Z3Exception |
static boolean | getNumeralSmall (long a0, long a1, LongPtr a2, LongPtr a3) throws Z3Exception |
static boolean | getNumeralInt (long a0, long a1, IntPtr a2) throws Z3Exception |
static boolean | getNumeralUint (long a0, long a1, IntPtr a2) throws Z3Exception |
static boolean | getNumeralUint64 (long a0, long a1, LongPtr a2) throws Z3Exception |
static boolean | getNumeralInt64 (long a0, long a1, LongPtr a2) throws Z3Exception |
static boolean | getNumeralRationalInt64 (long a0, long a1, LongPtr a2, LongPtr a3) throws Z3Exception |
static long | getAlgebraicNumberLower (long a0, long a1, int a2) throws Z3Exception |
static long | getAlgebraicNumberUpper (long a0, long a1, int a2) throws Z3Exception |
static long | patternToAst (long a0, long a1) throws Z3Exception |
static int | getPatternNumTerms (long a0, long a1) throws Z3Exception |
static long | getPattern (long a0, long a1, int a2) throws Z3Exception |
static int | getIndexValue (long a0, long a1) throws Z3Exception |
static boolean | isQuantifierForall (long a0, long a1) throws Z3Exception |
static boolean | isQuantifierExists (long a0, long a1) throws Z3Exception |
static boolean | isLambda (long a0, long a1) throws Z3Exception |
static int | getQuantifierWeight (long a0, long a1) throws Z3Exception |
static int | getQuantifierNumPatterns (long a0, long a1) throws Z3Exception |
static long | getQuantifierPatternAst (long a0, long a1, int a2) throws Z3Exception |
static int | getQuantifierNumNoPatterns (long a0, long a1) throws Z3Exception |
static long | getQuantifierNoPatternAst (long a0, long a1, int a2) throws Z3Exception |
static int | getQuantifierNumBound (long a0, long a1) throws Z3Exception |
static long | getQuantifierBoundName (long a0, long a1, int a2) throws Z3Exception |
static long | getQuantifierBoundSort (long a0, long a1, int a2) throws Z3Exception |
static long | getQuantifierBody (long a0, long a1) throws Z3Exception |
static long | simplify (long a0, long a1) throws Z3Exception |
static long | simplifyEx (long a0, long a1, long a2) throws Z3Exception |
static String | simplifyGetHelp (long a0) throws Z3Exception |
static long | simplifyGetParamDescrs (long a0) throws Z3Exception |
static long | updateTerm (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | substitute (long a0, long a1, int a2, long[] a3, long[] a4) throws Z3Exception |
static long | substituteVars (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | translate (long a0, long a1, long a2) throws Z3Exception |
static long | mkModel (long a0) throws Z3Exception |
static void | modelIncRef (long a0, long a1) throws Z3Exception |
static void | modelDecRef (long a0, long a1) throws Z3Exception |
static boolean | modelEval (long a0, long a1, long a2, boolean a3, LongPtr a4) throws Z3Exception |
static long | modelGetConstInterp (long a0, long a1, long a2) throws Z3Exception |
static boolean | modelHasInterp (long a0, long a1, long a2) throws Z3Exception |
static long | modelGetFuncInterp (long a0, long a1, long a2) throws Z3Exception |
static int | modelGetNumConsts (long a0, long a1) throws Z3Exception |
static long | modelGetConstDecl (long a0, long a1, int a2) throws Z3Exception |
static int | modelGetNumFuncs (long a0, long a1) throws Z3Exception |
static long | modelGetFuncDecl (long a0, long a1, int a2) throws Z3Exception |
static int | modelGetNumSorts (long a0, long a1) throws Z3Exception |
static long | modelGetSort (long a0, long a1, int a2) throws Z3Exception |
static long | modelGetSortUniverse (long a0, long a1, long a2) throws Z3Exception |
static long | modelTranslate (long a0, long a1, long a2) throws Z3Exception |
static boolean | isAsArray (long a0, long a1) throws Z3Exception |
static long | getAsArrayFuncDecl (long a0, long a1) throws Z3Exception |
static long | addFuncInterp (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | addConstInterp (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | funcInterpIncRef (long a0, long a1) throws Z3Exception |
static void | funcInterpDecRef (long a0, long a1) throws Z3Exception |
static int | funcInterpGetNumEntries (long a0, long a1) throws Z3Exception |
static long | funcInterpGetEntry (long a0, long a1, int a2) throws Z3Exception |
static long | funcInterpGetElse (long a0, long a1) throws Z3Exception |
static void | funcInterpSetElse (long a0, long a1, long a2) throws Z3Exception |
static int | funcInterpGetArity (long a0, long a1) throws Z3Exception |
static void | funcInterpAddEntry (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | funcEntryIncRef (long a0, long a1) throws Z3Exception |
static void | funcEntryDecRef (long a0, long a1) throws Z3Exception |
static long | funcEntryGetValue (long a0, long a1) throws Z3Exception |
static int | funcEntryGetNumArgs (long a0, long a1) throws Z3Exception |
static long | funcEntryGetArg (long a0, long a1, int a2) throws Z3Exception |
static int | openLog (String a0) |
static void | appendLog (String a0) |
static void | closeLog () |
static void | toggleWarningMessages (boolean a0) |
static void | setAstPrintMode (long a0, int a1) throws Z3Exception |
static String | astToString (long a0, long a1) throws Z3Exception |
static String | patternToString (long a0, long a1) throws Z3Exception |
static String | sortToString (long a0, long a1) throws Z3Exception |
static String | funcDeclToString (long a0, long a1) throws Z3Exception |
static String | modelToString (long a0, long a1) throws Z3Exception |
static String | benchmarkToSmtlibString (long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7) throws Z3Exception |
static long | parseSmtlib2String (long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7) throws Z3Exception |
static long | parseSmtlib2File (long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7) throws Z3Exception |
static String | evalSmtlib2String (long a0, String a1) throws Z3Exception |
static int | getErrorCode (long a0) throws Z3Exception |
static void | setError (long a0, int a1) throws Z3Exception |
static String | getErrorMsg (long a0, int a1) throws Z3Exception |
static void | getVersion (IntPtr a0, IntPtr a1, IntPtr a2, IntPtr a3) |
static String | getFullVersion () |
static void | enableTrace (String a0) |
static void | disableTrace (String a0) |
static void | resetMemory () |
static void | finalizeMemory () |
static long | mkGoal (long a0, boolean a1, boolean a2, boolean a3) throws Z3Exception |
static void | goalIncRef (long a0, long a1) throws Z3Exception |
static void | goalDecRef (long a0, long a1) throws Z3Exception |
static int | goalPrecision (long a0, long a1) throws Z3Exception |
static void | goalAssert (long a0, long a1, long a2) throws Z3Exception |
static boolean | goalInconsistent (long a0, long a1) throws Z3Exception |
static int | goalDepth (long a0, long a1) throws Z3Exception |
static void | goalReset (long a0, long a1) throws Z3Exception |
static int | goalSize (long a0, long a1) throws Z3Exception |
static long | goalFormula (long a0, long a1, int a2) throws Z3Exception |
static int | goalNumExprs (long a0, long a1) throws Z3Exception |
static boolean | goalIsDecidedSat (long a0, long a1) throws Z3Exception |
static boolean | goalIsDecidedUnsat (long a0, long a1) throws Z3Exception |
static long | goalTranslate (long a0, long a1, long a2) throws Z3Exception |
static long | goalConvertModel (long a0, long a1, long a2) throws Z3Exception |
static String | goalToString (long a0, long a1) throws Z3Exception |
static String | goalToDimacsString (long a0, long a1) throws Z3Exception |
static long | mkTactic (long a0, String a1) throws Z3Exception |
static void | tacticIncRef (long a0, long a1) throws Z3Exception |
static void | tacticDecRef (long a0, long a1) throws Z3Exception |
static long | mkProbe (long a0, String a1) throws Z3Exception |
static void | probeIncRef (long a0, long a1) throws Z3Exception |
static void | probeDecRef (long a0, long a1) throws Z3Exception |
static long | tacticAndThen (long a0, long a1, long a2) throws Z3Exception |
static long | tacticOrElse (long a0, long a1, long a2) throws Z3Exception |
static long | tacticParOr (long a0, int a1, long[] a2) throws Z3Exception |
static long | tacticParAndThen (long a0, long a1, long a2) throws Z3Exception |
static long | tacticTryFor (long a0, long a1, int a2) throws Z3Exception |
static long | tacticWhen (long a0, long a1, long a2) throws Z3Exception |
static long | tacticCond (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | tacticRepeat (long a0, long a1, int a2) throws Z3Exception |
static long | tacticSkip (long a0) throws Z3Exception |
static long | tacticFail (long a0) throws Z3Exception |
static long | tacticFailIf (long a0, long a1) throws Z3Exception |
static long | tacticFailIfNotDecided (long a0) throws Z3Exception |
static long | tacticUsingParams (long a0, long a1, long a2) throws Z3Exception |
static long | probeConst (long a0, double a1) throws Z3Exception |
static long | probeLt (long a0, long a1, long a2) throws Z3Exception |
static long | probeGt (long a0, long a1, long a2) throws Z3Exception |
static long | probeLe (long a0, long a1, long a2) throws Z3Exception |
static long | probeGe (long a0, long a1, long a2) throws Z3Exception |
static long | probeEq (long a0, long a1, long a2) throws Z3Exception |
static long | probeAnd (long a0, long a1, long a2) throws Z3Exception |
static long | probeOr (long a0, long a1, long a2) throws Z3Exception |
static long | probeNot (long a0, long a1) throws Z3Exception |
static int | getNumTactics (long a0) throws Z3Exception |
static String | getTacticName (long a0, int a1) throws Z3Exception |
static int | getNumProbes (long a0) throws Z3Exception |
static String | getProbeName (long a0, int a1) throws Z3Exception |
static String | tacticGetHelp (long a0, long a1) throws Z3Exception |
static long | tacticGetParamDescrs (long a0, long a1) throws Z3Exception |
static String | tacticGetDescr (long a0, String a1) throws Z3Exception |
static String | probeGetDescr (long a0, String a1) throws Z3Exception |
static double | probeApply (long a0, long a1, long a2) throws Z3Exception |
static long | tacticApply (long a0, long a1, long a2) throws Z3Exception |
static long | tacticApplyEx (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | applyResultIncRef (long a0, long a1) throws Z3Exception |
static void | applyResultDecRef (long a0, long a1) throws Z3Exception |
static String | applyResultToString (long a0, long a1) throws Z3Exception |
static int | applyResultGetNumSubgoals (long a0, long a1) throws Z3Exception |
static long | applyResultGetSubgoal (long a0, long a1, int a2) throws Z3Exception |
static long | mkSolver (long a0) throws Z3Exception |
static long | mkSimpleSolver (long a0) throws Z3Exception |
static long | mkSolverForLogic (long a0, long a1) throws Z3Exception |
static long | mkSolverFromTactic (long a0, long a1) throws Z3Exception |
static long | solverTranslate (long a0, long a1, long a2) throws Z3Exception |
static void | solverImportModelConverter (long a0, long a1, long a2) throws Z3Exception |
static String | solverGetHelp (long a0, long a1) throws Z3Exception |
static long | solverGetParamDescrs (long a0, long a1) throws Z3Exception |
static void | solverSetParams (long a0, long a1, long a2) throws Z3Exception |
static void | solverIncRef (long a0, long a1) throws Z3Exception |
static void | solverDecRef (long a0, long a1) throws Z3Exception |
static void | solverInterrupt (long a0, long a1) throws Z3Exception |
static void | solverPush (long a0, long a1) throws Z3Exception |
static void | solverPop (long a0, long a1, int a2) throws Z3Exception |
static void | solverReset (long a0, long a1) throws Z3Exception |
static int | solverGetNumScopes (long a0, long a1) throws Z3Exception |
static void | solverAssert (long a0, long a1, long a2) throws Z3Exception |
static void | solverAssertAndTrack (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | solverFromFile (long a0, long a1, String a2) throws Z3Exception |
static void | solverFromString (long a0, long a1, String a2) throws Z3Exception |
static long | solverGetAssertions (long a0, long a1) throws Z3Exception |
static long | solverGetUnits (long a0, long a1) throws Z3Exception |
static long | solverGetTrail (long a0, long a1) throws Z3Exception |
static long | solverGetNonUnits (long a0, long a1) throws Z3Exception |
static void | solverGetLevels (long a0, long a1, long a2, int a3, int[] a4) throws Z3Exception |
static int | solverCheck (long a0, long a1) throws Z3Exception |
static int | solverCheckAssumptions (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static int | getImpliedEqualities (long a0, long a1, int a2, long[] a3, int[] a4) throws Z3Exception |
static int | solverGetConsequences (long a0, long a1, long a2, long a3, long a4) throws Z3Exception |
static long | solverCube (long a0, long a1, long a2, int a3) throws Z3Exception |
static long | solverGetModel (long a0, long a1) throws Z3Exception |
static long | solverGetProof (long a0, long a1) throws Z3Exception |
static long | solverGetUnsatCore (long a0, long a1) throws Z3Exception |
static String | solverGetReasonUnknown (long a0, long a1) throws Z3Exception |
static long | solverGetStatistics (long a0, long a1) throws Z3Exception |
static String | solverToString (long a0, long a1) throws Z3Exception |
static String | solverToDimacsString (long a0, long a1) throws Z3Exception |
static String | statsToString (long a0, long a1) throws Z3Exception |
static void | statsIncRef (long a0, long a1) throws Z3Exception |
static void | statsDecRef (long a0, long a1) throws Z3Exception |
static int | statsSize (long a0, long a1) throws Z3Exception |
static String | statsGetKey (long a0, long a1, int a2) throws Z3Exception |
static boolean | statsIsUint (long a0, long a1, int a2) throws Z3Exception |
static boolean | statsIsDouble (long a0, long a1, int a2) throws Z3Exception |
static int | statsGetUintValue (long a0, long a1, int a2) throws Z3Exception |
static double | statsGetDoubleValue (long a0, long a1, int a2) throws Z3Exception |
static long | getEstimatedAllocSize () |
static long | mkAstVector (long a0) throws Z3Exception |
static void | astVectorIncRef (long a0, long a1) throws Z3Exception |
static void | astVectorDecRef (long a0, long a1) throws Z3Exception |
static int | astVectorSize (long a0, long a1) throws Z3Exception |
static long | astVectorGet (long a0, long a1, int a2) throws Z3Exception |
static void | astVectorSet (long a0, long a1, int a2, long a3) throws Z3Exception |
static void | astVectorResize (long a0, long a1, int a2) throws Z3Exception |
static void | astVectorPush (long a0, long a1, long a2) throws Z3Exception |
static long | astVectorTranslate (long a0, long a1, long a2) throws Z3Exception |
static String | astVectorToString (long a0, long a1) throws Z3Exception |
static long | mkAstMap (long a0) throws Z3Exception |
static void | astMapIncRef (long a0, long a1) throws Z3Exception |
static void | astMapDecRef (long a0, long a1) throws Z3Exception |
static boolean | astMapContains (long a0, long a1, long a2) throws Z3Exception |
static long | astMapFind (long a0, long a1, long a2) throws Z3Exception |
static void | astMapInsert (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | astMapErase (long a0, long a1, long a2) throws Z3Exception |
static void | astMapReset (long a0, long a1) throws Z3Exception |
static int | astMapSize (long a0, long a1) throws Z3Exception |
static long | astMapKeys (long a0, long a1) throws Z3Exception |
static String | astMapToString (long a0, long a1) throws Z3Exception |
static boolean | algebraicIsValue (long a0, long a1) throws Z3Exception |
static boolean | algebraicIsPos (long a0, long a1) throws Z3Exception |
static boolean | algebraicIsNeg (long a0, long a1) throws Z3Exception |
static boolean | algebraicIsZero (long a0, long a1) throws Z3Exception |
static int | algebraicSign (long a0, long a1) throws Z3Exception |
static long | algebraicAdd (long a0, long a1, long a2) throws Z3Exception |
static long | algebraicSub (long a0, long a1, long a2) throws Z3Exception |
static long | algebraicMul (long a0, long a1, long a2) throws Z3Exception |
static long | algebraicDiv (long a0, long a1, long a2) throws Z3Exception |
static long | algebraicRoot (long a0, long a1, int a2) throws Z3Exception |
static long | algebraicPower (long a0, long a1, int a2) throws Z3Exception |
static boolean | algebraicLt (long a0, long a1, long a2) throws Z3Exception |
static boolean | algebraicGt (long a0, long a1, long a2) throws Z3Exception |
static boolean | algebraicLe (long a0, long a1, long a2) throws Z3Exception |
static boolean | algebraicGe (long a0, long a1, long a2) throws Z3Exception |
static boolean | algebraicEq (long a0, long a1, long a2) throws Z3Exception |
static boolean | algebraicNeq (long a0, long a1, long a2) throws Z3Exception |
static long | algebraicRoots (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static int | algebraicEval (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | polynomialSubresultants (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | rcfDel (long a0, long a1) throws Z3Exception |
static long | rcfMkRational (long a0, String a1) throws Z3Exception |
static long | rcfMkSmallInt (long a0, int a1) throws Z3Exception |
static long | rcfMkPi (long a0) throws Z3Exception |
static long | rcfMkE (long a0) throws Z3Exception |
static long | rcfMkInfinitesimal (long a0) throws Z3Exception |
static int | rcfMkRoots (long a0, int a1, long[] a2, long[] a3) throws Z3Exception |
static long | rcfAdd (long a0, long a1, long a2) throws Z3Exception |
static long | rcfSub (long a0, long a1, long a2) throws Z3Exception |
static long | rcfMul (long a0, long a1, long a2) throws Z3Exception |
static long | rcfDiv (long a0, long a1, long a2) throws Z3Exception |
static long | rcfNeg (long a0, long a1) throws Z3Exception |
static long | rcfInv (long a0, long a1) throws Z3Exception |
static long | rcfPower (long a0, long a1, int a2) throws Z3Exception |
static boolean | rcfLt (long a0, long a1, long a2) throws Z3Exception |
static boolean | rcfGt (long a0, long a1, long a2) throws Z3Exception |
static boolean | rcfLe (long a0, long a1, long a2) throws Z3Exception |
static boolean | rcfGe (long a0, long a1, long a2) throws Z3Exception |
static boolean | rcfEq (long a0, long a1, long a2) throws Z3Exception |
static boolean | rcfNeq (long a0, long a1, long a2) throws Z3Exception |
static String | rcfNumToString (long a0, long a1, boolean a2, boolean a3) throws Z3Exception |
static String | rcfNumToDecimalString (long a0, long a1, int a2) throws Z3Exception |
static void | rcfGetNumeratorDenominator (long a0, long a1, LongPtr a2, LongPtr a3) throws Z3Exception |
static long | mkFixedpoint (long a0) throws Z3Exception |
static void | fixedpointIncRef (long a0, long a1) throws Z3Exception |
static void | fixedpointDecRef (long a0, long a1) throws Z3Exception |
static void | fixedpointAddRule (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | fixedpointAddFact (long a0, long a1, long a2, int a3, int[] a4) throws Z3Exception |
static void | fixedpointAssert (long a0, long a1, long a2) throws Z3Exception |
static int | fixedpointQuery (long a0, long a1, long a2) throws Z3Exception |
static int | fixedpointQueryRelations (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | fixedpointGetAnswer (long a0, long a1) throws Z3Exception |
static String | fixedpointGetReasonUnknown (long a0, long a1) throws Z3Exception |
static void | fixedpointUpdateRule (long a0, long a1, long a2, long a3) throws Z3Exception |
static int | fixedpointGetNumLevels (long a0, long a1, long a2) throws Z3Exception |
static long | fixedpointGetCoverDelta (long a0, long a1, int a2, long a3) throws Z3Exception |
static void | fixedpointAddCover (long a0, long a1, int a2, long a3, long a4) throws Z3Exception |
static long | fixedpointGetStatistics (long a0, long a1) throws Z3Exception |
static void | fixedpointRegisterRelation (long a0, long a1, long a2) throws Z3Exception |
static void | fixedpointSetPredicateRepresentation (long a0, long a1, long a2, int a3, long[] a4) throws Z3Exception |
static long | fixedpointGetRules (long a0, long a1) throws Z3Exception |
static long | fixedpointGetAssertions (long a0, long a1) throws Z3Exception |
static void | fixedpointSetParams (long a0, long a1, long a2) throws Z3Exception |
static String | fixedpointGetHelp (long a0, long a1) throws Z3Exception |
static long | fixedpointGetParamDescrs (long a0, long a1) throws Z3Exception |
static String | fixedpointToString (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | fixedpointFromString (long a0, long a1, String a2) throws Z3Exception |
static long | fixedpointFromFile (long a0, long a1, String a2) throws Z3Exception |
static long | mkOptimize (long a0) throws Z3Exception |
static void | optimizeIncRef (long a0, long a1) throws Z3Exception |
static void | optimizeDecRef (long a0, long a1) throws Z3Exception |
static void | optimizeAssert (long a0, long a1, long a2) throws Z3Exception |
static void | optimizeAssertAndTrack (long a0, long a1, long a2, long a3) throws Z3Exception |
static int | optimizeAssertSoft (long a0, long a1, long a2, String a3, long a4) throws Z3Exception |
static int | optimizeMaximize (long a0, long a1, long a2) throws Z3Exception |
static int | optimizeMinimize (long a0, long a1, long a2) throws Z3Exception |
static void | optimizePush (long a0, long a1) throws Z3Exception |
static void | optimizePop (long a0, long a1) throws Z3Exception |
static int | optimizeCheck (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static String | optimizeGetReasonUnknown (long a0, long a1) throws Z3Exception |
static long | optimizeGetModel (long a0, long a1) throws Z3Exception |
static long | optimizeGetUnsatCore (long a0, long a1) throws Z3Exception |
static void | optimizeSetParams (long a0, long a1, long a2) throws Z3Exception |
static long | optimizeGetParamDescrs (long a0, long a1) throws Z3Exception |
static long | optimizeGetLower (long a0, long a1, int a2) throws Z3Exception |
static long | optimizeGetUpper (long a0, long a1, int a2) throws Z3Exception |
static long | optimizeGetLowerAsVector (long a0, long a1, int a2) throws Z3Exception |
static long | optimizeGetUpperAsVector (long a0, long a1, int a2) throws Z3Exception |
static String | optimizeToString (long a0, long a1) throws Z3Exception |
static void | optimizeFromString (long a0, long a1, String a2) throws Z3Exception |
static void | optimizeFromFile (long a0, long a1, String a2) throws Z3Exception |
static String | optimizeGetHelp (long a0, long a1) throws Z3Exception |
static long | optimizeGetStatistics (long a0, long a1) throws Z3Exception |
static long | optimizeGetAssertions (long a0, long a1) throws Z3Exception |
static long | optimizeGetObjectives (long a0, long a1) throws Z3Exception |
static long | mkFpaRoundingModeSort (long a0) throws Z3Exception |
static long | mkFpaRoundNearestTiesToEven (long a0) throws Z3Exception |
static long | mkFpaRne (long a0) throws Z3Exception |
static long | mkFpaRoundNearestTiesToAway (long a0) throws Z3Exception |
static long | mkFpaRna (long a0) throws Z3Exception |
static long | mkFpaRoundTowardPositive (long a0) throws Z3Exception |
static long | mkFpaRtp (long a0) throws Z3Exception |
static long | mkFpaRoundTowardNegative (long a0) throws Z3Exception |
static long | mkFpaRtn (long a0) throws Z3Exception |
static long | mkFpaRoundTowardZero (long a0) throws Z3Exception |
static long | mkFpaRtz (long a0) throws Z3Exception |
static long | mkFpaSort (long a0, int a1, int a2) throws Z3Exception |
static long | mkFpaSortHalf (long a0) throws Z3Exception |
static long | mkFpaSort16 (long a0) throws Z3Exception |
static long | mkFpaSortSingle (long a0) throws Z3Exception |
static long | mkFpaSort32 (long a0) throws Z3Exception |
static long | mkFpaSortDouble (long a0) throws Z3Exception |
static long | mkFpaSort64 (long a0) throws Z3Exception |
static long | mkFpaSortQuadruple (long a0) throws Z3Exception |
static long | mkFpaSort128 (long a0) throws Z3Exception |
static long | mkFpaNan (long a0, long a1) throws Z3Exception |
static long | mkFpaInf (long a0, long a1, boolean a2) throws Z3Exception |
static long | mkFpaZero (long a0, long a1, boolean a2) throws Z3Exception |
static long | mkFpaFp (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaNumeralFloat (long a0, float a1, long a2) throws Z3Exception |
static long | mkFpaNumeralDouble (long a0, double a1, long a2) throws Z3Exception |
static long | mkFpaNumeralInt (long a0, int a1, long a2) throws Z3Exception |
static long | mkFpaNumeralIntUint (long a0, boolean a1, int a2, int a3, long a4) throws Z3Exception |
static long | mkFpaNumeralInt64Uint64 (long a0, boolean a1, long a2, long a3, long a4) throws Z3Exception |
static long | mkFpaAbs (long a0, long a1) throws Z3Exception |
static long | mkFpaNeg (long a0, long a1) throws Z3Exception |
static long | mkFpaAdd (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaSub (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaMul (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaDiv (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaFma (long a0, long a1, long a2, long a3, long a4) throws Z3Exception |
static long | mkFpaSqrt (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaRem (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaRoundToIntegral (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaMin (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaMax (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaLeq (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaLt (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaGeq (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaGt (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaEq (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaIsNormal (long a0, long a1) throws Z3Exception |
static long | mkFpaIsSubnormal (long a0, long a1) throws Z3Exception |
static long | mkFpaIsZero (long a0, long a1) throws Z3Exception |
static long | mkFpaIsInfinite (long a0, long a1) throws Z3Exception |
static long | mkFpaIsNan (long a0, long a1) throws Z3Exception |
static long | mkFpaIsNegative (long a0, long a1) throws Z3Exception |
static long | mkFpaIsPositive (long a0, long a1) throws Z3Exception |
static long | mkFpaToFpBv (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaToFpFloat (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaToFpReal (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaToFpSigned (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaToFpUnsigned (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaToUbv (long a0, long a1, long a2, int a3) throws Z3Exception |
static long | mkFpaToSbv (long a0, long a1, long a2, int a3) throws Z3Exception |
static long | mkFpaToReal (long a0, long a1) throws Z3Exception |
static int | fpaGetEbits (long a0, long a1) throws Z3Exception |
static int | fpaGetSbits (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralNan (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralInf (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralZero (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralNormal (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralSubnormal (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralPositive (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralNegative (long a0, long a1) throws Z3Exception |
static long | fpaGetNumeralSignBv (long a0, long a1) throws Z3Exception |
static long | fpaGetNumeralSignificandBv (long a0, long a1) throws Z3Exception |
static boolean | fpaGetNumeralSign (long a0, long a1, IntPtr a2) throws Z3Exception |
static String | fpaGetNumeralSignificandString (long a0, long a1) throws Z3Exception |
static boolean | fpaGetNumeralSignificandUint64 (long a0, long a1, LongPtr a2) throws Z3Exception |
static String | fpaGetNumeralExponentString (long a0, long a1, boolean a2) throws Z3Exception |
static boolean | fpaGetNumeralExponentInt64 (long a0, long a1, LongPtr a2, boolean a3) throws Z3Exception |
static long | fpaGetNumeralExponentBv (long a0, long a1, boolean a2) throws Z3Exception |
static long | mkFpaToIeeeBv (long a0, long a1) throws Z3Exception |
static long | mkFpaToFpIntReal (long a0, long a1, long a2, long a3, long a4) throws Z3Exception |
static int | fixedpointQueryFromLvl (long a0, long a1, long a2, int a3) throws Z3Exception |
static long | fixedpointGetGroundSatAnswer (long a0, long a1) throws Z3Exception |
static long | fixedpointGetRulesAlongTrace (long a0, long a1) throws Z3Exception |
static long | fixedpointGetRuleNamesAlongTrace (long a0, long a1) throws Z3Exception |
static void | fixedpointAddInvariant (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | fixedpointGetReachable (long a0, long a1, long a2) throws Z3Exception |
static long | qeModelProject (long a0, long a1, int a2, long[] a3, long a4) throws Z3Exception |
static long | qeModelProjectSkolem (long a0, long a1, int a2, long[] a3, long a4, long a5) throws Z3Exception |
static long | modelExtrapolate (long a0, long a1, long a2) throws Z3Exception |
static long | qeLite (long a0, long a1, long a2) throws Z3Exception |
Static Protected Member Functions | |
static native void | INTERNALglobalParamSet (String a0, String a1) |
static native void | INTERNALglobalParamResetAll () |
static native boolean | INTERNALglobalParamGet (String a0, StringPtr a1) |
static native long | INTERNALmkConfig () |
static native void | INTERNALdelConfig (long a0) |
static native void | INTERNALsetParamValue (long a0, String a1, String a2) |
static native long | INTERNALmkContext (long a0) |
static native long | INTERNALmkContextRc (long a0) |
static native void | INTERNALdelContext (long a0) |
static native void | INTERNALincRef (long a0, long a1) |
static native void | INTERNALdecRef (long a0, long a1) |
static native void | INTERNALupdateParamValue (long a0, String a1, String a2) |
static native void | INTERNALinterrupt (long a0) |
static native long | INTERNALmkParams (long a0) |
static native void | INTERNALparamsIncRef (long a0, long a1) |
static native void | INTERNALparamsDecRef (long a0, long a1) |
static native void | INTERNALparamsSetBool (long a0, long a1, long a2, boolean a3) |
static native void | INTERNALparamsSetUint (long a0, long a1, long a2, int a3) |
static native void | INTERNALparamsSetDouble (long a0, long a1, long a2, double a3) |
static native void | INTERNALparamsSetSymbol (long a0, long a1, long a2, long a3) |
static native String | INTERNALparamsToString (long a0, long a1) |
static native void | INTERNALparamsValidate (long a0, long a1, long a2) |
static native void | INTERNALparamDescrsIncRef (long a0, long a1) |
static native void | INTERNALparamDescrsDecRef (long a0, long a1) |
static native int | INTERNALparamDescrsGetKind (long a0, long a1, long a2) |
static native int | INTERNALparamDescrsSize (long a0, long a1) |
static native long | INTERNALparamDescrsGetName (long a0, long a1, int a2) |
static native String | INTERNALparamDescrsGetDocumentation (long a0, long a1, long a2) |
static native String | INTERNALparamDescrsToString (long a0, long a1) |
static native long | INTERNALmkIntSymbol (long a0, int a1) |
static native long | INTERNALmkStringSymbol (long a0, String a1) |
static native long | INTERNALmkUninterpretedSort (long a0, long a1) |
static native long | INTERNALmkBoolSort (long a0) |
static native long | INTERNALmkIntSort (long a0) |
static native long | INTERNALmkRealSort (long a0) |
static native long | INTERNALmkBvSort (long a0, int a1) |
static native long | INTERNALmkFiniteDomainSort (long a0, long a1, long a2) |
static native long | INTERNALmkArraySort (long a0, long a1, long a2) |
static native long | INTERNALmkArraySortN (long a0, int a1, long[] a2, long a3) |
static native long | INTERNALmkTupleSort (long a0, long a1, int a2, long[] a3, long[] a4, LongPtr a5, long[] a6) |
static native long | INTERNALmkEnumerationSort (long a0, long a1, int a2, long[] a3, long[] a4, long[] a5) |
static native long | INTERNALmkListSort (long a0, long a1, long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8) |
static native long | INTERNALmkConstructor (long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6) |
static native void | INTERNALdelConstructor (long a0, long a1) |
static native long | INTERNALmkDatatype (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALmkConstructorList (long a0, int a1, long[] a2) |
static native void | INTERNALdelConstructorList (long a0, long a1) |
static native void | INTERNALmkDatatypes (long a0, int a1, long[] a2, long[] a3, long[] a4) |
static native void | INTERNALqueryConstructor (long a0, long a1, int a2, LongPtr a3, LongPtr a4, long[] a5) |
static native long | INTERNALmkFuncDecl (long a0, long a1, int a2, long[] a3, long a4) |
static native long | INTERNALmkApp (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALmkConst (long a0, long a1, long a2) |
static native long | INTERNALmkFreshFuncDecl (long a0, String a1, int a2, long[] a3, long a4) |
static native long | INTERNALmkFreshConst (long a0, String a1, long a2) |
static native long | INTERNALmkRecFuncDecl (long a0, long a1, int a2, long[] a3, long a4) |
static native void | INTERNALaddRecDef (long a0, long a1, int a2, long[] a3, long a4) |
static native long | INTERNALmkTrue (long a0) |
static native long | INTERNALmkFalse (long a0) |
static native long | INTERNALmkEq (long a0, long a1, long a2) |
static native long | INTERNALmkDistinct (long a0, int a1, long[] a2) |
static native long | INTERNALmkNot (long a0, long a1) |
static native long | INTERNALmkIte (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkIff (long a0, long a1, long a2) |
static native long | INTERNALmkImplies (long a0, long a1, long a2) |
static native long | INTERNALmkXor (long a0, long a1, long a2) |
static native long | INTERNALmkAnd (long a0, int a1, long[] a2) |
static native long | INTERNALmkOr (long a0, int a1, long[] a2) |
static native long | INTERNALmkAdd (long a0, int a1, long[] a2) |
static native long | INTERNALmkMul (long a0, int a1, long[] a2) |
static native long | INTERNALmkSub (long a0, int a1, long[] a2) |
static native long | INTERNALmkUnaryMinus (long a0, long a1) |
static native long | INTERNALmkDiv (long a0, long a1, long a2) |
static native long | INTERNALmkMod (long a0, long a1, long a2) |
static native long | INTERNALmkRem (long a0, long a1, long a2) |
static native long | INTERNALmkPower (long a0, long a1, long a2) |
static native long | INTERNALmkLt (long a0, long a1, long a2) |
static native long | INTERNALmkLe (long a0, long a1, long a2) |
static native long | INTERNALmkGt (long a0, long a1, long a2) |
static native long | INTERNALmkGe (long a0, long a1, long a2) |
static native long | INTERNALmkDivides (long a0, long a1, long a2) |
static native long | INTERNALmkInt2real (long a0, long a1) |
static native long | INTERNALmkReal2int (long a0, long a1) |
static native long | INTERNALmkIsInt (long a0, long a1) |
static native long | INTERNALmkBvnot (long a0, long a1) |
static native long | INTERNALmkBvredand (long a0, long a1) |
static native long | INTERNALmkBvredor (long a0, long a1) |
static native long | INTERNALmkBvand (long a0, long a1, long a2) |
static native long | INTERNALmkBvor (long a0, long a1, long a2) |
static native long | INTERNALmkBvxor (long a0, long a1, long a2) |
static native long | INTERNALmkBvnand (long a0, long a1, long a2) |
static native long | INTERNALmkBvnor (long a0, long a1, long a2) |
static native long | INTERNALmkBvxnor (long a0, long a1, long a2) |
static native long | INTERNALmkBvneg (long a0, long a1) |
static native long | INTERNALmkBvadd (long a0, long a1, long a2) |
static native long | INTERNALmkBvsub (long a0, long a1, long a2) |
static native long | INTERNALmkBvmul (long a0, long a1, long a2) |
static native long | INTERNALmkBvudiv (long a0, long a1, long a2) |
static native long | INTERNALmkBvsdiv (long a0, long a1, long a2) |
static native long | INTERNALmkBvurem (long a0, long a1, long a2) |
static native long | INTERNALmkBvsrem (long a0, long a1, long a2) |
static native long | INTERNALmkBvsmod (long a0, long a1, long a2) |
static native long | INTERNALmkBvult (long a0, long a1, long a2) |
static native long | INTERNALmkBvslt (long a0, long a1, long a2) |
static native long | INTERNALmkBvule (long a0, long a1, long a2) |
static native long | INTERNALmkBvsle (long a0, long a1, long a2) |
static native long | INTERNALmkBvuge (long a0, long a1, long a2) |
static native long | INTERNALmkBvsge (long a0, long a1, long a2) |
static native long | INTERNALmkBvugt (long a0, long a1, long a2) |
static native long | INTERNALmkBvsgt (long a0, long a1, long a2) |
static native long | INTERNALmkConcat (long a0, long a1, long a2) |
static native long | INTERNALmkExtract (long a0, int a1, int a2, long a3) |
static native long | INTERNALmkSignExt (long a0, int a1, long a2) |
static native long | INTERNALmkZeroExt (long a0, int a1, long a2) |
static native long | INTERNALmkRepeat (long a0, int a1, long a2) |
static native long | INTERNALmkBvshl (long a0, long a1, long a2) |
static native long | INTERNALmkBvlshr (long a0, long a1, long a2) |
static native long | INTERNALmkBvashr (long a0, long a1, long a2) |
static native long | INTERNALmkRotateLeft (long a0, int a1, long a2) |
static native long | INTERNALmkRotateRight (long a0, int a1, long a2) |
static native long | INTERNALmkExtRotateLeft (long a0, long a1, long a2) |
static native long | INTERNALmkExtRotateRight (long a0, long a1, long a2) |
static native long | INTERNALmkInt2bv (long a0, int a1, long a2) |
static native long | INTERNALmkBv2int (long a0, long a1, boolean a2) |
static native long | INTERNALmkBvaddNoOverflow (long a0, long a1, long a2, boolean a3) |
static native long | INTERNALmkBvaddNoUnderflow (long a0, long a1, long a2) |
static native long | INTERNALmkBvsubNoOverflow (long a0, long a1, long a2) |
static native long | INTERNALmkBvsubNoUnderflow (long a0, long a1, long a2, boolean a3) |
static native long | INTERNALmkBvsdivNoOverflow (long a0, long a1, long a2) |
static native long | INTERNALmkBvnegNoOverflow (long a0, long a1) |
static native long | INTERNALmkBvmulNoOverflow (long a0, long a1, long a2, boolean a3) |
static native long | INTERNALmkBvmulNoUnderflow (long a0, long a1, long a2) |
static native long | INTERNALmkSelect (long a0, long a1, long a2) |
static native long | INTERNALmkSelectN (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALmkStore (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkStoreN (long a0, long a1, int a2, long[] a3, long a4) |
static native long | INTERNALmkConstArray (long a0, long a1, long a2) |
static native long | INTERNALmkMap (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALmkArrayDefault (long a0, long a1) |
static native long | INTERNALmkAsArray (long a0, long a1) |
static native long | INTERNALmkSetHasSize (long a0, long a1, long a2) |
static native long | INTERNALmkSetSort (long a0, long a1) |
static native long | INTERNALmkEmptySet (long a0, long a1) |
static native long | INTERNALmkFullSet (long a0, long a1) |
static native long | INTERNALmkSetAdd (long a0, long a1, long a2) |
static native long | INTERNALmkSetDel (long a0, long a1, long a2) |
static native long | INTERNALmkSetUnion (long a0, int a1, long[] a2) |
static native long | INTERNALmkSetIntersect (long a0, int a1, long[] a2) |
static native long | INTERNALmkSetDifference (long a0, long a1, long a2) |
static native long | INTERNALmkSetComplement (long a0, long a1) |
static native long | INTERNALmkSetMember (long a0, long a1, long a2) |
static native long | INTERNALmkSetSubset (long a0, long a1, long a2) |
static native long | INTERNALmkArrayExt (long a0, long a1, long a2) |
static native long | INTERNALmkNumeral (long a0, String a1, long a2) |
static native long | INTERNALmkReal (long a0, int a1, int a2) |
static native long | INTERNALmkInt (long a0, int a1, long a2) |
static native long | INTERNALmkUnsignedInt (long a0, int a1, long a2) |
static native long | INTERNALmkInt64 (long a0, long a1, long a2) |
static native long | INTERNALmkUnsignedInt64 (long a0, long a1, long a2) |
static native long | INTERNALmkBvNumeral (long a0, int a1, boolean[] a2) |
static native long | INTERNALmkSeqSort (long a0, long a1) |
static native boolean | INTERNALisSeqSort (long a0, long a1) |
static native long | INTERNALgetSeqSortBasis (long a0, long a1) |
static native long | INTERNALmkReSort (long a0, long a1) |
static native boolean | INTERNALisReSort (long a0, long a1) |
static native long | INTERNALgetReSortBasis (long a0, long a1) |
static native long | INTERNALmkStringSort (long a0) |
static native boolean | INTERNALisStringSort (long a0, long a1) |
static native long | INTERNALmkString (long a0, String a1) |
static native long | INTERNALmkLstring (long a0, int a1, String a2) |
static native boolean | INTERNALisString (long a0, long a1) |
static native String | INTERNALgetString (long a0, long a1) |
static native String | INTERNALgetLstring (long a0, long a1, IntPtr a2) |
static native long | INTERNALmkSeqEmpty (long a0, long a1) |
static native long | INTERNALmkSeqUnit (long a0, long a1) |
static native long | INTERNALmkSeqConcat (long a0, int a1, long[] a2) |
static native long | INTERNALmkSeqPrefix (long a0, long a1, long a2) |
static native long | INTERNALmkSeqSuffix (long a0, long a1, long a2) |
static native long | INTERNALmkSeqContains (long a0, long a1, long a2) |
static native long | INTERNALmkStrLt (long a0, long a1, long a2) |
static native long | INTERNALmkStrLe (long a0, long a1, long a2) |
static native long | INTERNALmkSeqExtract (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkSeqReplace (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkSeqAt (long a0, long a1, long a2) |
static native long | INTERNALmkSeqNth (long a0, long a1, long a2) |
static native long | INTERNALmkSeqLength (long a0, long a1) |
static native long | INTERNALmkSeqIndex (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkSeqLastIndex (long a0, long a1, long a2) |
static native long | INTERNALmkStrToInt (long a0, long a1) |
static native long | INTERNALmkIntToStr (long a0, long a1) |
static native long | INTERNALmkSeqToRe (long a0, long a1) |
static native long | INTERNALmkSeqInRe (long a0, long a1, long a2) |
static native long | INTERNALmkRePlus (long a0, long a1) |
static native long | INTERNALmkReStar (long a0, long a1) |
static native long | INTERNALmkReOption (long a0, long a1) |
static native long | INTERNALmkReUnion (long a0, int a1, long[] a2) |
static native long | INTERNALmkReConcat (long a0, int a1, long[] a2) |
static native long | INTERNALmkReRange (long a0, long a1, long a2) |
static native long | INTERNALmkReLoop (long a0, long a1, int a2, int a3) |
static native long | INTERNALmkReIntersect (long a0, int a1, long[] a2) |
static native long | INTERNALmkReComplement (long a0, long a1) |
static native long | INTERNALmkReEmpty (long a0, long a1) |
static native long | INTERNALmkReFull (long a0, long a1) |
static native long | INTERNALmkLinearOrder (long a0, long a1, int a2) |
static native long | INTERNALmkPartialOrder (long a0, long a1, int a2) |
static native long | INTERNALmkPiecewiseLinearOrder (long a0, long a1, int a2) |
static native long | INTERNALmkTreeOrder (long a0, long a1, int a2) |
static native long | INTERNALmkTransitiveClosure (long a0, long a1) |
static native long | INTERNALmkPattern (long a0, int a1, long[] a2) |
static native long | INTERNALmkBound (long a0, int a1, long a2) |
static native long | INTERNALmkForall (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7) |
static native long | INTERNALmkExists (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7) |
static native long | INTERNALmkQuantifier (long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8) |
static native long | INTERNALmkQuantifierEx (long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long[] a11, long a12) |
static native long | INTERNALmkForallConst (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6) |
static native long | INTERNALmkExistsConst (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6) |
static native long | INTERNALmkQuantifierConst (long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7) |
static native long | INTERNALmkQuantifierConstEx (long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long a11) |
static native long | INTERNALmkLambda (long a0, int a1, long[] a2, long[] a3, long a4) |
static native long | INTERNALmkLambdaConst (long a0, int a1, long[] a2, long a3) |
static native int | INTERNALgetSymbolKind (long a0, long a1) |
static native int | INTERNALgetSymbolInt (long a0, long a1) |
static native String | INTERNALgetSymbolString (long a0, long a1) |
static native long | INTERNALgetSortName (long a0, long a1) |
static native int | INTERNALgetSortId (long a0, long a1) |
static native long | INTERNALsortToAst (long a0, long a1) |
static native boolean | INTERNALisEqSort (long a0, long a1, long a2) |
static native int | INTERNALgetSortKind (long a0, long a1) |
static native int | INTERNALgetBvSortSize (long a0, long a1) |
static native boolean | INTERNALgetFiniteDomainSortSize (long a0, long a1, LongPtr a2) |
static native long | INTERNALgetArraySortDomain (long a0, long a1) |
static native long | INTERNALgetArraySortRange (long a0, long a1) |
static native long | INTERNALgetTupleSortMkDecl (long a0, long a1) |
static native int | INTERNALgetTupleSortNumFields (long a0, long a1) |
static native long | INTERNALgetTupleSortFieldDecl (long a0, long a1, int a2) |
static native int | INTERNALgetDatatypeSortNumConstructors (long a0, long a1) |
static native long | INTERNALgetDatatypeSortConstructor (long a0, long a1, int a2) |
static native long | INTERNALgetDatatypeSortRecognizer (long a0, long a1, int a2) |
static native long | INTERNALgetDatatypeSortConstructorAccessor (long a0, long a1, int a2, int a3) |
static native long | INTERNALdatatypeUpdateField (long a0, long a1, long a2, long a3) |
static native int | INTERNALgetRelationArity (long a0, long a1) |
static native long | INTERNALgetRelationColumn (long a0, long a1, int a2) |
static native long | INTERNALmkAtmost (long a0, int a1, long[] a2, int a3) |
static native long | INTERNALmkAtleast (long a0, int a1, long[] a2, int a3) |
static native long | INTERNALmkPble (long a0, int a1, long[] a2, int[] a3, int a4) |
static native long | INTERNALmkPbge (long a0, int a1, long[] a2, int[] a3, int a4) |
static native long | INTERNALmkPbeq (long a0, int a1, long[] a2, int[] a3, int a4) |
static native long | INTERNALfuncDeclToAst (long a0, long a1) |
static native boolean | INTERNALisEqFuncDecl (long a0, long a1, long a2) |
static native int | INTERNALgetFuncDeclId (long a0, long a1) |
static native long | INTERNALgetDeclName (long a0, long a1) |
static native int | INTERNALgetDeclKind (long a0, long a1) |
static native int | INTERNALgetDomainSize (long a0, long a1) |
static native int | INTERNALgetArity (long a0, long a1) |
static native long | INTERNALgetDomain (long a0, long a1, int a2) |
static native long | INTERNALgetRange (long a0, long a1) |
static native int | INTERNALgetDeclNumParameters (long a0, long a1) |
static native int | INTERNALgetDeclParameterKind (long a0, long a1, int a2) |
static native int | INTERNALgetDeclIntParameter (long a0, long a1, int a2) |
static native double | INTERNALgetDeclDoubleParameter (long a0, long a1, int a2) |
static native long | INTERNALgetDeclSymbolParameter (long a0, long a1, int a2) |
static native long | INTERNALgetDeclSortParameter (long a0, long a1, int a2) |
static native long | INTERNALgetDeclAstParameter (long a0, long a1, int a2) |
static native long | INTERNALgetDeclFuncDeclParameter (long a0, long a1, int a2) |
static native String | INTERNALgetDeclRationalParameter (long a0, long a1, int a2) |
static native long | INTERNALappToAst (long a0, long a1) |
static native long | INTERNALgetAppDecl (long a0, long a1) |
static native int | INTERNALgetAppNumArgs (long a0, long a1) |
static native long | INTERNALgetAppArg (long a0, long a1, int a2) |
static native boolean | INTERNALisEqAst (long a0, long a1, long a2) |
static native int | INTERNALgetAstId (long a0, long a1) |
static native int | INTERNALgetAstHash (long a0, long a1) |
static native long | INTERNALgetSort (long a0, long a1) |
static native boolean | INTERNALisWellSorted (long a0, long a1) |
static native int | INTERNALgetBoolValue (long a0, long a1) |
static native int | INTERNALgetAstKind (long a0, long a1) |
static native boolean | INTERNALisApp (long a0, long a1) |
static native boolean | INTERNALisNumeralAst (long a0, long a1) |
static native boolean | INTERNALisAlgebraicNumber (long a0, long a1) |
static native long | INTERNALtoApp (long a0, long a1) |
static native long | INTERNALtoFuncDecl (long a0, long a1) |
static native String | INTERNALgetNumeralString (long a0, long a1) |
static native String | INTERNALgetNumeralDecimalString (long a0, long a1, int a2) |
static native double | INTERNALgetNumeralDouble (long a0, long a1) |
static native long | INTERNALgetNumerator (long a0, long a1) |
static native long | INTERNALgetDenominator (long a0, long a1) |
static native boolean | INTERNALgetNumeralSmall (long a0, long a1, LongPtr a2, LongPtr a3) |
static native boolean | INTERNALgetNumeralInt (long a0, long a1, IntPtr a2) |
static native boolean | INTERNALgetNumeralUint (long a0, long a1, IntPtr a2) |
static native boolean | INTERNALgetNumeralUint64 (long a0, long a1, LongPtr a2) |
static native boolean | INTERNALgetNumeralInt64 (long a0, long a1, LongPtr a2) |
static native boolean | INTERNALgetNumeralRationalInt64 (long a0, long a1, LongPtr a2, LongPtr a3) |
static native long | INTERNALgetAlgebraicNumberLower (long a0, long a1, int a2) |
static native long | INTERNALgetAlgebraicNumberUpper (long a0, long a1, int a2) |
static native long | INTERNALpatternToAst (long a0, long a1) |
static native int | INTERNALgetPatternNumTerms (long a0, long a1) |
static native long | INTERNALgetPattern (long a0, long a1, int a2) |
static native int | INTERNALgetIndexValue (long a0, long a1) |
static native boolean | INTERNALisQuantifierForall (long a0, long a1) |
static native boolean | INTERNALisQuantifierExists (long a0, long a1) |
static native boolean | INTERNALisLambda (long a0, long a1) |
static native int | INTERNALgetQuantifierWeight (long a0, long a1) |
static native int | INTERNALgetQuantifierNumPatterns (long a0, long a1) |
static native long | INTERNALgetQuantifierPatternAst (long a0, long a1, int a2) |
static native int | INTERNALgetQuantifierNumNoPatterns (long a0, long a1) |
static native long | INTERNALgetQuantifierNoPatternAst (long a0, long a1, int a2) |
static native int | INTERNALgetQuantifierNumBound (long a0, long a1) |
static native long | INTERNALgetQuantifierBoundName (long a0, long a1, int a2) |
static native long | INTERNALgetQuantifierBoundSort (long a0, long a1, int a2) |
static native long | INTERNALgetQuantifierBody (long a0, long a1) |
static native long | INTERNALsimplify (long a0, long a1) |
static native long | INTERNALsimplifyEx (long a0, long a1, long a2) |
static native String | INTERNALsimplifyGetHelp (long a0) |
static native long | INTERNALsimplifyGetParamDescrs (long a0) |
static native long | INTERNALupdateTerm (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALsubstitute (long a0, long a1, int a2, long[] a3, long[] a4) |
static native long | INTERNALsubstituteVars (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALtranslate (long a0, long a1, long a2) |
static native long | INTERNALmkModel (long a0) |
static native void | INTERNALmodelIncRef (long a0, long a1) |
static native void | INTERNALmodelDecRef (long a0, long a1) |
static native boolean | INTERNALmodelEval (long a0, long a1, long a2, boolean a3, LongPtr a4) |
static native long | INTERNALmodelGetConstInterp (long a0, long a1, long a2) |
static native boolean | INTERNALmodelHasInterp (long a0, long a1, long a2) |
static native long | INTERNALmodelGetFuncInterp (long a0, long a1, long a2) |
static native int | INTERNALmodelGetNumConsts (long a0, long a1) |
static native long | INTERNALmodelGetConstDecl (long a0, long a1, int a2) |
static native int | INTERNALmodelGetNumFuncs (long a0, long a1) |
static native long | INTERNALmodelGetFuncDecl (long a0, long a1, int a2) |
static native int | INTERNALmodelGetNumSorts (long a0, long a1) |
static native long | INTERNALmodelGetSort (long a0, long a1, int a2) |
static native long | INTERNALmodelGetSortUniverse (long a0, long a1, long a2) |
static native long | INTERNALmodelTranslate (long a0, long a1, long a2) |
static native boolean | INTERNALisAsArray (long a0, long a1) |
static native long | INTERNALgetAsArrayFuncDecl (long a0, long a1) |
static native long | INTERNALaddFuncInterp (long a0, long a1, long a2, long a3) |
static native void | INTERNALaddConstInterp (long a0, long a1, long a2, long a3) |
static native void | INTERNALfuncInterpIncRef (long a0, long a1) |
static native void | INTERNALfuncInterpDecRef (long a0, long a1) |
static native int | INTERNALfuncInterpGetNumEntries (long a0, long a1) |
static native long | INTERNALfuncInterpGetEntry (long a0, long a1, int a2) |
static native long | INTERNALfuncInterpGetElse (long a0, long a1) |
static native void | INTERNALfuncInterpSetElse (long a0, long a1, long a2) |
static native int | INTERNALfuncInterpGetArity (long a0, long a1) |
static native void | INTERNALfuncInterpAddEntry (long a0, long a1, long a2, long a3) |
static native void | INTERNALfuncEntryIncRef (long a0, long a1) |
static native void | INTERNALfuncEntryDecRef (long a0, long a1) |
static native long | INTERNALfuncEntryGetValue (long a0, long a1) |
static native int | INTERNALfuncEntryGetNumArgs (long a0, long a1) |
static native long | INTERNALfuncEntryGetArg (long a0, long a1, int a2) |
static native int | INTERNALopenLog (String a0) |
static native void | INTERNALappendLog (String a0) |
static native void | INTERNALcloseLog () |
static native void | INTERNALtoggleWarningMessages (boolean a0) |
static native void | INTERNALsetAstPrintMode (long a0, int a1) |
static native String | INTERNALastToString (long a0, long a1) |
static native String | INTERNALpatternToString (long a0, long a1) |
static native String | INTERNALsortToString (long a0, long a1) |
static native String | INTERNALfuncDeclToString (long a0, long a1) |
static native String | INTERNALmodelToString (long a0, long a1) |
static native String | INTERNALbenchmarkToSmtlibString (long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7) |
static native long | INTERNALparseSmtlib2String (long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7) |
static native long | INTERNALparseSmtlib2File (long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7) |
static native String | INTERNALevalSmtlib2String (long a0, String a1) |
static native int | INTERNALgetErrorCode (long a0) |
static native void | INTERNALsetError (long a0, int a1) |
static native String | INTERNALgetErrorMsg (long a0, int a1) |
static native void | INTERNALgetVersion (IntPtr a0, IntPtr a1, IntPtr a2, IntPtr a3) |
static native String | INTERNALgetFullVersion () |
static native void | INTERNALenableTrace (String a0) |
static native void | INTERNALdisableTrace (String a0) |
static native void | INTERNALresetMemory () |
static native void | INTERNALfinalizeMemory () |
static native long | INTERNALmkGoal (long a0, boolean a1, boolean a2, boolean a3) |
static native void | INTERNALgoalIncRef (long a0, long a1) |
static native void | INTERNALgoalDecRef (long a0, long a1) |
static native int | INTERNALgoalPrecision (long a0, long a1) |
static native void | INTERNALgoalAssert (long a0, long a1, long a2) |
static native boolean | INTERNALgoalInconsistent (long a0, long a1) |
static native int | INTERNALgoalDepth (long a0, long a1) |
static native void | INTERNALgoalReset (long a0, long a1) |
static native int | INTERNALgoalSize (long a0, long a1) |
static native long | INTERNALgoalFormula (long a0, long a1, int a2) |
static native int | INTERNALgoalNumExprs (long a0, long a1) |
static native boolean | INTERNALgoalIsDecidedSat (long a0, long a1) |
static native boolean | INTERNALgoalIsDecidedUnsat (long a0, long a1) |
static native long | INTERNALgoalTranslate (long a0, long a1, long a2) |
static native long | INTERNALgoalConvertModel (long a0, long a1, long a2) |
static native String | INTERNALgoalToString (long a0, long a1) |
static native String | INTERNALgoalToDimacsString (long a0, long a1) |
static native long | INTERNALmkTactic (long a0, String a1) |
static native void | INTERNALtacticIncRef (long a0, long a1) |
static native void | INTERNALtacticDecRef (long a0, long a1) |
static native long | INTERNALmkProbe (long a0, String a1) |
static native void | INTERNALprobeIncRef (long a0, long a1) |
static native void | INTERNALprobeDecRef (long a0, long a1) |
static native long | INTERNALtacticAndThen (long a0, long a1, long a2) |
static native long | INTERNALtacticOrElse (long a0, long a1, long a2) |
static native long | INTERNALtacticParOr (long a0, int a1, long[] a2) |
static native long | INTERNALtacticParAndThen (long a0, long a1, long a2) |
static native long | INTERNALtacticTryFor (long a0, long a1, int a2) |
static native long | INTERNALtacticWhen (long a0, long a1, long a2) |
static native long | INTERNALtacticCond (long a0, long a1, long a2, long a3) |
static native long | INTERNALtacticRepeat (long a0, long a1, int a2) |
static native long | INTERNALtacticSkip (long a0) |
static native long | INTERNALtacticFail (long a0) |
static native long | INTERNALtacticFailIf (long a0, long a1) |
static native long | INTERNALtacticFailIfNotDecided (long a0) |
static native long | INTERNALtacticUsingParams (long a0, long a1, long a2) |
static native long | INTERNALprobeConst (long a0, double a1) |
static native long | INTERNALprobeLt (long a0, long a1, long a2) |
static native long | INTERNALprobeGt (long a0, long a1, long a2) |
static native long | INTERNALprobeLe (long a0, long a1, long a2) |
static native long | INTERNALprobeGe (long a0, long a1, long a2) |
static native long | INTERNALprobeEq (long a0, long a1, long a2) |
static native long | INTERNALprobeAnd (long a0, long a1, long a2) |
static native long | INTERNALprobeOr (long a0, long a1, long a2) |
static native long | INTERNALprobeNot (long a0, long a1) |
static native int | INTERNALgetNumTactics (long a0) |
static native String | INTERNALgetTacticName (long a0, int a1) |
static native int | INTERNALgetNumProbes (long a0) |
static native String | INTERNALgetProbeName (long a0, int a1) |
static native String | INTERNALtacticGetHelp (long a0, long a1) |
static native long | INTERNALtacticGetParamDescrs (long a0, long a1) |
static native String | INTERNALtacticGetDescr (long a0, String a1) |
static native String | INTERNALprobeGetDescr (long a0, String a1) |
static native double | INTERNALprobeApply (long a0, long a1, long a2) |
static native long | INTERNALtacticApply (long a0, long a1, long a2) |
static native long | INTERNALtacticApplyEx (long a0, long a1, long a2, long a3) |
static native void | INTERNALapplyResultIncRef (long a0, long a1) |
static native void | INTERNALapplyResultDecRef (long a0, long a1) |
static native String | INTERNALapplyResultToString (long a0, long a1) |
static native int | INTERNALapplyResultGetNumSubgoals (long a0, long a1) |
static native long | INTERNALapplyResultGetSubgoal (long a0, long a1, int a2) |
static native long | INTERNALmkSolver (long a0) |
static native long | INTERNALmkSimpleSolver (long a0) |
static native long | INTERNALmkSolverForLogic (long a0, long a1) |
static native long | INTERNALmkSolverFromTactic (long a0, long a1) |
static native long | INTERNALsolverTranslate (long a0, long a1, long a2) |
static native void | INTERNALsolverImportModelConverter (long a0, long a1, long a2) |
static native String | INTERNALsolverGetHelp (long a0, long a1) |
static native long | INTERNALsolverGetParamDescrs (long a0, long a1) |
static native void | INTERNALsolverSetParams (long a0, long a1, long a2) |
static native void | INTERNALsolverIncRef (long a0, long a1) |
static native void | INTERNALsolverDecRef (long a0, long a1) |
static native void | INTERNALsolverInterrupt (long a0, long a1) |
static native void | INTERNALsolverPush (long a0, long a1) |
static native void | INTERNALsolverPop (long a0, long a1, int a2) |
static native void | INTERNALsolverReset (long a0, long a1) |
static native int | INTERNALsolverGetNumScopes (long a0, long a1) |
static native void | INTERNALsolverAssert (long a0, long a1, long a2) |
static native void | INTERNALsolverAssertAndTrack (long a0, long a1, long a2, long a3) |
static native void | INTERNALsolverFromFile (long a0, long a1, String a2) |
static native void | INTERNALsolverFromString (long a0, long a1, String a2) |
static native long | INTERNALsolverGetAssertions (long a0, long a1) |
static native long | INTERNALsolverGetUnits (long a0, long a1) |
static native long | INTERNALsolverGetTrail (long a0, long a1) |
static native long | INTERNALsolverGetNonUnits (long a0, long a1) |
static native void | INTERNALsolverGetLevels (long a0, long a1, long a2, int a3, int[] a4) |
static native int | INTERNALsolverCheck (long a0, long a1) |
static native int | INTERNALsolverCheckAssumptions (long a0, long a1, int a2, long[] a3) |
static native int | INTERNALgetImpliedEqualities (long a0, long a1, int a2, long[] a3, int[] a4) |
static native int | INTERNALsolverGetConsequences (long a0, long a1, long a2, long a3, long a4) |
static native long | INTERNALsolverCube (long a0, long a1, long a2, int a3) |
static native long | INTERNALsolverGetModel (long a0, long a1) |
static native long | INTERNALsolverGetProof (long a0, long a1) |
static native long | INTERNALsolverGetUnsatCore (long a0, long a1) |
static native String | INTERNALsolverGetReasonUnknown (long a0, long a1) |
static native long | INTERNALsolverGetStatistics (long a0, long a1) |
static native String | INTERNALsolverToString (long a0, long a1) |
static native String | INTERNALsolverToDimacsString (long a0, long a1) |
static native String | INTERNALstatsToString (long a0, long a1) |
static native void | INTERNALstatsIncRef (long a0, long a1) |
static native void | INTERNALstatsDecRef (long a0, long a1) |
static native int | INTERNALstatsSize (long a0, long a1) |
static native String | INTERNALstatsGetKey (long a0, long a1, int a2) |
static native boolean | INTERNALstatsIsUint (long a0, long a1, int a2) |
static native boolean | INTERNALstatsIsDouble (long a0, long a1, int a2) |
static native int | INTERNALstatsGetUintValue (long a0, long a1, int a2) |
static native double | INTERNALstatsGetDoubleValue (long a0, long a1, int a2) |
static native long | INTERNALgetEstimatedAllocSize () |
static native long | INTERNALmkAstVector (long a0) |
static native void | INTERNALastVectorIncRef (long a0, long a1) |
static native void | INTERNALastVectorDecRef (long a0, long a1) |
static native int | INTERNALastVectorSize (long a0, long a1) |
static native long | INTERNALastVectorGet (long a0, long a1, int a2) |
static native void | INTERNALastVectorSet (long a0, long a1, int a2, long a3) |
static native void | INTERNALastVectorResize (long a0, long a1, int a2) |
static native void | INTERNALastVectorPush (long a0, long a1, long a2) |
static native long | INTERNALastVectorTranslate (long a0, long a1, long a2) |
static native String | INTERNALastVectorToString (long a0, long a1) |
static native long | INTERNALmkAstMap (long a0) |
static native void | INTERNALastMapIncRef (long a0, long a1) |
static native void | INTERNALastMapDecRef (long a0, long a1) |
static native boolean | INTERNALastMapContains (long a0, long a1, long a2) |
static native long | INTERNALastMapFind (long a0, long a1, long a2) |
static native void | INTERNALastMapInsert (long a0, long a1, long a2, long a3) |
static native void | INTERNALastMapErase (long a0, long a1, long a2) |
static native void | INTERNALastMapReset (long a0, long a1) |
static native int | INTERNALastMapSize (long a0, long a1) |
static native long | INTERNALastMapKeys (long a0, long a1) |
static native String | INTERNALastMapToString (long a0, long a1) |
static native boolean | INTERNALalgebraicIsValue (long a0, long a1) |
static native boolean | INTERNALalgebraicIsPos (long a0, long a1) |
static native boolean | INTERNALalgebraicIsNeg (long a0, long a1) |
static native boolean | INTERNALalgebraicIsZero (long a0, long a1) |
static native int | INTERNALalgebraicSign (long a0, long a1) |
static native long | INTERNALalgebraicAdd (long a0, long a1, long a2) |
static native long | INTERNALalgebraicSub (long a0, long a1, long a2) |
static native long | INTERNALalgebraicMul (long a0, long a1, long a2) |
static native long | INTERNALalgebraicDiv (long a0, long a1, long a2) |
static native long | INTERNALalgebraicRoot (long a0, long a1, int a2) |
static native long | INTERNALalgebraicPower (long a0, long a1, int a2) |
static native boolean | INTERNALalgebraicLt (long a0, long a1, long a2) |
static native boolean | INTERNALalgebraicGt (long a0, long a1, long a2) |
static native boolean | INTERNALalgebraicLe (long a0, long a1, long a2) |
static native boolean | INTERNALalgebraicGe (long a0, long a1, long a2) |
static native boolean | INTERNALalgebraicEq (long a0, long a1, long a2) |
static native boolean | INTERNALalgebraicNeq (long a0, long a1, long a2) |
static native long | INTERNALalgebraicRoots (long a0, long a1, int a2, long[] a3) |
static native int | INTERNALalgebraicEval (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALpolynomialSubresultants (long a0, long a1, long a2, long a3) |
static native void | INTERNALrcfDel (long a0, long a1) |
static native long | INTERNALrcfMkRational (long a0, String a1) |
static native long | INTERNALrcfMkSmallInt (long a0, int a1) |
static native long | INTERNALrcfMkPi (long a0) |
static native long | INTERNALrcfMkE (long a0) |
static native long | INTERNALrcfMkInfinitesimal (long a0) |
static native int | INTERNALrcfMkRoots (long a0, int a1, long[] a2, long[] a3) |
static native long | INTERNALrcfAdd (long a0, long a1, long a2) |
static native long | INTERNALrcfSub (long a0, long a1, long a2) |
static native long | INTERNALrcfMul (long a0, long a1, long a2) |
static native long | INTERNALrcfDiv (long a0, long a1, long a2) |
static native long | INTERNALrcfNeg (long a0, long a1) |
static native long | INTERNALrcfInv (long a0, long a1) |
static native long | INTERNALrcfPower (long a0, long a1, int a2) |
static native boolean | INTERNALrcfLt (long a0, long a1, long a2) |
static native boolean | INTERNALrcfGt (long a0, long a1, long a2) |
static native boolean | INTERNALrcfLe (long a0, long a1, long a2) |
static native boolean | INTERNALrcfGe (long a0, long a1, long a2) |
static native boolean | INTERNALrcfEq (long a0, long a1, long a2) |
static native boolean | INTERNALrcfNeq (long a0, long a1, long a2) |
static native String | INTERNALrcfNumToString (long a0, long a1, boolean a2, boolean a3) |
static native String | INTERNALrcfNumToDecimalString (long a0, long a1, int a2) |
static native void | INTERNALrcfGetNumeratorDenominator (long a0, long a1, LongPtr a2, LongPtr a3) |
static native long | INTERNALmkFixedpoint (long a0) |
static native void | INTERNALfixedpointIncRef (long a0, long a1) |
static native void | INTERNALfixedpointDecRef (long a0, long a1) |
static native void | INTERNALfixedpointAddRule (long a0, long a1, long a2, long a3) |
static native void | INTERNALfixedpointAddFact (long a0, long a1, long a2, int a3, int[] a4) |
static native void | INTERNALfixedpointAssert (long a0, long a1, long a2) |
static native int | INTERNALfixedpointQuery (long a0, long a1, long a2) |
static native int | INTERNALfixedpointQueryRelations (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALfixedpointGetAnswer (long a0, long a1) |
static native String | INTERNALfixedpointGetReasonUnknown (long a0, long a1) |
static native void | INTERNALfixedpointUpdateRule (long a0, long a1, long a2, long a3) |
static native int | INTERNALfixedpointGetNumLevels (long a0, long a1, long a2) |
static native long | INTERNALfixedpointGetCoverDelta (long a0, long a1, int a2, long a3) |
static native void | INTERNALfixedpointAddCover (long a0, long a1, int a2, long a3, long a4) |
static native long | INTERNALfixedpointGetStatistics (long a0, long a1) |
static native void | INTERNALfixedpointRegisterRelation (long a0, long a1, long a2) |
static native void | INTERNALfixedpointSetPredicateRepresentation (long a0, long a1, long a2, int a3, long[] a4) |
static native long | INTERNALfixedpointGetRules (long a0, long a1) |
static native long | INTERNALfixedpointGetAssertions (long a0, long a1) |
static native void | INTERNALfixedpointSetParams (long a0, long a1, long a2) |
static native String | INTERNALfixedpointGetHelp (long a0, long a1) |
static native long | INTERNALfixedpointGetParamDescrs (long a0, long a1) |
static native String | INTERNALfixedpointToString (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALfixedpointFromString (long a0, long a1, String a2) |
static native long | INTERNALfixedpointFromFile (long a0, long a1, String a2) |
static native long | INTERNALmkOptimize (long a0) |
static native void | INTERNALoptimizeIncRef (long a0, long a1) |
static native void | INTERNALoptimizeDecRef (long a0, long a1) |
static native void | INTERNALoptimizeAssert (long a0, long a1, long a2) |
static native void | INTERNALoptimizeAssertAndTrack (long a0, long a1, long a2, long a3) |
static native int | INTERNALoptimizeAssertSoft (long a0, long a1, long a2, String a3, long a4) |
static native int | INTERNALoptimizeMaximize (long a0, long a1, long a2) |
static native int | INTERNALoptimizeMinimize (long a0, long a1, long a2) |
static native void | INTERNALoptimizePush (long a0, long a1) |
static native void | INTERNALoptimizePop (long a0, long a1) |
static native int | INTERNALoptimizeCheck (long a0, long a1, int a2, long[] a3) |
static native String | INTERNALoptimizeGetReasonUnknown (long a0, long a1) |
static native long | INTERNALoptimizeGetModel (long a0, long a1) |
static native long | INTERNALoptimizeGetUnsatCore (long a0, long a1) |
static native void | INTERNALoptimizeSetParams (long a0, long a1, long a2) |
static native long | INTERNALoptimizeGetParamDescrs (long a0, long a1) |
static native long | INTERNALoptimizeGetLower (long a0, long a1, int a2) |
static native long | INTERNALoptimizeGetUpper (long a0, long a1, int a2) |
static native long | INTERNALoptimizeGetLowerAsVector (long a0, long a1, int a2) |
static native long | INTERNALoptimizeGetUpperAsVector (long a0, long a1, int a2) |
static native String | INTERNALoptimizeToString (long a0, long a1) |
static native void | INTERNALoptimizeFromString (long a0, long a1, String a2) |
static native void | INTERNALoptimizeFromFile (long a0, long a1, String a2) |
static native String | INTERNALoptimizeGetHelp (long a0, long a1) |
static native long | INTERNALoptimizeGetStatistics (long a0, long a1) |
static native long | INTERNALoptimizeGetAssertions (long a0, long a1) |
static native long | INTERNALoptimizeGetObjectives (long a0, long a1) |
static native long | INTERNALmkFpaRoundingModeSort (long a0) |
static native long | INTERNALmkFpaRoundNearestTiesToEven (long a0) |
static native long | INTERNALmkFpaRne (long a0) |
static native long | INTERNALmkFpaRoundNearestTiesToAway (long a0) |
static native long | INTERNALmkFpaRna (long a0) |
static native long | INTERNALmkFpaRoundTowardPositive (long a0) |
static native long | INTERNALmkFpaRtp (long a0) |
static native long | INTERNALmkFpaRoundTowardNegative (long a0) |
static native long | INTERNALmkFpaRtn (long a0) |
static native long | INTERNALmkFpaRoundTowardZero (long a0) |
static native long | INTERNALmkFpaRtz (long a0) |
static native long | INTERNALmkFpaSort (long a0, int a1, int a2) |
static native long | INTERNALmkFpaSortHalf (long a0) |
static native long | INTERNALmkFpaSort16 (long a0) |
static native long | INTERNALmkFpaSortSingle (long a0) |
static native long | INTERNALmkFpaSort32 (long a0) |
static native long | INTERNALmkFpaSortDouble (long a0) |
static native long | INTERNALmkFpaSort64 (long a0) |
static native long | INTERNALmkFpaSortQuadruple (long a0) |
static native long | INTERNALmkFpaSort128 (long a0) |
static native long | INTERNALmkFpaNan (long a0, long a1) |
static native long | INTERNALmkFpaInf (long a0, long a1, boolean a2) |
static native long | INTERNALmkFpaZero (long a0, long a1, boolean a2) |
static native long | INTERNALmkFpaFp (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaNumeralFloat (long a0, float a1, long a2) |
static native long | INTERNALmkFpaNumeralDouble (long a0, double a1, long a2) |
static native long | INTERNALmkFpaNumeralInt (long a0, int a1, long a2) |
static native long | INTERNALmkFpaNumeralIntUint (long a0, boolean a1, int a2, int a3, long a4) |
static native long | INTERNALmkFpaNumeralInt64Uint64 (long a0, boolean a1, long a2, long a3, long a4) |
static native long | INTERNALmkFpaAbs (long a0, long a1) |
static native long | INTERNALmkFpaNeg (long a0, long a1) |
static native long | INTERNALmkFpaAdd (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaSub (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaMul (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaDiv (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaFma (long a0, long a1, long a2, long a3, long a4) |
static native long | INTERNALmkFpaSqrt (long a0, long a1, long a2) |
static native long | INTERNALmkFpaRem (long a0, long a1, long a2) |
static native long | INTERNALmkFpaRoundToIntegral (long a0, long a1, long a2) |
static native long | INTERNALmkFpaMin (long a0, long a1, long a2) |
static native long | INTERNALmkFpaMax (long a0, long a1, long a2) |
static native long | INTERNALmkFpaLeq (long a0, long a1, long a2) |
static native long | INTERNALmkFpaLt (long a0, long a1, long a2) |
static native long | INTERNALmkFpaGeq (long a0, long a1, long a2) |
static native long | INTERNALmkFpaGt (long a0, long a1, long a2) |
static native long | INTERNALmkFpaEq (long a0, long a1, long a2) |
static native long | INTERNALmkFpaIsNormal (long a0, long a1) |
static native long | INTERNALmkFpaIsSubnormal (long a0, long a1) |
static native long | INTERNALmkFpaIsZero (long a0, long a1) |
static native long | INTERNALmkFpaIsInfinite (long a0, long a1) |
static native long | INTERNALmkFpaIsNan (long a0, long a1) |
static native long | INTERNALmkFpaIsNegative (long a0, long a1) |
static native long | INTERNALmkFpaIsPositive (long a0, long a1) |
static native long | INTERNALmkFpaToFpBv (long a0, long a1, long a2) |
static native long | INTERNALmkFpaToFpFloat (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaToFpReal (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaToFpSigned (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaToFpUnsigned (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaToUbv (long a0, long a1, long a2, int a3) |
static native long | INTERNALmkFpaToSbv (long a0, long a1, long a2, int a3) |
static native long | INTERNALmkFpaToReal (long a0, long a1) |
static native int | INTERNALfpaGetEbits (long a0, long a1) |
static native int | INTERNALfpaGetSbits (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralNan (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralInf (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralZero (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralNormal (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralSubnormal (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralPositive (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralNegative (long a0, long a1) |
static native long | INTERNALfpaGetNumeralSignBv (long a0, long a1) |
static native long | INTERNALfpaGetNumeralSignificandBv (long a0, long a1) |
static native boolean | INTERNALfpaGetNumeralSign (long a0, long a1, IntPtr a2) |
static native String | INTERNALfpaGetNumeralSignificandString (long a0, long a1) |
static native boolean | INTERNALfpaGetNumeralSignificandUint64 (long a0, long a1, LongPtr a2) |
static native String | INTERNALfpaGetNumeralExponentString (long a0, long a1, boolean a2) |
static native boolean | INTERNALfpaGetNumeralExponentInt64 (long a0, long a1, LongPtr a2, boolean a3) |
static native long | INTERNALfpaGetNumeralExponentBv (long a0, long a1, boolean a2) |
static native long | INTERNALmkFpaToIeeeBv (long a0, long a1) |
static native long | INTERNALmkFpaToFpIntReal (long a0, long a1, long a2, long a3, long a4) |
static native int | INTERNALfixedpointQueryFromLvl (long a0, long a1, long a2, int a3) |
static native long | INTERNALfixedpointGetGroundSatAnswer (long a0, long a1) |
static native long | INTERNALfixedpointGetRulesAlongTrace (long a0, long a1) |
static native long | INTERNALfixedpointGetRuleNamesAlongTrace (long a0, long a1) |
static native void | INTERNALfixedpointAddInvariant (long a0, long a1, long a2, long a3) |
static native long | INTERNALfixedpointGetReachable (long a0, long a1, long a2) |
static native long | INTERNALqeModelProject (long a0, long a1, int a2, long[] a3, long a4) |
static native long | INTERNALqeModelProjectSkolem (long a0, long a1, int a2, long[] a3, long a4, long a5) |
static native long | INTERNALmodelExtrapolate (long a0, long a1, long a2) |
static native long | INTERNALqeLite (long a0, long a1, long a2) |
Definition at line 4 of file Native.java.
|
inlinestatic |
Definition at line 3672 of file Native.java.
|
inlinestatic |
Definition at line 3663 of file Native.java.
|
inlinestatic |
Definition at line 1155 of file Native.java.
|
inlinestatic |
Definition at line 5123 of file Native.java.
|
inlinestatic |
Definition at line 5150 of file Native.java.
|
inlinestatic |
Definition at line 5213 of file Native.java.
|
inlinestatic |
Definition at line 5240 of file Native.java.
|
inlinestatic |
Definition at line 5204 of file Native.java.
|
inlinestatic |
Definition at line 5186 of file Native.java.
|
inlinestatic |
Definition at line 5096 of file Native.java.
|
inlinestatic |
Definition at line 5087 of file Native.java.
|
inlinestatic |
Definition at line 5078 of file Native.java.
|
inlinestatic |
Definition at line 5105 of file Native.java.
|
inlinestatic |
Definition at line 5195 of file Native.java.
|
inlinestatic |
Definition at line 5177 of file Native.java.
|
inlinestatic |
Definition at line 5141 of file Native.java.
|
inlinestatic |
Definition at line 5222 of file Native.java.
|
inlinestatic |
Definition at line 5168 of file Native.java.
|
inlinestatic |
Definition at line 5159 of file Native.java.
|
inlinestatic |
Definition at line 5231 of file Native.java.
|
inlinestatic |
Definition at line 5114 of file Native.java.
|
inlinestatic |
Definition at line 5132 of file Native.java.
|
inlinestatic |
Definition at line 3797 of file Native.java.
Referenced by Log.append().
|
inlinestatic |
Definition at line 4459 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4451 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 3035 of file Native.java.
|
inlinestatic |
Definition at line 5009 of file Native.java.
|
inlinestatic |
Definition at line 5001 of file Native.java.
|
inlinestatic |
Definition at line 5035 of file Native.java.
|
inlinestatic |
Definition at line 5018 of file Native.java.
|
inlinestatic |
Definition at line 4993 of file Native.java.
|
inlinestatic |
Definition at line 5027 of file Native.java.
|
inlinestatic |
Definition at line 5060 of file Native.java.
|
inlinestatic |
Definition at line 5043 of file Native.java.
|
inlinestatic |
Definition at line 5051 of file Native.java.
|
inlinestatic |
Definition at line 5069 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4916 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4908 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3802 of file Native.java.
Referenced by Log.close().
|
inlinestatic |
|
inlinestatic |
Definition at line 766 of file Native.java.
|
inlinestatic |
Definition at line 727 of file Native.java.
Referenced by Context.Context().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 753 of file Native.java.
Referenced by Context.close().
|
inlinestatic |
Definition at line 3940 of file Native.java.
Referenced by Global.disableTrace().
|
inlinestatic |
Definition at line 3935 of file Native.java.
Referenced by Global.enableTrace().
|
inlinestatic |
Definition at line 3892 of file Native.java.
|
inlinestatic |
Definition at line 3950 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 6668 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 5480 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 6641 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 6676 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 6659 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 6650 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 5472 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 6632 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2873 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 3756 of file Native.java.
|
inlinestatic |
Definition at line 3782 of file Native.java.
|
inlinestatic |
Definition at line 3773 of file Native.java.
|
inlinestatic |
Definition at line 3764 of file Native.java.
|
inlinestatic |
Definition at line 3748 of file Native.java.
|
inlinestatic |
Definition at line 3740 of file Native.java.
|
inlinestatic |
Definition at line 3688 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3680 of file Native.java.
|
inlinestatic |
Definition at line 3723 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2774 of file Native.java.
Referenced by DatatypeSort.getAccessors(), ListSort.getConsDecl(), EnumSort.getConstDecl(), EnumSort.getConstDecls(), DatatypeSort.getConstructors(), and ListSort.getNilDecl().
|
inlinestatic |
Definition at line 2792 of file Native.java.
Referenced by DatatypeSort.getAccessors(), ListSort.getHeadDecl(), and ListSort.getTailDecl().
|
inlinestatic |
Definition at line 2765 of file Native.java.
Referenced by EnumSort.getConstDecls(), DatatypeSort.getNumConstructors(), and EnumSort.getTesterDecls().
|
inlinestatic |
Definition at line 2783 of file Native.java.
Referenced by ListSort.getIsConsDecl(), ListSort.getIsNilDecl(), DatatypeSort.getRecognizers(), EnumSort.getTesterDecl(), and EnumSort.getTesterDecls().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2963 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 2999 of file Native.java.
|
inlinestatic |
Definition at line 2990 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3901 of file Native.java.
|
inlinestatic |
Definition at line 3915 of file Native.java.
|
inlinestatic |
Definition at line 4893 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 3929 of file Native.java.
Referenced by Version.getFullVersion().
|
inlinestatic |
|
inlinestatic |
Definition at line 4724 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 2198 of file Native.java.
|
inlinestatic |
Definition at line 3188 of file Native.java.
Referenced by AlgebraicNum.toDecimal(), and RatNum.toDecimalString().
|
inlinestatic |
Definition at line 3197 of file Native.java.
|
inlinestatic |
Definition at line 3233 of file Native.java.
Referenced by BitVecNum.getInt(), IntNum.getInt(), and FiniteDomainNum.getInt().
|
inlinestatic |
Definition at line 3260 of file Native.java.
Referenced by IntNum.getInt64(), FiniteDomainNum.getInt64(), and BitVecNum.getLong().
|
inlinestatic |
Definition at line 3269 of file Native.java.
|
inlinestatic |
Definition at line 3224 of file Native.java.
|
inlinestatic |
Definition at line 3179 of file Native.java.
Referenced by IntNum.toString(), BitVecNum.toString(), FiniteDomainNum.toString(), RatNum.toString(), and FPNum.toString().
|
inlinestatic |
Definition at line 3242 of file Native.java.
|
inlinestatic |
Definition at line 3251 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3431 of file Native.java.
Referenced by Lambda.getBody(), and Quantifier.getBody().
|
inlinestatic |
Definition at line 3413 of file Native.java.
Referenced by Lambda.getBoundVariableNames(), and Quantifier.getBoundVariableNames().
|
inlinestatic |
Definition at line 3422 of file Native.java.
Referenced by Lambda.getBoundVariableSorts(), and Quantifier.getBoundVariableSorts().
|
inlinestatic |
|
inlinestatic |
Definition at line 3404 of file Native.java.
Referenced by Lambda.getNumBound(), and Quantifier.getNumBound().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2945 of file Native.java.
Referenced by Model.getFuncInterp(), and FuncDecl.getRange().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2135 of file Native.java.
|
inlinestatic |
Definition at line 2108 of file Native.java.
|
inlinestatic |
Definition at line 3098 of file Native.java.
Referenced by Expr.getSort(), Expr.isArray(), Expr.isBool(), Expr.isBV(), Expr.isFiniteDomain(), Expr.isInt(), Expr.isReal(), and Expr.isRelation().
|
inlinestatic |
|
inlinestatic |
Definition at line 2693 of file Native.java.
Referenced by Model.getFuncInterp(), Sort.getSortKind(), Expr.isArray(), Expr.isBV(), Expr.isInt(), and Expr.isReal().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3924 of file Native.java.
Referenced by Version.getBuild(), Version.getMajor(), Version.getMinor(), Version.getRevision(), and Version.getString().
|
inlinestatic |
Definition at line 715 of file Native.java.
Referenced by Global.getParameter().
|
inlinestatic |
Definition at line 710 of file Native.java.
Referenced by Global.resetParameters().
|
inlinestatic |
Definition at line 705 of file Native.java.
Referenced by Global.setParameter().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3972 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3964 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4095 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 758 of file Native.java.
|
staticprotected |
Referenced by Native.addConstInterp().
|
staticprotected |
Referenced by Native.addFuncInterp().
|
staticprotected |
Referenced by Native.addRecDef().
|
staticprotected |
Referenced by Native.algebraicAdd().
|
staticprotected |
Referenced by Native.algebraicDiv().
|
staticprotected |
Referenced by Native.algebraicEq().
|
staticprotected |
Referenced by Native.algebraicEval().
|
staticprotected |
Referenced by Native.algebraicGe().
|
staticprotected |
Referenced by Native.algebraicGt().
|
staticprotected |
Referenced by Native.algebraicIsNeg().
|
staticprotected |
Referenced by Native.algebraicIsPos().
|
staticprotected |
Referenced by Native.algebraicIsValue().
|
staticprotected |
Referenced by Native.algebraicIsZero().
|
staticprotected |
Referenced by Native.algebraicLe().
|
staticprotected |
Referenced by Native.algebraicLt().
|
staticprotected |
Referenced by Native.algebraicMul().
|
staticprotected |
Referenced by Native.algebraicNeq().
|
staticprotected |
Referenced by Native.algebraicPower().
|
staticprotected |
Referenced by Native.algebraicRoot().
|
staticprotected |
Referenced by Native.algebraicRoots().
|
staticprotected |
Referenced by Native.algebraicSign().
|
staticprotected |
Referenced by Native.algebraicSub().
|
staticprotected |
Referenced by Native.appendLog().
|
staticprotected |
Referenced by Native.applyResultDecRef().
|
staticprotected |
Referenced by Native.applyResultGetNumSubgoals().
|
staticprotected |
Referenced by Native.applyResultGetSubgoal().
|
staticprotected |
Referenced by Native.applyResultIncRef().
|
staticprotected |
Referenced by Native.applyResultToString().
|
staticprotected |
Referenced by Native.appToAst().
|
staticprotected |
Referenced by Native.astMapContains().
|
staticprotected |
Referenced by Native.astMapDecRef().
|
staticprotected |
Referenced by Native.astMapErase().
|
staticprotected |
Referenced by Native.astMapFind().
|
staticprotected |
Referenced by Native.astMapIncRef().
|
staticprotected |
Referenced by Native.astMapInsert().
|
staticprotected |
Referenced by Native.astMapKeys().
|
staticprotected |
Referenced by Native.astMapReset().
|
staticprotected |
Referenced by Native.astMapSize().
|
staticprotected |
Referenced by Native.astMapToString().
|
staticprotected |
Referenced by Native.astToString().
|
staticprotected |
Referenced by Native.astVectorDecRef().
|
staticprotected |
Referenced by Native.astVectorGet().
|
staticprotected |
Referenced by Native.astVectorIncRef().
|
staticprotected |
Referenced by Native.astVectorPush().
|
staticprotected |
Referenced by Native.astVectorResize().
|
staticprotected |
Referenced by Native.astVectorSet().
|
staticprotected |
Referenced by Native.astVectorSize().
|
staticprotected |
Referenced by Native.astVectorToString().
|
staticprotected |
Referenced by Native.astVectorTranslate().
|
staticprotected |
Referenced by Native.benchmarkToSmtlibString().
|
staticprotected |
Referenced by Native.closeLog().
|
staticprotected |
Referenced by Native.datatypeUpdateField().
|
staticprotected |
Referenced by Native.decRef().
|
staticprotected |
Referenced by Native.delConfig().
|
staticprotected |
Referenced by Native.delConstructor().
|
staticprotected |
Referenced by Native.delConstructorList().
|
staticprotected |
Referenced by Native.delContext().
|
staticprotected |
Referenced by Native.disableTrace().
|
staticprotected |
Referenced by Native.enableTrace().
|
staticprotected |
Referenced by Native.evalSmtlib2String().
|
staticprotected |
Referenced by Native.finalizeMemory().
|
staticprotected |
Referenced by Native.fixedpointAddCover().
|
staticprotected |
Referenced by Native.fixedpointAddFact().
|
staticprotected |
Referenced by Native.fixedpointAddInvariant().
|
staticprotected |
Referenced by Native.fixedpointAddRule().
|
staticprotected |
Referenced by Native.fixedpointAssert().
|
staticprotected |
Referenced by Native.fixedpointDecRef().
|
staticprotected |
Referenced by Native.fixedpointFromFile().
|
staticprotected |
Referenced by Native.fixedpointFromString().
|
staticprotected |
Referenced by Native.fixedpointGetAnswer().
|
staticprotected |
Referenced by Native.fixedpointGetAssertions().
|
staticprotected |
Referenced by Native.fixedpointGetCoverDelta().
|
staticprotected |
Referenced by Native.fixedpointGetGroundSatAnswer().
|
staticprotected |
Referenced by Native.fixedpointGetHelp().
|
staticprotected |
Referenced by Native.fixedpointGetNumLevels().
|
staticprotected |
Referenced by Native.fixedpointGetParamDescrs().
|
staticprotected |
Referenced by Native.fixedpointGetReachable().
|
staticprotected |
Referenced by Native.fixedpointGetReasonUnknown().
|
staticprotected |
Referenced by Native.fixedpointGetRuleNamesAlongTrace().
|
staticprotected |
Referenced by Native.fixedpointGetRules().
|
staticprotected |
Referenced by Native.fixedpointGetRulesAlongTrace().
|
staticprotected |
Referenced by Native.fixedpointGetStatistics().
|
staticprotected |
Referenced by Native.fixedpointIncRef().
|
staticprotected |
Referenced by Native.fixedpointQuery().
|
staticprotected |
Referenced by Native.fixedpointQueryFromLvl().
|
staticprotected |
Referenced by Native.fixedpointQueryRelations().
|
staticprotected |
Referenced by Native.fixedpointRegisterRelation().
|
staticprotected |
Referenced by Native.fixedpointSetParams().
|
staticprotected |
Referenced by Native.fixedpointSetPredicateRepresentation().
|
staticprotected |
Referenced by Native.fixedpointToString().
|
staticprotected |
Referenced by Native.fixedpointUpdateRule().
|
staticprotected |
Referenced by Native.fpaGetEbits().
|
staticprotected |
Referenced by Native.fpaGetNumeralExponentBv().
|
staticprotected |
Referenced by Native.fpaGetNumeralExponentInt64().
|
staticprotected |
Referenced by Native.fpaGetNumeralExponentString().
|
staticprotected |
Referenced by Native.fpaGetNumeralSign().
|
staticprotected |
Referenced by Native.fpaGetNumeralSignBv().
|
staticprotected |
Referenced by Native.fpaGetNumeralSignificandBv().
|
staticprotected |
Referenced by Native.fpaGetNumeralSignificandString().
|
staticprotected |
Referenced by Native.fpaGetNumeralSignificandUint64().
|
staticprotected |
Referenced by Native.fpaGetSbits().
|
staticprotected |
Referenced by Native.fpaIsNumeralInf().
|
staticprotected |
Referenced by Native.fpaIsNumeralNan().
|
staticprotected |
Referenced by Native.fpaIsNumeralNegative().
|
staticprotected |
Referenced by Native.fpaIsNumeralNormal().
|
staticprotected |
Referenced by Native.fpaIsNumeralPositive().
|
staticprotected |
Referenced by Native.fpaIsNumeralSubnormal().
|
staticprotected |
Referenced by Native.fpaIsNumeralZero().
|
staticprotected |
Referenced by Native.funcDeclToAst().
|
staticprotected |
Referenced by Native.funcDeclToString().
|
staticprotected |
Referenced by Native.funcEntryDecRef().
|
staticprotected |
Referenced by Native.funcEntryGetArg().
|
staticprotected |
Referenced by Native.funcEntryGetNumArgs().
|
staticprotected |
Referenced by Native.funcEntryGetValue().
|
staticprotected |
Referenced by Native.funcEntryIncRef().
|
staticprotected |
Referenced by Native.funcInterpAddEntry().
|
staticprotected |
Referenced by Native.funcInterpDecRef().
|
staticprotected |
Referenced by Native.funcInterpGetArity().
|
staticprotected |
Referenced by Native.funcInterpGetElse().
|
staticprotected |
Referenced by Native.funcInterpGetEntry().
|
staticprotected |
Referenced by Native.funcInterpGetNumEntries().
|
staticprotected |
Referenced by Native.funcInterpIncRef().
|
staticprotected |
Referenced by Native.funcInterpSetElse().
|
staticprotected |
Referenced by Native.getAlgebraicNumberLower().
|
staticprotected |
Referenced by Native.getAlgebraicNumberUpper().
|
staticprotected |
Referenced by Native.getAppArg().
|
staticprotected |
Referenced by Native.getAppDecl().
|
staticprotected |
Referenced by Native.getAppNumArgs().
|
staticprotected |
Referenced by Native.getArity().
|
staticprotected |
Referenced by Native.getArraySortDomain().
|
staticprotected |
Referenced by Native.getArraySortRange().
|
staticprotected |
Referenced by Native.getAsArrayFuncDecl().
|
staticprotected |
Referenced by Native.getAstHash().
|
staticprotected |
Referenced by Native.getAstId().
|
staticprotected |
Referenced by Native.getAstKind().
|
staticprotected |
Referenced by Native.getBoolValue().
|
staticprotected |
Referenced by Native.getBvSortSize().
|
staticprotected |
Referenced by Native.getDatatypeSortConstructor().
|
staticprotected |
Referenced by Native.getDatatypeSortConstructorAccessor().
|
staticprotected |
Referenced by Native.getDatatypeSortNumConstructors().
|
staticprotected |
Referenced by Native.getDatatypeSortRecognizer().
|
staticprotected |
Referenced by Native.getDeclAstParameter().
|
staticprotected |
Referenced by Native.getDeclDoubleParameter().
|
staticprotected |
Referenced by Native.getDeclFuncDeclParameter().
|
staticprotected |
Referenced by Native.getDeclIntParameter().
|
staticprotected |
Referenced by Native.getDeclKind().
|
staticprotected |
Referenced by Native.getDeclName().
|
staticprotected |
Referenced by Native.getDeclNumParameters().
|
staticprotected |
Referenced by Native.getDeclParameterKind().
|
staticprotected |
Referenced by Native.getDeclRationalParameter().
|
staticprotected |
Referenced by Native.getDeclSortParameter().
|
staticprotected |
Referenced by Native.getDeclSymbolParameter().
|
staticprotected |
Referenced by Native.getDenominator().
|
staticprotected |
Referenced by Native.getDomain().
|
staticprotected |
Referenced by Native.getDomainSize().
|
staticprotected |
Referenced by Native.addConstInterp(), Native.addFuncInterp(), Native.addRecDef(), Native.algebraicAdd(), Native.algebraicDiv(), Native.algebraicEq(), Native.algebraicEval(), Native.algebraicGe(), Native.algebraicGt(), Native.algebraicIsNeg(), Native.algebraicIsPos(), Native.algebraicIsValue(), Native.algebraicIsZero(), Native.algebraicLe(), Native.algebraicLt(), Native.algebraicMul(), Native.algebraicNeq(), Native.algebraicPower(), Native.algebraicRoot(), Native.algebraicRoots(), Native.algebraicSign(), Native.algebraicSub(), Native.applyResultDecRef(), Native.applyResultGetNumSubgoals(), Native.applyResultGetSubgoal(), Native.applyResultIncRef(), Native.applyResultToString(), Native.appToAst(), Native.astMapContains(), Native.astMapDecRef(), Native.astMapErase(), Native.astMapFind(), Native.astMapIncRef(), Native.astMapInsert(), Native.astMapKeys(), Native.astMapReset(), Native.astMapSize(), Native.astMapToString(), Native.astToString(), Native.astVectorDecRef(), Native.astVectorGet(), Native.astVectorIncRef(), Native.astVectorPush(), Native.astVectorResize(), Native.astVectorSet(), Native.astVectorSize(), Native.astVectorToString(), Native.astVectorTranslate(), Native.benchmarkToSmtlibString(), Native.datatypeUpdateField(), Native.decRef(), Native.delConstructor(), Native.delConstructorList(), Native.evalSmtlib2String(), Native.fixedpointAddCover(), Native.fixedpointAddFact(), Native.fixedpointAddInvariant(), Native.fixedpointAddRule(), Native.fixedpointAssert(), Native.fixedpointDecRef(), Native.fixedpointFromFile(), Native.fixedpointFromString(), Native.fixedpointGetAnswer(), Native.fixedpointGetAssertions(), Native.fixedpointGetCoverDelta(), Native.fixedpointGetGroundSatAnswer(), Native.fixedpointGetHelp(), Native.fixedpointGetNumLevels(), Native.fixedpointGetParamDescrs(), Native.fixedpointGetReachable(), Native.fixedpointGetReasonUnknown(), Native.fixedpointGetRuleNamesAlongTrace(), Native.fixedpointGetRules(), Native.fixedpointGetRulesAlongTrace(), Native.fixedpointGetStatistics(), Native.fixedpointIncRef(), Native.fixedpointQuery(), Native.fixedpointQueryFromLvl(), Native.fixedpointQueryRelations(), Native.fixedpointRegisterRelation(), Native.fixedpointSetParams(), Native.fixedpointSetPredicateRepresentation(), Native.fixedpointToString(), Native.fixedpointUpdateRule(), Native.fpaGetEbits(), Native.fpaGetNumeralExponentBv(), Native.fpaGetNumeralExponentInt64(), Native.fpaGetNumeralExponentString(), Native.fpaGetNumeralSign(), Native.fpaGetNumeralSignBv(), Native.fpaGetNumeralSignificandBv(), Native.fpaGetNumeralSignificandString(), Native.fpaGetNumeralSignificandUint64(), Native.fpaGetSbits(), Native.fpaIsNumeralInf(), Native.fpaIsNumeralNan(), Native.fpaIsNumeralNegative(), Native.fpaIsNumeralNormal(), Native.fpaIsNumeralPositive(), Native.fpaIsNumeralSubnormal(), Native.fpaIsNumeralZero(), Native.funcDeclToAst(), Native.funcDeclToString(), Native.funcEntryDecRef(), Native.funcEntryGetArg(), Native.funcEntryGetNumArgs(), Native.funcEntryGetValue(), Native.funcEntryIncRef(), Native.funcInterpAddEntry(), Native.funcInterpDecRef(), Native.funcInterpGetArity(), Native.funcInterpGetElse(), Native.funcInterpGetEntry(), Native.funcInterpGetNumEntries(), Native.funcInterpIncRef(), Native.funcInterpSetElse(), Native.getAlgebraicNumberLower(), Native.getAlgebraicNumberUpper(), Native.getAppArg(), Native.getAppDecl(), Native.getAppNumArgs(), Native.getArity(), Native.getArraySortDomain(), Native.getArraySortRange(), Native.getAsArrayFuncDecl(), Native.getAstHash(), Native.getAstId(), Native.getAstKind(), Native.getBoolValue(), Native.getBvSortSize(), Native.getDatatypeSortConstructor(), Native.getDatatypeSortConstructorAccessor(), Native.getDatatypeSortNumConstructors(), Native.getDatatypeSortRecognizer(), Native.getDeclAstParameter(), Native.getDeclDoubleParameter(), Native.getDeclFuncDeclParameter(), Native.getDeclIntParameter(), Native.getDeclKind(), Native.getDeclName(), Native.getDeclNumParameters(), Native.getDeclParameterKind(), Native.getDeclRationalParameter(), Native.getDeclSortParameter(), Native.getDeclSymbolParameter(), Native.getDenominator(), Native.getDomain(), Native.getDomainSize(), Native.getErrorCode(), Native.getErrorMsg(), Native.getFiniteDomainSortSize(), Native.getFuncDeclId(), Native.getImpliedEqualities(), Native.getIndexValue(), Native.getLstring(), Native.getNumeralDecimalString(), Native.getNumeralDouble(), Native.getNumeralInt(), Native.getNumeralInt64(), Native.getNumeralRationalInt64(), Native.getNumeralSmall(), Native.getNumeralString(), Native.getNumeralUint(), Native.getNumeralUint64(), Native.getNumerator(), Native.getNumProbes(), Native.getNumTactics(), Native.getPattern(), Native.getPatternNumTerms(), Native.getProbeName(), Native.getQuantifierBody(), Native.getQuantifierBoundName(), Native.getQuantifierBoundSort(), Native.getQuantifierNoPatternAst(), Native.getQuantifierNumBound(), Native.getQuantifierNumNoPatterns(), Native.getQuantifierNumPatterns(), Native.getQuantifierPatternAst(), Native.getQuantifierWeight(), Native.getRange(), Native.getRelationArity(), Native.getRelationColumn(), Native.getReSortBasis(), Native.getSeqSortBasis(), Native.getSort(), Native.getSortId(), Native.getSortKind(), Native.getSortName(), Native.getString(), Native.getSymbolInt(), Native.getSymbolKind(), Native.getSymbolString(), Native.getTacticName(), Native.getTupleSortFieldDecl(), Native.getTupleSortMkDecl(), Native.getTupleSortNumFields(), Native.goalAssert(), Native.goalConvertModel(), Native.goalDecRef(), Native.goalDepth(), Native.goalFormula(), Native.goalInconsistent(), Native.goalIncRef(), Native.goalIsDecidedSat(), Native.goalIsDecidedUnsat(), Native.goalNumExprs(), Native.goalPrecision(), Native.goalReset(), Native.goalSize(), Native.goalToDimacsString(), Native.goalToString(), Native.goalTranslate(), Native.incRef(), Native.interrupt(), Native.isAlgebraicNumber(), Native.isApp(), Native.isAsArray(), Native.isEqAst(), Native.isEqFuncDecl(), Native.isEqSort(), Native.isLambda(), Native.isNumeralAst(), Native.isQuantifierExists(), Native.isQuantifierForall(), Native.isReSort(), Native.isSeqSort(), Native.isString(), Native.isStringSort(), Native.isWellSorted(), Native.mkAdd(), Native.mkAnd(), Native.mkApp(), Native.mkArrayDefault(), Native.mkArrayExt(), Native.mkArraySort(), Native.mkArraySortN(), Native.mkAsArray(), Native.mkAstMap(), Native.mkAstVector(), Native.mkAtleast(), Native.mkAtmost(), Native.mkBoolSort(), Native.mkBound(), Native.mkBv2int(), Native.mkBvadd(), Native.mkBvaddNoOverflow(), Native.mkBvaddNoUnderflow(), Native.mkBvand(), Native.mkBvashr(), Native.mkBvlshr(), Native.mkBvmul(), Native.mkBvmulNoOverflow(), Native.mkBvmulNoUnderflow(), Native.mkBvnand(), Native.mkBvneg(), Native.mkBvnegNoOverflow(), Native.mkBvnor(), Native.mkBvnot(), Native.mkBvNumeral(), Native.mkBvor(), Native.mkBvredand(), Native.mkBvredor(), Native.mkBvsdiv(), Native.mkBvsdivNoOverflow(), Native.mkBvsge(), Native.mkBvsgt(), Native.mkBvshl(), Native.mkBvsle(), Native.mkBvslt(), Native.mkBvsmod(), Native.mkBvSort(), Native.mkBvsrem(), Native.mkBvsub(), Native.mkBvsubNoOverflow(), Native.mkBvsubNoUnderflow(), Native.mkBvudiv(), Native.mkBvuge(), Native.mkBvugt(), Native.mkBvule(), Native.mkBvult(), Native.mkBvurem(), Native.mkBvxnor(), Native.mkBvxor(), Native.mkConcat(), Native.mkConst(), Native.mkConstArray(), Native.mkConstructor(), Native.mkConstructorList(), Native.mkDatatype(), Native.mkDatatypes(), Native.mkDistinct(), Native.mkDiv(), Native.mkDivides(), Native.mkEmptySet(), Native.mkEnumerationSort(), Native.mkEq(), Native.mkExists(), Native.mkExistsConst(), Native.mkExtract(), Native.mkExtRotateLeft(), Native.mkExtRotateRight(), Native.mkFalse(), Native.mkFiniteDomainSort(), Native.mkFixedpoint(), Native.mkForall(), Native.mkForallConst(), Native.mkFpaAbs(), Native.mkFpaAdd(), Native.mkFpaDiv(), Native.mkFpaEq(), Native.mkFpaFma(), Native.mkFpaFp(), Native.mkFpaGeq(), Native.mkFpaGt(), Native.mkFpaInf(), Native.mkFpaIsInfinite(), Native.mkFpaIsNan(), Native.mkFpaIsNegative(), Native.mkFpaIsNormal(), Native.mkFpaIsPositive(), Native.mkFpaIsSubnormal(), Native.mkFpaIsZero(), Native.mkFpaLeq(), Native.mkFpaLt(), Native.mkFpaMax(), Native.mkFpaMin(), Native.mkFpaMul(), Native.mkFpaNan(), Native.mkFpaNeg(), Native.mkFpaNumeralDouble(), Native.mkFpaNumeralFloat(), Native.mkFpaNumeralInt(), Native.mkFpaNumeralInt64Uint64(), Native.mkFpaNumeralIntUint(), Native.mkFpaRem(), Native.mkFpaRna(), Native.mkFpaRne(), Native.mkFpaRoundingModeSort(), Native.mkFpaRoundNearestTiesToAway(), Native.mkFpaRoundNearestTiesToEven(), Native.mkFpaRoundToIntegral(), Native.mkFpaRoundTowardNegative(), Native.mkFpaRoundTowardPositive(), Native.mkFpaRoundTowardZero(), Native.mkFpaRtn(), Native.mkFpaRtp(), Native.mkFpaRtz(), Native.mkFpaSort(), Native.mkFpaSort128(), Native.mkFpaSort16(), Native.mkFpaSort32(), Native.mkFpaSort64(), Native.mkFpaSortDouble(), Native.mkFpaSortHalf(), Native.mkFpaSortQuadruple(), Native.mkFpaSortSingle(), Native.mkFpaSqrt(), Native.mkFpaSub(), Native.mkFpaToFpBv(), Native.mkFpaToFpFloat(), Native.mkFpaToFpIntReal(), Native.mkFpaToFpReal(), Native.mkFpaToFpSigned(), Native.mkFpaToFpUnsigned(), Native.mkFpaToIeeeBv(), Native.mkFpaToReal(), Native.mkFpaToSbv(), Native.mkFpaToUbv(), Native.mkFpaZero(), Native.mkFreshConst(), Native.mkFreshFuncDecl(), Native.mkFullSet(), Native.mkFuncDecl(), Native.mkGe(), Native.mkGoal(), Native.mkGt(), Native.mkIff(), Native.mkImplies(), Native.mkInt(), Native.mkInt2bv(), Native.mkInt2real(), Native.mkInt64(), Native.mkIntSort(), Native.mkIntSymbol(), Native.mkIntToStr(), Native.mkIsInt(), Native.mkIte(), Native.mkLambda(), Native.mkLambdaConst(), Native.mkLe(), Native.mkLinearOrder(), Native.mkListSort(), Native.mkLstring(), Native.mkLt(), Native.mkMap(), Native.mkMod(), Native.mkModel(), Native.mkMul(), Native.mkNot(), Native.mkNumeral(), Native.mkOptimize(), Native.mkOr(), Native.mkParams(), Native.mkPartialOrder(), Native.mkPattern(), Native.mkPbeq(), Native.mkPbge(), Native.mkPble(), Native.mkPiecewiseLinearOrder(), Native.mkPower(), Native.mkProbe(), Native.mkQuantifier(), Native.mkQuantifierConst(), Native.mkQuantifierConstEx(), Native.mkQuantifierEx(), Native.mkReal(), Native.mkReal2int(), Native.mkRealSort(), Native.mkRecFuncDecl(), Native.mkReComplement(), Native.mkReConcat(), Native.mkReEmpty(), Native.mkReFull(), Native.mkReIntersect(), Native.mkReLoop(), Native.mkRem(), Native.mkReOption(), Native.mkRepeat(), Native.mkRePlus(), Native.mkReRange(), Native.mkReSort(), Native.mkReStar(), Native.mkReUnion(), Native.mkRotateLeft(), Native.mkRotateRight(), Native.mkSelect(), Native.mkSelectN(), Native.mkSeqAt(), Native.mkSeqConcat(), Native.mkSeqContains(), Native.mkSeqEmpty(), Native.mkSeqExtract(), Native.mkSeqIndex(), Native.mkSeqInRe(), Native.mkSeqLastIndex(), Native.mkSeqLength(), Native.mkSeqNth(), Native.mkSeqPrefix(), Native.mkSeqReplace(), Native.mkSeqSort(), Native.mkSeqSuffix(), Native.mkSeqToRe(), Native.mkSeqUnit(), Native.mkSetAdd(), Native.mkSetComplement(), Native.mkSetDel(), Native.mkSetDifference(), Native.mkSetHasSize(), Native.mkSetIntersect(), Native.mkSetMember(), Native.mkSetSort(), Native.mkSetSubset(), Native.mkSetUnion(), Native.mkSignExt(), Native.mkSimpleSolver(), Native.mkSolver(), Native.mkSolverForLogic(), Native.mkSolverFromTactic(), Native.mkStore(), Native.mkStoreN(), Native.mkString(), Native.mkStringSort(), Native.mkStringSymbol(), Native.mkStrLe(), Native.mkStrLt(), Native.mkStrToInt(), Native.mkSub(), Native.mkTactic(), Native.mkTransitiveClosure(), Native.mkTreeOrder(), Native.mkTrue(), Native.mkTupleSort(), Native.mkUnaryMinus(), Native.mkUninterpretedSort(), Native.mkUnsignedInt(), Native.mkUnsignedInt64(), Native.mkXor(), Native.mkZeroExt(), Native.modelDecRef(), Native.modelEval(), Native.modelExtrapolate(), Native.modelGetConstDecl(), Native.modelGetConstInterp(), Native.modelGetFuncDecl(), Native.modelGetFuncInterp(), Native.modelGetNumConsts(), Native.modelGetNumFuncs(), Native.modelGetNumSorts(), Native.modelGetSort(), Native.modelGetSortUniverse(), Native.modelHasInterp(), Native.modelIncRef(), Native.modelToString(), Native.modelTranslate(), Native.optimizeAssert(), Native.optimizeAssertAndTrack(), Native.optimizeAssertSoft(), Native.optimizeCheck(), Native.optimizeDecRef(), Native.optimizeFromFile(), Native.optimizeFromString(), Native.optimizeGetAssertions(), Native.optimizeGetHelp(), Native.optimizeGetLower(), Native.optimizeGetLowerAsVector(), Native.optimizeGetModel(), Native.optimizeGetObjectives(), Native.optimizeGetParamDescrs(), Native.optimizeGetReasonUnknown(), Native.optimizeGetStatistics(), Native.optimizeGetUnsatCore(), Native.optimizeGetUpper(), Native.optimizeGetUpperAsVector(), Native.optimizeIncRef(), Native.optimizeMaximize(), Native.optimizeMinimize(), Native.optimizePop(), Native.optimizePush(), Native.optimizeSetParams(), Native.optimizeToString(), Native.paramDescrsDecRef(), Native.paramDescrsGetDocumentation(), Native.paramDescrsGetKind(), Native.paramDescrsGetName(), Native.paramDescrsIncRef(), Native.paramDescrsSize(), Native.paramDescrsToString(), Native.paramsDecRef(), Native.paramsIncRef(), Native.paramsSetBool(), Native.paramsSetDouble(), Native.paramsSetSymbol(), Native.paramsSetUint(), Native.paramsToString(), Native.paramsValidate(), Native.parseSmtlib2File(), Native.parseSmtlib2String(), Native.patternToAst(), Native.patternToString(), Native.polynomialSubresultants(), Native.probeAnd(), Native.probeApply(), Native.probeConst(), Native.probeDecRef(), Native.probeEq(), Native.probeGe(), Native.probeGetDescr(), Native.probeGt(), Native.probeIncRef(), Native.probeLe(), Native.probeLt(), Native.probeNot(), Native.probeOr(), Native.qeLite(), Native.qeModelProject(), Native.qeModelProjectSkolem(), Native.queryConstructor(), Native.rcfAdd(), Native.rcfDel(), Native.rcfDiv(), Native.rcfEq(), Native.rcfGe(), Native.rcfGetNumeratorDenominator(), Native.rcfGt(), Native.rcfInv(), Native.rcfLe(), Native.rcfLt(), Native.rcfMkE(), Native.rcfMkInfinitesimal(), Native.rcfMkPi(), Native.rcfMkRational(), Native.rcfMkRoots(), Native.rcfMkSmallInt(), Native.rcfMul(), Native.rcfNeg(), Native.rcfNeq(), Native.rcfNumToDecimalString(), Native.rcfNumToString(), Native.rcfPower(), Native.rcfSub(), Native.setAstPrintMode(), Native.setError(), Native.simplify(), Native.simplifyEx(), Native.simplifyGetHelp(), Native.simplifyGetParamDescrs(), Native.solverAssert(), Native.solverAssertAndTrack(), Native.solverCheck(), Native.solverCheckAssumptions(), Native.solverCube(), Native.solverDecRef(), Native.solverFromFile(), Native.solverFromString(), Native.solverGetAssertions(), Native.solverGetConsequences(), Native.solverGetHelp(), Native.solverGetLevels(), Native.solverGetModel(), Native.solverGetNonUnits(), Native.solverGetNumScopes(), Native.solverGetParamDescrs(), Native.solverGetProof(), Native.solverGetReasonUnknown(), Native.solverGetStatistics(), Native.solverGetTrail(), Native.solverGetUnits(), Native.solverGetUnsatCore(), Native.solverImportModelConverter(), Native.solverIncRef(), Native.solverInterrupt(), Native.solverPop(), Native.solverPush(), Native.solverReset(), Native.solverSetParams(), Native.solverToDimacsString(), Native.solverToString(), Native.solverTranslate(), Native.sortToAst(), Native.sortToString(), Native.statsDecRef(), Native.statsGetDoubleValue(), Native.statsGetKey(), Native.statsGetUintValue(), Native.statsIncRef(), Native.statsIsDouble(), Native.statsIsUint(), Native.statsSize(), Native.statsToString(), Native.substitute(), Native.substituteVars(), Native.tacticAndThen(), Native.tacticApply(), Native.tacticApplyEx(), Native.tacticCond(), Native.tacticDecRef(), Native.tacticFail(), Native.tacticFailIf(), Native.tacticFailIfNotDecided(), Native.tacticGetDescr(), Native.tacticGetHelp(), Native.tacticGetParamDescrs(), Native.tacticIncRef(), Native.tacticOrElse(), Native.tacticParAndThen(), Native.tacticParOr(), Native.tacticRepeat(), Native.tacticSkip(), Native.tacticTryFor(), Native.tacticUsingParams(), Native.tacticWhen(), Native.toApp(), Native.toFuncDecl(), Native.translate(), Native.updateParamValue(), and Native.updateTerm().
|
staticprotected |
Referenced by Native.addConstInterp(), Native.addFuncInterp(), Native.addRecDef(), Native.algebraicAdd(), Native.algebraicDiv(), Native.algebraicEq(), Native.algebraicEval(), Native.algebraicGe(), Native.algebraicGt(), Native.algebraicIsNeg(), Native.algebraicIsPos(), Native.algebraicIsValue(), Native.algebraicIsZero(), Native.algebraicLe(), Native.algebraicLt(), Native.algebraicMul(), Native.algebraicNeq(), Native.algebraicPower(), Native.algebraicRoot(), Native.algebraicRoots(), Native.algebraicSign(), Native.algebraicSub(), Native.applyResultDecRef(), Native.applyResultGetNumSubgoals(), Native.applyResultGetSubgoal(), Native.applyResultIncRef(), Native.applyResultToString(), Native.appToAst(), Native.astMapContains(), Native.astMapDecRef(), Native.astMapErase(), Native.astMapFind(), Native.astMapIncRef(), Native.astMapInsert(), Native.astMapKeys(), Native.astMapReset(), Native.astMapSize(), Native.astMapToString(), Native.astToString(), Native.astVectorDecRef(), Native.astVectorGet(), Native.astVectorIncRef(), Native.astVectorPush(), Native.astVectorResize(), Native.astVectorSet(), Native.astVectorSize(), Native.astVectorToString(), Native.astVectorTranslate(), Native.benchmarkToSmtlibString(), Native.datatypeUpdateField(), Native.decRef(), Native.delConstructor(), Native.delConstructorList(), Native.evalSmtlib2String(), Native.fixedpointAddCover(), Native.fixedpointAddFact(), Native.fixedpointAddInvariant(), Native.fixedpointAddRule(), Native.fixedpointAssert(), Native.fixedpointDecRef(), Native.fixedpointFromFile(), Native.fixedpointFromString(), Native.fixedpointGetAnswer(), Native.fixedpointGetAssertions(), Native.fixedpointGetCoverDelta(), Native.fixedpointGetGroundSatAnswer(), Native.fixedpointGetHelp(), Native.fixedpointGetNumLevels(), Native.fixedpointGetParamDescrs(), Native.fixedpointGetReachable(), Native.fixedpointGetReasonUnknown(), Native.fixedpointGetRuleNamesAlongTrace(), Native.fixedpointGetRules(), Native.fixedpointGetRulesAlongTrace(), Native.fixedpointGetStatistics(), Native.fixedpointIncRef(), Native.fixedpointQuery(), Native.fixedpointQueryFromLvl(), Native.fixedpointQueryRelations(), Native.fixedpointRegisterRelation(), Native.fixedpointSetParams(), Native.fixedpointSetPredicateRepresentation(), Native.fixedpointToString(), Native.fixedpointUpdateRule(), Native.fpaGetEbits(), Native.fpaGetNumeralExponentBv(), Native.fpaGetNumeralExponentInt64(), Native.fpaGetNumeralExponentString(), Native.fpaGetNumeralSign(), Native.fpaGetNumeralSignBv(), Native.fpaGetNumeralSignificandBv(), Native.fpaGetNumeralSignificandString(), Native.fpaGetNumeralSignificandUint64(), Native.fpaGetSbits(), Native.fpaIsNumeralInf(), Native.fpaIsNumeralNan(), Native.fpaIsNumeralNegative(), Native.fpaIsNumeralNormal(), Native.fpaIsNumeralPositive(), Native.fpaIsNumeralSubnormal(), Native.fpaIsNumeralZero(), Native.funcDeclToAst(), Native.funcDeclToString(), Native.funcEntryDecRef(), Native.funcEntryGetArg(), Native.funcEntryGetNumArgs(), Native.funcEntryGetValue(), Native.funcEntryIncRef(), Native.funcInterpAddEntry(), Native.funcInterpDecRef(), Native.funcInterpGetArity(), Native.funcInterpGetElse(), Native.funcInterpGetEntry(), Native.funcInterpGetNumEntries(), Native.funcInterpIncRef(), Native.funcInterpSetElse(), Native.getAlgebraicNumberLower(), Native.getAlgebraicNumberUpper(), Native.getAppArg(), Native.getAppDecl(), Native.getAppNumArgs(), Native.getArity(), Native.getArraySortDomain(), Native.getArraySortRange(), Native.getAsArrayFuncDecl(), Native.getAstHash(), Native.getAstId(), Native.getAstKind(), Native.getBoolValue(), Native.getBvSortSize(), Native.getDatatypeSortConstructor(), Native.getDatatypeSortConstructorAccessor(), Native.getDatatypeSortNumConstructors(), Native.getDatatypeSortRecognizer(), Native.getDeclAstParameter(), Native.getDeclDoubleParameter(), Native.getDeclFuncDeclParameter(), Native.getDeclIntParameter(), Native.getDeclKind(), Native.getDeclName(), Native.getDeclNumParameters(), Native.getDeclParameterKind(), Native.getDeclRationalParameter(), Native.getDeclSortParameter(), Native.getDeclSymbolParameter(), Native.getDenominator(), Native.getDomain(), Native.getDomainSize(), Native.getErrorMsg(), Native.getFiniteDomainSortSize(), Native.getFuncDeclId(), Native.getImpliedEqualities(), Native.getIndexValue(), Native.getLstring(), Native.getNumeralDecimalString(), Native.getNumeralDouble(), Native.getNumeralInt(), Native.getNumeralInt64(), Native.getNumeralRationalInt64(), Native.getNumeralSmall(), Native.getNumeralString(), Native.getNumeralUint(), Native.getNumeralUint64(), Native.getNumerator(), Native.getNumProbes(), Native.getNumTactics(), Native.getPattern(), Native.getPatternNumTerms(), Native.getProbeName(), Native.getQuantifierBody(), Native.getQuantifierBoundName(), Native.getQuantifierBoundSort(), Native.getQuantifierNoPatternAst(), Native.getQuantifierNumBound(), Native.getQuantifierNumNoPatterns(), Native.getQuantifierNumPatterns(), Native.getQuantifierPatternAst(), Native.getQuantifierWeight(), Native.getRange(), Native.getRelationArity(), Native.getRelationColumn(), Native.getReSortBasis(), Native.getSeqSortBasis(), Native.getSort(), Native.getSortId(), Native.getSortKind(), Native.getSortName(), Native.getString(), Native.getSymbolInt(), Native.getSymbolKind(), Native.getSymbolString(), Native.getTacticName(), Native.getTupleSortFieldDecl(), Native.getTupleSortMkDecl(), Native.getTupleSortNumFields(), Native.goalAssert(), Native.goalConvertModel(), Native.goalDecRef(), Native.goalDepth(), Native.goalFormula(), Native.goalInconsistent(), Native.goalIncRef(), Native.goalIsDecidedSat(), Native.goalIsDecidedUnsat(), Native.goalNumExprs(), Native.goalPrecision(), Native.goalReset(), Native.goalSize(), Native.goalToDimacsString(), Native.goalToString(), Native.goalTranslate(), Native.incRef(), Native.interrupt(), Native.isAlgebraicNumber(), Native.isApp(), Native.isAsArray(), Native.isEqAst(), Native.isEqFuncDecl(), Native.isEqSort(), Native.isLambda(), Native.isNumeralAst(), Native.isQuantifierExists(), Native.isQuantifierForall(), Native.isReSort(), Native.isSeqSort(), Native.isString(), Native.isStringSort(), Native.isWellSorted(), Native.mkAdd(), Native.mkAnd(), Native.mkApp(), Native.mkArrayDefault(), Native.mkArrayExt(), Native.mkArraySort(), Native.mkArraySortN(), Native.mkAsArray(), Native.mkAstMap(), Native.mkAstVector(), Native.mkAtleast(), Native.mkAtmost(), Native.mkBoolSort(), Native.mkBound(), Native.mkBv2int(), Native.mkBvadd(), Native.mkBvaddNoOverflow(), Native.mkBvaddNoUnderflow(), Native.mkBvand(), Native.mkBvashr(), Native.mkBvlshr(), Native.mkBvmul(), Native.mkBvmulNoOverflow(), Native.mkBvmulNoUnderflow(), Native.mkBvnand(), Native.mkBvneg(), Native.mkBvnegNoOverflow(), Native.mkBvnor(), Native.mkBvnot(), Native.mkBvNumeral(), Native.mkBvor(), Native.mkBvredand(), Native.mkBvredor(), Native.mkBvsdiv(), Native.mkBvsdivNoOverflow(), Native.mkBvsge(), Native.mkBvsgt(), Native.mkBvshl(), Native.mkBvsle(), Native.mkBvslt(), Native.mkBvsmod(), Native.mkBvSort(), Native.mkBvsrem(), Native.mkBvsub(), Native.mkBvsubNoOverflow(), Native.mkBvsubNoUnderflow(), Native.mkBvudiv(), Native.mkBvuge(), Native.mkBvugt(), Native.mkBvule(), Native.mkBvult(), Native.mkBvurem(), Native.mkBvxnor(), Native.mkBvxor(), Native.mkConcat(), Native.mkConst(), Native.mkConstArray(), Native.mkConstructor(), Native.mkConstructorList(), Native.mkDatatype(), Native.mkDatatypes(), Native.mkDistinct(), Native.mkDiv(), Native.mkDivides(), Native.mkEmptySet(), Native.mkEnumerationSort(), Native.mkEq(), Native.mkExists(), Native.mkExistsConst(), Native.mkExtract(), Native.mkExtRotateLeft(), Native.mkExtRotateRight(), Native.mkFalse(), Native.mkFiniteDomainSort(), Native.mkFixedpoint(), Native.mkForall(), Native.mkForallConst(), Native.mkFpaAbs(), Native.mkFpaAdd(), Native.mkFpaDiv(), Native.mkFpaEq(), Native.mkFpaFma(), Native.mkFpaFp(), Native.mkFpaGeq(), Native.mkFpaGt(), Native.mkFpaInf(), Native.mkFpaIsInfinite(), Native.mkFpaIsNan(), Native.mkFpaIsNegative(), Native.mkFpaIsNormal(), Native.mkFpaIsPositive(), Native.mkFpaIsSubnormal(), Native.mkFpaIsZero(), Native.mkFpaLeq(), Native.mkFpaLt(), Native.mkFpaMax(), Native.mkFpaMin(), Native.mkFpaMul(), Native.mkFpaNan(), Native.mkFpaNeg(), Native.mkFpaNumeralDouble(), Native.mkFpaNumeralFloat(), Native.mkFpaNumeralInt(), Native.mkFpaNumeralInt64Uint64(), Native.mkFpaNumeralIntUint(), Native.mkFpaRem(), Native.mkFpaRna(), Native.mkFpaRne(), Native.mkFpaRoundingModeSort(), Native.mkFpaRoundNearestTiesToAway(), Native.mkFpaRoundNearestTiesToEven(), Native.mkFpaRoundToIntegral(), Native.mkFpaRoundTowardNegative(), Native.mkFpaRoundTowardPositive(), Native.mkFpaRoundTowardZero(), Native.mkFpaRtn(), Native.mkFpaRtp(), Native.mkFpaRtz(), Native.mkFpaSort(), Native.mkFpaSort128(), Native.mkFpaSort16(), Native.mkFpaSort32(), Native.mkFpaSort64(), Native.mkFpaSortDouble(), Native.mkFpaSortHalf(), Native.mkFpaSortQuadruple(), Native.mkFpaSortSingle(), Native.mkFpaSqrt(), Native.mkFpaSub(), Native.mkFpaToFpBv(), Native.mkFpaToFpFloat(), Native.mkFpaToFpIntReal(), Native.mkFpaToFpReal(), Native.mkFpaToFpSigned(), Native.mkFpaToFpUnsigned(), Native.mkFpaToIeeeBv(), Native.mkFpaToReal(), Native.mkFpaToSbv(), Native.mkFpaToUbv(), Native.mkFpaZero(), Native.mkFreshConst(), Native.mkFreshFuncDecl(), Native.mkFullSet(), Native.mkFuncDecl(), Native.mkGe(), Native.mkGoal(), Native.mkGt(), Native.mkIff(), Native.mkImplies(), Native.mkInt(), Native.mkInt2bv(), Native.mkInt2real(), Native.mkInt64(), Native.mkIntSort(), Native.mkIntSymbol(), Native.mkIntToStr(), Native.mkIsInt(), Native.mkIte(), Native.mkLambda(), Native.mkLambdaConst(), Native.mkLe(), Native.mkLinearOrder(), Native.mkListSort(), Native.mkLstring(), Native.mkLt(), Native.mkMap(), Native.mkMod(), Native.mkModel(), Native.mkMul(), Native.mkNot(), Native.mkNumeral(), Native.mkOptimize(), Native.mkOr(), Native.mkParams(), Native.mkPartialOrder(), Native.mkPattern(), Native.mkPbeq(), Native.mkPbge(), Native.mkPble(), Native.mkPiecewiseLinearOrder(), Native.mkPower(), Native.mkProbe(), Native.mkQuantifier(), Native.mkQuantifierConst(), Native.mkQuantifierConstEx(), Native.mkQuantifierEx(), Native.mkReal(), Native.mkReal2int(), Native.mkRealSort(), Native.mkRecFuncDecl(), Native.mkReComplement(), Native.mkReConcat(), Native.mkReEmpty(), Native.mkReFull(), Native.mkReIntersect(), Native.mkReLoop(), Native.mkRem(), Native.mkReOption(), Native.mkRepeat(), Native.mkRePlus(), Native.mkReRange(), Native.mkReSort(), Native.mkReStar(), Native.mkReUnion(), Native.mkRotateLeft(), Native.mkRotateRight(), Native.mkSelect(), Native.mkSelectN(), Native.mkSeqAt(), Native.mkSeqConcat(), Native.mkSeqContains(), Native.mkSeqEmpty(), Native.mkSeqExtract(), Native.mkSeqIndex(), Native.mkSeqInRe(), Native.mkSeqLastIndex(), Native.mkSeqLength(), Native.mkSeqNth(), Native.mkSeqPrefix(), Native.mkSeqReplace(), Native.mkSeqSort(), Native.mkSeqSuffix(), Native.mkSeqToRe(), Native.mkSeqUnit(), Native.mkSetAdd(), Native.mkSetComplement(), Native.mkSetDel(), Native.mkSetDifference(), Native.mkSetHasSize(), Native.mkSetIntersect(), Native.mkSetMember(), Native.mkSetSort(), Native.mkSetSubset(), Native.mkSetUnion(), Native.mkSignExt(), Native.mkSimpleSolver(), Native.mkSolver(), Native.mkSolverForLogic(), Native.mkSolverFromTactic(), Native.mkStore(), Native.mkStoreN(), Native.mkString(), Native.mkStringSort(), Native.mkStringSymbol(), Native.mkStrLe(), Native.mkStrLt(), Native.mkStrToInt(), Native.mkSub(), Native.mkTactic(), Native.mkTransitiveClosure(), Native.mkTreeOrder(), Native.mkTrue(), Native.mkTupleSort(), Native.mkUnaryMinus(), Native.mkUninterpretedSort(), Native.mkUnsignedInt(), Native.mkUnsignedInt64(), Native.mkXor(), Native.mkZeroExt(), Native.modelDecRef(), Native.modelEval(), Native.modelExtrapolate(), Native.modelGetConstDecl(), Native.modelGetConstInterp(), Native.modelGetFuncDecl(), Native.modelGetFuncInterp(), Native.modelGetNumConsts(), Native.modelGetNumFuncs(), Native.modelGetNumSorts(), Native.modelGetSort(), Native.modelGetSortUniverse(), Native.modelHasInterp(), Native.modelIncRef(), Native.modelToString(), Native.modelTranslate(), Native.optimizeAssert(), Native.optimizeAssertAndTrack(), Native.optimizeAssertSoft(), Native.optimizeCheck(), Native.optimizeDecRef(), Native.optimizeFromFile(), Native.optimizeFromString(), Native.optimizeGetAssertions(), Native.optimizeGetHelp(), Native.optimizeGetLower(), Native.optimizeGetLowerAsVector(), Native.optimizeGetModel(), Native.optimizeGetObjectives(), Native.optimizeGetParamDescrs(), Native.optimizeGetReasonUnknown(), Native.optimizeGetStatistics(), Native.optimizeGetUnsatCore(), Native.optimizeGetUpper(), Native.optimizeGetUpperAsVector(), Native.optimizeIncRef(), Native.optimizeMaximize(), Native.optimizeMinimize(), Native.optimizePop(), Native.optimizePush(), Native.optimizeSetParams(), Native.optimizeToString(), Native.paramDescrsDecRef(), Native.paramDescrsGetDocumentation(), Native.paramDescrsGetKind(), Native.paramDescrsGetName(), Native.paramDescrsIncRef(), Native.paramDescrsSize(), Native.paramDescrsToString(), Native.paramsDecRef(), Native.paramsIncRef(), Native.paramsSetBool(), Native.paramsSetDouble(), Native.paramsSetSymbol(), Native.paramsSetUint(), Native.paramsToString(), Native.paramsValidate(), Native.parseSmtlib2File(), Native.parseSmtlib2String(), Native.patternToAst(), Native.patternToString(), Native.polynomialSubresultants(), Native.probeAnd(), Native.probeApply(), Native.probeConst(), Native.probeDecRef(), Native.probeEq(), Native.probeGe(), Native.probeGetDescr(), Native.probeGt(), Native.probeIncRef(), Native.probeLe(), Native.probeLt(), Native.probeNot(), Native.probeOr(), Native.qeLite(), Native.qeModelProject(), Native.qeModelProjectSkolem(), Native.queryConstructor(), Native.rcfAdd(), Native.rcfDel(), Native.rcfDiv(), Native.rcfEq(), Native.rcfGe(), Native.rcfGetNumeratorDenominator(), Native.rcfGt(), Native.rcfInv(), Native.rcfLe(), Native.rcfLt(), Native.rcfMkE(), Native.rcfMkInfinitesimal(), Native.rcfMkPi(), Native.rcfMkRational(), Native.rcfMkRoots(), Native.rcfMkSmallInt(), Native.rcfMul(), Native.rcfNeg(), Native.rcfNeq(), Native.rcfNumToDecimalString(), Native.rcfNumToString(), Native.rcfPower(), Native.rcfSub(), Native.setAstPrintMode(), Native.setError(), Native.simplify(), Native.simplifyEx(), Native.simplifyGetHelp(), Native.simplifyGetParamDescrs(), Native.solverAssert(), Native.solverAssertAndTrack(), Native.solverCheck(), Native.solverCheckAssumptions(), Native.solverCube(), Native.solverDecRef(), Native.solverFromFile(), Native.solverFromString(), Native.solverGetAssertions(), Native.solverGetConsequences(), Native.solverGetHelp(), Native.solverGetLevels(), Native.solverGetModel(), Native.solverGetNonUnits(), Native.solverGetNumScopes(), Native.solverGetParamDescrs(), Native.solverGetProof(), Native.solverGetReasonUnknown(), Native.solverGetStatistics(), Native.solverGetTrail(), Native.solverGetUnits(), Native.solverGetUnsatCore(), Native.solverImportModelConverter(), Native.solverIncRef(), Native.solverInterrupt(), Native.solverPop(), Native.solverPush(), Native.solverReset(), Native.solverSetParams(), Native.solverToDimacsString(), Native.solverToString(), Native.solverTranslate(), Native.sortToAst(), Native.sortToString(), Native.statsDecRef(), Native.statsGetDoubleValue(), Native.statsGetKey(), Native.statsGetUintValue(), Native.statsIncRef(), Native.statsIsDouble(), Native.statsIsUint(), Native.statsSize(), Native.statsToString(), Native.substitute(), Native.substituteVars(), Native.tacticAndThen(), Native.tacticApply(), Native.tacticApplyEx(), Native.tacticCond(), Native.tacticDecRef(), Native.tacticFail(), Native.tacticFailIf(), Native.tacticFailIfNotDecided(), Native.tacticGetDescr(), Native.tacticGetHelp(), Native.tacticGetParamDescrs(), Native.tacticIncRef(), Native.tacticOrElse(), Native.tacticParAndThen(), Native.tacticParOr(), Native.tacticRepeat(), Native.tacticSkip(), Native.tacticTryFor(), Native.tacticUsingParams(), Native.tacticWhen(), Native.toApp(), Native.toFuncDecl(), Native.translate(), Native.updateParamValue(), and Native.updateTerm().
|
staticprotected |
Referenced by Native.getEstimatedAllocSize().
|
staticprotected |
Referenced by Native.getFiniteDomainSortSize().
|
staticprotected |
Referenced by Native.getFullVersion().
|
staticprotected |
Referenced by Native.getFuncDeclId().
|
staticprotected |
Referenced by Native.getImpliedEqualities().
|
staticprotected |
Referenced by Native.getIndexValue().
|
staticprotected |
Referenced by Native.getLstring().
|
staticprotected |
Referenced by Native.getNumeralDecimalString().
|
staticprotected |
Referenced by Native.getNumeralDouble().
|
staticprotected |
Referenced by Native.getNumeralInt().
|
staticprotected |
Referenced by Native.getNumeralInt64().
|
staticprotected |
Referenced by Native.getNumeralRationalInt64().
|
staticprotected |
Referenced by Native.getNumeralSmall().
|
staticprotected |
Referenced by Native.getNumeralString().
|
staticprotected |
Referenced by Native.getNumeralUint().
|
staticprotected |
Referenced by Native.getNumeralUint64().
|
staticprotected |
Referenced by Native.getNumerator().
|
staticprotected |
Referenced by Native.getNumProbes().
|
staticprotected |
Referenced by Native.getNumTactics().
|
staticprotected |
Referenced by Native.getPattern().
|
staticprotected |
Referenced by Native.getPatternNumTerms().
|
staticprotected |
Referenced by Native.getProbeName().
|
staticprotected |
Referenced by Native.getQuantifierBody().
|
staticprotected |
Referenced by Native.getQuantifierBoundName().
|
staticprotected |
Referenced by Native.getQuantifierBoundSort().
|
staticprotected |
Referenced by Native.getQuantifierNoPatternAst().
|
staticprotected |
Referenced by Native.getQuantifierNumBound().
|
staticprotected |
Referenced by Native.getQuantifierNumNoPatterns().
|
staticprotected |
Referenced by Native.getQuantifierNumPatterns().
|
staticprotected |
Referenced by Native.getQuantifierPatternAst().
|
staticprotected |
Referenced by Native.getQuantifierWeight().
|
staticprotected |
Referenced by Native.getRange().
|
staticprotected |
Referenced by Native.getRelationArity().
|
staticprotected |
Referenced by Native.getRelationColumn().
|
staticprotected |
Referenced by Native.getReSortBasis().
|
staticprotected |
Referenced by Native.getSeqSortBasis().
|
staticprotected |
Referenced by Native.getSort().
|
staticprotected |
Referenced by Native.getSortId().
|
staticprotected |
Referenced by Native.getSortKind().
|
staticprotected |
Referenced by Native.getSortName().
|
staticprotected |
Referenced by Native.getString().
|
staticprotected |
Referenced by Native.getSymbolInt().
|
staticprotected |
Referenced by Native.getSymbolKind().
|
staticprotected |
Referenced by Native.getSymbolString().
|
staticprotected |
Referenced by Native.getTacticName().
|
staticprotected |
Referenced by Native.getTupleSortFieldDecl().
|
staticprotected |
Referenced by Native.getTupleSortMkDecl().
|
staticprotected |
Referenced by Native.getTupleSortNumFields().
|
staticprotected |
Referenced by Native.getVersion().
|
staticprotected |
Referenced by Native.globalParamGet().
|
staticprotected |
Referenced by Native.globalParamResetAll().
|
staticprotected |
Referenced by Native.globalParamSet().
|
staticprotected |
Referenced by Native.goalAssert().
|
staticprotected |
Referenced by Native.goalConvertModel().
|
staticprotected |
Referenced by Native.goalDecRef().
|
staticprotected |
Referenced by Native.goalDepth().
|
staticprotected |
Referenced by Native.goalFormula().
|
staticprotected |
Referenced by Native.goalInconsistent().
|
staticprotected |
Referenced by Native.goalIncRef().
|
staticprotected |
Referenced by Native.goalIsDecidedSat().
|
staticprotected |
Referenced by Native.goalIsDecidedUnsat().
|
staticprotected |
Referenced by Native.goalNumExprs().
|
staticprotected |
Referenced by Native.goalPrecision().
|
staticprotected |
Referenced by Native.goalReset().
|
staticprotected |
Referenced by Native.goalSize().
|
staticprotected |
Referenced by Native.goalToDimacsString().
|
staticprotected |
Referenced by Native.goalToString().
|
staticprotected |
Referenced by Native.goalTranslate().
|
staticprotected |
Referenced by Native.incRef().
|
staticprotected |
Referenced by Native.interrupt().
|
staticprotected |
Referenced by Native.isAlgebraicNumber().
|
staticprotected |
Referenced by Native.isApp().
|
staticprotected |
Referenced by Native.isAsArray().
|
staticprotected |
Referenced by Native.isEqAst().
|
staticprotected |
Referenced by Native.isEqFuncDecl().
|
staticprotected |
Referenced by Native.isEqSort().
|
staticprotected |
Referenced by Native.isLambda().
|
staticprotected |
Referenced by Native.isNumeralAst().
|
staticprotected |
Referenced by Native.isQuantifierExists().
|
staticprotected |
Referenced by Native.isQuantifierForall().
|
staticprotected |
Referenced by Native.isReSort().
|
staticprotected |
Referenced by Native.isSeqSort().
|
staticprotected |
Referenced by Native.isString().
|
staticprotected |
Referenced by Native.isStringSort().
|
staticprotected |
Referenced by Native.isWellSorted().
|
staticprotected |
Referenced by Native.mkAdd().
|
staticprotected |
Referenced by Native.mkAnd().
|
staticprotected |
Referenced by Native.mkApp().
|
staticprotected |
Referenced by Native.mkArrayDefault().
|
staticprotected |
Referenced by Native.mkArrayExt().
|
staticprotected |
Referenced by Native.mkArraySort().
|
staticprotected |
Referenced by Native.mkArraySortN().
|
staticprotected |
Referenced by Native.mkAsArray().
|
staticprotected |
Referenced by Native.mkAstMap().
|
staticprotected |
Referenced by Native.mkAstVector().
|
staticprotected |
Referenced by Native.mkAtleast().
|
staticprotected |
Referenced by Native.mkAtmost().
|
staticprotected |
Referenced by Native.mkBoolSort().
|
staticprotected |
Referenced by Native.mkBound().
|
staticprotected |
Referenced by Native.mkBv2int().
|
staticprotected |
Referenced by Native.mkBvadd().
|
staticprotected |
Referenced by Native.mkBvaddNoOverflow().
|
staticprotected |
Referenced by Native.mkBvaddNoUnderflow().
|
staticprotected |
Referenced by Native.mkBvand().
|
staticprotected |
Referenced by Native.mkBvashr().
|
staticprotected |
Referenced by Native.mkBvlshr().
|
staticprotected |
Referenced by Native.mkBvmul().
|
staticprotected |
Referenced by Native.mkBvmulNoOverflow().
|
staticprotected |
Referenced by Native.mkBvmulNoUnderflow().
|
staticprotected |
Referenced by Native.mkBvnand().
|
staticprotected |
Referenced by Native.mkBvneg().
|
staticprotected |
Referenced by Native.mkBvnegNoOverflow().
|
staticprotected |
Referenced by Native.mkBvnor().
|
staticprotected |
Referenced by Native.mkBvnot().
|
staticprotected |
Referenced by Native.mkBvNumeral().
|
staticprotected |
Referenced by Native.mkBvor().
|
staticprotected |
Referenced by Native.mkBvredand().
|
staticprotected |
Referenced by Native.mkBvredor().
|
staticprotected |
Referenced by Native.mkBvsdiv().
|
staticprotected |
Referenced by Native.mkBvsdivNoOverflow().
|
staticprotected |
Referenced by Native.mkBvsge().
|
staticprotected |
Referenced by Native.mkBvsgt().
|
staticprotected |
Referenced by Native.mkBvshl().
|
staticprotected |
Referenced by Native.mkBvsle().
|
staticprotected |
Referenced by Native.mkBvslt().
|
staticprotected |
Referenced by Native.mkBvsmod().
|
staticprotected |
Referenced by Native.mkBvSort().
|
staticprotected |
Referenced by Native.mkBvsrem().
|
staticprotected |
Referenced by Native.mkBvsub().
|
staticprotected |
Referenced by Native.mkBvsubNoOverflow().
|
staticprotected |
Referenced by Native.mkBvsubNoUnderflow().
|
staticprotected |
Referenced by Native.mkBvudiv().
|
staticprotected |
Referenced by Native.mkBvuge().
|
staticprotected |
Referenced by Native.mkBvugt().
|
staticprotected |
Referenced by Native.mkBvule().
|
staticprotected |
Referenced by Native.mkBvult().
|
staticprotected |
Referenced by Native.mkBvurem().
|
staticprotected |
Referenced by Native.mkBvxnor().
|
staticprotected |
Referenced by Native.mkBvxor().
|
staticprotected |
Referenced by Native.mkConcat().
|
staticprotected |
Referenced by Native.mkConfig().
|
staticprotected |
Referenced by Native.mkConst().
|
staticprotected |
Referenced by Native.mkConstArray().
|
staticprotected |
Referenced by Native.mkConstructor().
|
staticprotected |
Referenced by Native.mkConstructorList().
|
staticprotected |
Referenced by Native.mkContext().
|
staticprotected |
Referenced by Native.mkContextRc().
|
staticprotected |
Referenced by Native.mkDatatype().
|
staticprotected |
Referenced by Native.mkDatatypes().
|
staticprotected |
Referenced by Native.mkDistinct().
|
staticprotected |
Referenced by Native.mkDiv().
|
staticprotected |
Referenced by Native.mkDivides().
|
staticprotected |
Referenced by Native.mkEmptySet().
|
staticprotected |
Referenced by Native.mkEnumerationSort().
|
staticprotected |
Referenced by Native.mkEq().
|
staticprotected |
Referenced by Native.mkExists().
|
staticprotected |
Referenced by Native.mkExistsConst().
|
staticprotected |
Referenced by Native.mkExtract().
|
staticprotected |
Referenced by Native.mkExtRotateLeft().
|
staticprotected |
Referenced by Native.mkExtRotateRight().
|
staticprotected |
Referenced by Native.mkFalse().
|
staticprotected |
Referenced by Native.mkFiniteDomainSort().
|
staticprotected |
Referenced by Native.mkFixedpoint().
|
staticprotected |
Referenced by Native.mkForall().
|
staticprotected |
Referenced by Native.mkForallConst().
|
staticprotected |
Referenced by Native.mkFpaAbs().
|
staticprotected |
Referenced by Native.mkFpaAdd().
|
staticprotected |
Referenced by Native.mkFpaDiv().
|
staticprotected |
Referenced by Native.mkFpaEq().
|
staticprotected |
Referenced by Native.mkFpaFma().
|
staticprotected |
Referenced by Native.mkFpaFp().
|
staticprotected |
Referenced by Native.mkFpaGeq().
|
staticprotected |
Referenced by Native.mkFpaGt().
|
staticprotected |
Referenced by Native.mkFpaInf().
|
staticprotected |
Referenced by Native.mkFpaIsInfinite().
|
staticprotected |
Referenced by Native.mkFpaIsNan().
|
staticprotected |
Referenced by Native.mkFpaIsNegative().
|
staticprotected |
Referenced by Native.mkFpaIsNormal().
|
staticprotected |
Referenced by Native.mkFpaIsPositive().
|
staticprotected |
Referenced by Native.mkFpaIsSubnormal().
|
staticprotected |
Referenced by Native.mkFpaIsZero().
|
staticprotected |
Referenced by Native.mkFpaLeq().
|
staticprotected |
Referenced by Native.mkFpaLt().
|
staticprotected |
Referenced by Native.mkFpaMax().
|
staticprotected |
Referenced by Native.mkFpaMin().
|
staticprotected |
Referenced by Native.mkFpaMul().
|
staticprotected |
Referenced by Native.mkFpaNan().
|
staticprotected |
Referenced by Native.mkFpaNeg().
|
staticprotected |
Referenced by Native.mkFpaNumeralDouble().
|
staticprotected |
Referenced by Native.mkFpaNumeralFloat().
|
staticprotected |
Referenced by Native.mkFpaNumeralInt().
|
staticprotected |
Referenced by Native.mkFpaNumeralInt64Uint64().
|
staticprotected |
Referenced by Native.mkFpaNumeralIntUint().
|
staticprotected |
Referenced by Native.mkFpaRem().
|
staticprotected |
Referenced by Native.mkFpaRna().
|
staticprotected |
Referenced by Native.mkFpaRne().
|
staticprotected |
Referenced by Native.mkFpaRoundingModeSort().
|
staticprotected |
Referenced by Native.mkFpaRoundNearestTiesToAway().
|
staticprotected |
Referenced by Native.mkFpaRoundNearestTiesToEven().
|
staticprotected |
Referenced by Native.mkFpaRoundToIntegral().
|
staticprotected |
Referenced by Native.mkFpaRoundTowardNegative().
|
staticprotected |
Referenced by Native.mkFpaRoundTowardPositive().
|
staticprotected |
Referenced by Native.mkFpaRoundTowardZero().
|
staticprotected |
Referenced by Native.mkFpaRtn().
|
staticprotected |
Referenced by Native.mkFpaRtp().
|
staticprotected |
Referenced by Native.mkFpaRtz().
|
staticprotected |
Referenced by Native.mkFpaSort().
|
staticprotected |
Referenced by Native.mkFpaSort128().
|
staticprotected |
Referenced by Native.mkFpaSort16().
|
staticprotected |
Referenced by Native.mkFpaSort32().
|
staticprotected |
Referenced by Native.mkFpaSort64().
|
staticprotected |
Referenced by Native.mkFpaSortDouble().
|
staticprotected |
Referenced by Native.mkFpaSortHalf().
|
staticprotected |
Referenced by Native.mkFpaSortQuadruple().
|
staticprotected |
Referenced by Native.mkFpaSortSingle().
|
staticprotected |
Referenced by Native.mkFpaSqrt().
|
staticprotected |
Referenced by Native.mkFpaSub().
|
staticprotected |
Referenced by Native.mkFpaToFpBv().
|
staticprotected |
Referenced by Native.mkFpaToFpFloat().
|
staticprotected |
Referenced by Native.mkFpaToFpIntReal().
|
staticprotected |
Referenced by Native.mkFpaToFpReal().
|
staticprotected |
Referenced by Native.mkFpaToFpSigned().
|
staticprotected |
Referenced by Native.mkFpaToFpUnsigned().
|
staticprotected |
Referenced by Native.mkFpaToIeeeBv().
|
staticprotected |
Referenced by Native.mkFpaToReal().
|
staticprotected |
Referenced by Native.mkFpaToSbv().
|
staticprotected |
Referenced by Native.mkFpaToUbv().
|
staticprotected |
Referenced by Native.mkFpaZero().
|
staticprotected |
Referenced by Native.mkFreshConst().
|
staticprotected |
Referenced by Native.mkFreshFuncDecl().
|
staticprotected |
Referenced by Native.mkFullSet().
|
staticprotected |
Referenced by Native.mkFuncDecl().
|
staticprotected |
Referenced by Native.mkGe().
|
staticprotected |
Referenced by Native.mkGoal().
|
staticprotected |
Referenced by Native.mkGt().
|
staticprotected |
Referenced by Native.mkIff().
|
staticprotected |
Referenced by Native.mkImplies().
|
staticprotected |
Referenced by Native.mkInt().
|
staticprotected |
Referenced by Native.mkInt2bv().
|
staticprotected |
Referenced by Native.mkInt2real().
|
staticprotected |
Referenced by Native.mkInt64().
|
staticprotected |
Referenced by Native.mkIntSort().
|
staticprotected |
Referenced by Native.mkIntSymbol().
|
staticprotected |
Referenced by Native.mkIntToStr().
|
staticprotected |
Referenced by Native.mkIsInt().
|
staticprotected |
Referenced by Native.mkIte().
|
staticprotected |
Referenced by Native.mkLambda().
|
staticprotected |
Referenced by Native.mkLambdaConst().
|
staticprotected |
Referenced by Native.mkLe().
|
staticprotected |
Referenced by Native.mkLinearOrder().
|
staticprotected |
Referenced by Native.mkListSort().
|
staticprotected |
Referenced by Native.mkLstring().
|
staticprotected |
Referenced by Native.mkLt().
|
staticprotected |
Referenced by Native.mkMap().
|
staticprotected |
Referenced by Native.mkMod().
|
staticprotected |
Referenced by Native.mkModel().
|
staticprotected |
Referenced by Native.mkMul().
|
staticprotected |
Referenced by Native.mkNot().
|
staticprotected |
Referenced by Native.mkNumeral().
|
staticprotected |
Referenced by Native.mkOptimize().
|
staticprotected |
Referenced by Native.mkOr().
|
staticprotected |
Referenced by Native.mkParams().
|
staticprotected |
Referenced by Native.mkPartialOrder().
|
staticprotected |
Referenced by Native.mkPattern().
|
staticprotected |
Referenced by Native.mkPbeq().
|
staticprotected |
Referenced by Native.mkPbge().
|
staticprotected |
Referenced by Native.mkPble().
|
staticprotected |
Referenced by Native.mkPiecewiseLinearOrder().
|
staticprotected |
Referenced by Native.mkPower().
|
staticprotected |
Referenced by Native.mkProbe().
|
staticprotected |
Referenced by Native.mkQuantifier().
|
staticprotected |
Referenced by Native.mkQuantifierConst().
|
staticprotected |
Referenced by Native.mkQuantifierConstEx().
|
staticprotected |
Referenced by Native.mkQuantifierEx().
|
staticprotected |
Referenced by Native.mkReal().
|
staticprotected |
Referenced by Native.mkReal2int().
|
staticprotected |
Referenced by Native.mkRealSort().
|
staticprotected |
Referenced by Native.mkRecFuncDecl().
|
staticprotected |
Referenced by Native.mkReComplement().
|
staticprotected |
Referenced by Native.mkReConcat().
|
staticprotected |
Referenced by Native.mkReEmpty().
|
staticprotected |
Referenced by Native.mkReFull().
|
staticprotected |
Referenced by Native.mkReIntersect().
|
staticprotected |
Referenced by Native.mkReLoop().
|
staticprotected |
Referenced by Native.mkRem().
|
staticprotected |
Referenced by Native.mkReOption().
|
staticprotected |
Referenced by Native.mkRepeat().
|
staticprotected |
Referenced by Native.mkRePlus().
|
staticprotected |
Referenced by Native.mkReRange().
|
staticprotected |
Referenced by Native.mkReSort().
|
staticprotected |
Referenced by Native.mkReStar().
|
staticprotected |
Referenced by Native.mkReUnion().
|
staticprotected |
Referenced by Native.mkRotateLeft().
|
staticprotected |
Referenced by Native.mkRotateRight().
|
staticprotected |
Referenced by Native.mkSelect().
|
staticprotected |
Referenced by Native.mkSelectN().
|
staticprotected |
Referenced by Native.mkSeqAt().
|
staticprotected |
Referenced by Native.mkSeqConcat().
|
staticprotected |
Referenced by Native.mkSeqContains().
|
staticprotected |
Referenced by Native.mkSeqEmpty().
|
staticprotected |
Referenced by Native.mkSeqExtract().
|
staticprotected |
Referenced by Native.mkSeqIndex().
|
staticprotected |
Referenced by Native.mkSeqInRe().
|
staticprotected |
Referenced by Native.mkSeqLastIndex().
|
staticprotected |
Referenced by Native.mkSeqLength().
|
staticprotected |
Referenced by Native.mkSeqNth().
|
staticprotected |
Referenced by Native.mkSeqPrefix().
|
staticprotected |
Referenced by Native.mkSeqReplace().
|
staticprotected |
Referenced by Native.mkSeqSort().
|
staticprotected |
Referenced by Native.mkSeqSuffix().
|
staticprotected |
Referenced by Native.mkSeqToRe().
|
staticprotected |
Referenced by Native.mkSeqUnit().
|
staticprotected |
Referenced by Native.mkSetAdd().
|
staticprotected |
Referenced by Native.mkSetComplement().
|
staticprotected |
Referenced by Native.mkSetDel().
|
staticprotected |
Referenced by Native.mkSetDifference().
|
staticprotected |
Referenced by Native.mkSetHasSize().
|
staticprotected |
Referenced by Native.mkSetIntersect().
|
staticprotected |
Referenced by Native.mkSetMember().
|
staticprotected |
Referenced by Native.mkSetSort().
|
staticprotected |
Referenced by Native.mkSetSubset().
|
staticprotected |
Referenced by Native.mkSetUnion().
|
staticprotected |
Referenced by Native.mkSignExt().
|
staticprotected |
Referenced by Native.mkSimpleSolver().
|
staticprotected |
Referenced by Native.mkSolver().
|
staticprotected |
Referenced by Native.mkSolverForLogic().
|
staticprotected |
Referenced by Native.mkSolverFromTactic().
|
staticprotected |
Referenced by Native.mkStore().
|
staticprotected |
Referenced by Native.mkStoreN().
|
staticprotected |
Referenced by Native.mkString().
|
staticprotected |
Referenced by Native.mkStringSort().
|
staticprotected |
Referenced by Native.mkStringSymbol().
|
staticprotected |
Referenced by Native.mkStrLe().
|
staticprotected |
Referenced by Native.mkStrLt().
|
staticprotected |
Referenced by Native.mkStrToInt().
|
staticprotected |
Referenced by Native.mkSub().
|
staticprotected |
Referenced by Native.mkTactic().
|
staticprotected |
Referenced by Native.mkTransitiveClosure().
|
staticprotected |
Referenced by Native.mkTreeOrder().
|
staticprotected |
Referenced by Native.mkTrue().
|
staticprotected |
Referenced by Native.mkTupleSort().
|
staticprotected |
Referenced by Native.mkUnaryMinus().
|
staticprotected |
Referenced by Native.mkUninterpretedSort().
|
staticprotected |
Referenced by Native.mkUnsignedInt().
|
staticprotected |
Referenced by Native.mkUnsignedInt64().
|
staticprotected |
Referenced by Native.mkXor().
|
staticprotected |
Referenced by Native.mkZeroExt().
|
staticprotected |
Referenced by Native.modelDecRef().
|
staticprotected |
Referenced by Native.modelEval().
|
staticprotected |
Referenced by Native.modelExtrapolate().
|
staticprotected |
Referenced by Native.modelGetConstDecl().
|
staticprotected |
Referenced by Native.modelGetConstInterp().
|
staticprotected |
Referenced by Native.modelGetFuncDecl().
|
staticprotected |
Referenced by Native.modelGetFuncInterp().
|
staticprotected |
Referenced by Native.modelGetNumConsts().
|
staticprotected |
Referenced by Native.modelGetNumFuncs().
|
staticprotected |
Referenced by Native.modelGetNumSorts().
|
staticprotected |
Referenced by Native.modelGetSort().
|
staticprotected |
Referenced by Native.modelGetSortUniverse().
|
staticprotected |
Referenced by Native.modelHasInterp().
|
staticprotected |
Referenced by Native.modelIncRef().
|
staticprotected |
Referenced by Native.modelToString().
|
staticprotected |
Referenced by Native.modelTranslate().
|
staticprotected |
Referenced by Native.openLog().
|
staticprotected |
Referenced by Native.optimizeAssert().
|
staticprotected |
Referenced by Native.optimizeAssertAndTrack().
|
staticprotected |
Referenced by Native.optimizeAssertSoft().
|
staticprotected |
Referenced by Native.optimizeCheck().
|
staticprotected |
Referenced by Native.optimizeDecRef().
|
staticprotected |
Referenced by Native.optimizeFromFile().
|
staticprotected |
Referenced by Native.optimizeFromString().
|
staticprotected |
Referenced by Native.optimizeGetAssertions().
|
staticprotected |
Referenced by Native.optimizeGetHelp().
|
staticprotected |
Referenced by Native.optimizeGetLower().
|
staticprotected |
Referenced by Native.optimizeGetLowerAsVector().
|
staticprotected |
Referenced by Native.optimizeGetModel().
|
staticprotected |
Referenced by Native.optimizeGetObjectives().
|
staticprotected |
Referenced by Native.optimizeGetParamDescrs().
|
staticprotected |
Referenced by Native.optimizeGetReasonUnknown().
|
staticprotected |
Referenced by Native.optimizeGetStatistics().
|
staticprotected |
Referenced by Native.optimizeGetUnsatCore().
|
staticprotected |
Referenced by Native.optimizeGetUpper().
|
staticprotected |
Referenced by Native.optimizeGetUpperAsVector().
|
staticprotected |
Referenced by Native.optimizeIncRef().
|
staticprotected |
Referenced by Native.optimizeMaximize().
|
staticprotected |
Referenced by Native.optimizeMinimize().
|
staticprotected |
Referenced by Native.optimizePop().
|
staticprotected |
Referenced by Native.optimizePush().
|
staticprotected |
Referenced by Native.optimizeSetParams().
|
staticprotected |
Referenced by Native.optimizeToString().
|
staticprotected |
Referenced by Native.paramDescrsDecRef().
|
staticprotected |
Referenced by Native.paramDescrsGetDocumentation().
|
staticprotected |
Referenced by Native.paramDescrsGetKind().
|
staticprotected |
Referenced by Native.paramDescrsGetName().
|
staticprotected |
Referenced by Native.paramDescrsIncRef().
|
staticprotected |
Referenced by Native.paramDescrsSize().
|
staticprotected |
Referenced by Native.paramDescrsToString().
|
staticprotected |
Referenced by Native.paramsDecRef().
|
staticprotected |
Referenced by Native.paramsIncRef().
|
staticprotected |
Referenced by Native.paramsSetBool().
|
staticprotected |
Referenced by Native.paramsSetDouble().
|
staticprotected |
Referenced by Native.paramsSetSymbol().
|
staticprotected |
Referenced by Native.paramsSetUint().
|
staticprotected |
Referenced by Native.paramsToString().
|
staticprotected |
Referenced by Native.paramsValidate().
|
staticprotected |
Referenced by Native.parseSmtlib2File().
|
staticprotected |
Referenced by Native.parseSmtlib2String().
|
staticprotected |
Referenced by Native.patternToAst().
|
staticprotected |
Referenced by Native.patternToString().
|
staticprotected |
Referenced by Native.polynomialSubresultants().
|
staticprotected |
Referenced by Native.probeAnd().
|
staticprotected |
Referenced by Native.probeApply().
|
staticprotected |
Referenced by Native.probeConst().
|
staticprotected |
Referenced by Native.probeDecRef().
|
staticprotected |
Referenced by Native.probeEq().
|
staticprotected |
Referenced by Native.probeGe().
|
staticprotected |
Referenced by Native.probeGetDescr().
|
staticprotected |
Referenced by Native.probeGt().
|
staticprotected |
Referenced by Native.probeIncRef().
|
staticprotected |
Referenced by Native.probeLe().
|
staticprotected |
Referenced by Native.probeLt().
|
staticprotected |
Referenced by Native.probeNot().
|
staticprotected |
Referenced by Native.probeOr().
|
staticprotected |
Referenced by Native.qeLite().
|
staticprotected |
Referenced by Native.qeModelProject().
|
staticprotected |
Referenced by Native.qeModelProjectSkolem().
|
staticprotected |
Referenced by Native.queryConstructor().
|
staticprotected |
Referenced by Native.rcfAdd().
|
staticprotected |
Referenced by Native.rcfDel().
|
staticprotected |
Referenced by Native.rcfDiv().
|
staticprotected |
Referenced by Native.rcfEq().
|
staticprotected |
Referenced by Native.rcfGe().
|
staticprotected |
Referenced by Native.rcfGetNumeratorDenominator().
|
staticprotected |
Referenced by Native.rcfGt().
|
staticprotected |
Referenced by Native.rcfInv().
|
staticprotected |
Referenced by Native.rcfLe().
|
staticprotected |
Referenced by Native.rcfLt().
|
staticprotected |
Referenced by Native.rcfMkE().
|
staticprotected |
Referenced by Native.rcfMkInfinitesimal().
|
staticprotected |
Referenced by Native.rcfMkPi().
|
staticprotected |
Referenced by Native.rcfMkRational().
|
staticprotected |
Referenced by Native.rcfMkRoots().
|
staticprotected |
Referenced by Native.rcfMkSmallInt().
|
staticprotected |
Referenced by Native.rcfMul().
|
staticprotected |
Referenced by Native.rcfNeg().
|
staticprotected |
Referenced by Native.rcfNeq().
|
staticprotected |
Referenced by Native.rcfNumToDecimalString().
|
staticprotected |
Referenced by Native.rcfNumToString().
|
staticprotected |
Referenced by Native.rcfPower().
|
staticprotected |
Referenced by Native.rcfSub().
|
staticprotected |
Referenced by Native.resetMemory().
|
staticprotected |
Referenced by Native.setAstPrintMode().
|
staticprotected |
Referenced by Native.setError().
|
staticprotected |
Referenced by Native.setParamValue().
|
staticprotected |
Referenced by Native.simplify().
|
staticprotected |
Referenced by Native.simplifyEx().
|
staticprotected |
Referenced by Native.simplifyGetHelp().
|
staticprotected |
Referenced by Native.simplifyGetParamDescrs().
|
staticprotected |
Referenced by Native.solverAssert().
|
staticprotected |
Referenced by Native.solverAssertAndTrack().
|
staticprotected |
Referenced by Native.solverCheck().
|
staticprotected |
Referenced by Native.solverCheckAssumptions().
|
staticprotected |
Referenced by Native.solverCube().
|
staticprotected |
Referenced by Native.solverDecRef().
|
staticprotected |
Referenced by Native.solverFromFile().
|
staticprotected |
Referenced by Native.solverFromString().
|
staticprotected |
Referenced by Native.solverGetAssertions().
|
staticprotected |
Referenced by Native.solverGetConsequences().
|
staticprotected |
Referenced by Native.solverGetHelp().
|
staticprotected |
Referenced by Native.solverGetLevels().
|
staticprotected |
Referenced by Native.solverGetModel().
|
staticprotected |
Referenced by Native.solverGetNonUnits().
|
staticprotected |
Referenced by Native.solverGetNumScopes().
|
staticprotected |
Referenced by Native.solverGetParamDescrs().
|
staticprotected |
Referenced by Native.solverGetProof().
|
staticprotected |
Referenced by Native.solverGetReasonUnknown().
|
staticprotected |
Referenced by Native.solverGetStatistics().
|
staticprotected |
Referenced by Native.solverGetTrail().
|
staticprotected |
Referenced by Native.solverGetUnits().
|
staticprotected |
Referenced by Native.solverGetUnsatCore().
|
staticprotected |
Referenced by Native.solverImportModelConverter().
|
staticprotected |
Referenced by Native.solverIncRef().
|
staticprotected |
Referenced by Native.solverInterrupt().
|
staticprotected |
Referenced by Native.solverPop().
|
staticprotected |
Referenced by Native.solverPush().
|
staticprotected |
Referenced by Native.solverReset().
|
staticprotected |
Referenced by Native.solverSetParams().
|
staticprotected |
Referenced by Native.solverToDimacsString().
|
staticprotected |
Referenced by Native.solverToString().
|
staticprotected |
Referenced by Native.solverTranslate().
|
staticprotected |
Referenced by Native.sortToAst().
|
staticprotected |
Referenced by Native.sortToString().
|
staticprotected |
Referenced by Native.statsDecRef().
|
staticprotected |
Referenced by Native.statsGetDoubleValue().
|
staticprotected |
Referenced by Native.statsGetKey().
|
staticprotected |
Referenced by Native.statsGetUintValue().
|
staticprotected |
Referenced by Native.statsIncRef().
|
staticprotected |
Referenced by Native.statsIsDouble().
|
staticprotected |
Referenced by Native.statsIsUint().
|
staticprotected |
Referenced by Native.statsSize().
|
staticprotected |
Referenced by Native.statsToString().
|
staticprotected |
Referenced by Native.substitute().
|
staticprotected |
Referenced by Native.substituteVars().
|
staticprotected |
Referenced by Native.tacticAndThen().
|
staticprotected |
Referenced by Native.tacticApply().
|
staticprotected |
Referenced by Native.tacticApplyEx().
|
staticprotected |
Referenced by Native.tacticCond().
|
staticprotected |
Referenced by Native.tacticDecRef().
|
staticprotected |
Referenced by Native.tacticFail().
|
staticprotected |
Referenced by Native.tacticFailIf().
|
staticprotected |
Referenced by Native.tacticFailIfNotDecided().
|
staticprotected |
Referenced by Native.tacticGetDescr().
|
staticprotected |
Referenced by Native.tacticGetHelp().
|
staticprotected |
Referenced by Native.tacticGetParamDescrs().
|
staticprotected |
Referenced by Native.tacticIncRef().
|
staticprotected |
Referenced by Native.tacticOrElse().
|
staticprotected |
Referenced by Native.tacticParAndThen().
|
staticprotected |
Referenced by Native.tacticParOr().
|
staticprotected |
Referenced by Native.tacticRepeat().
|
staticprotected |
Referenced by Native.tacticSkip().
|
staticprotected |
Referenced by Native.tacticTryFor().
|
staticprotected |
Referenced by Native.tacticUsingParams().
|
staticprotected |
Referenced by Native.tacticWhen().
|
staticprotected |
Referenced by Native.toApp().
|
staticprotected |
Referenced by Native.toFuncDecl().
|
staticprotected |
Referenced by Native.toggleWarningMessages().
|
staticprotected |
Referenced by Native.translate().
|
staticprotected |
Referenced by Native.updateParamValue().
|
staticprotected |
Referenced by Native.updateTerm().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3134 of file Native.java.
Referenced by Expr.isArray(), Expr.isFiniteDomain(), and Expr.isRelation().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3350 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2126 of file Native.java.
|
inlinestatic |
Definition at line 2099 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 2153 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 1110 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 997 of file Native.java.
|
inlinestatic |
Definition at line 1006 of file Native.java.
|
inlinestatic |
Definition at line 1901 of file Native.java.
|
inlinestatic |
Definition at line 4984 of file Native.java.
|
inlinestatic |
Definition at line 4899 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2081 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 721 of file Native.java.
Referenced by Context.Context().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 1042 of file Native.java.
|
inlinestatic |
Definition at line 1068 of file Native.java.
|
inlinestatic |
Definition at line 737 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 1059 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 1370 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 1024 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 2549 of file Native.java.
|
inlinestatic |
Definition at line 2585 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 988 of file Native.java.
|
inlinestatic |
Definition at line 5463 of file Native.java.
|
inlinestatic |
Definition at line 2540 of file Native.java.
|
inlinestatic |
Definition at line 2576 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 1128 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 1101 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 3955 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2045 of file Native.java.
Referenced by Context.mkInt(), Context.mkNumeral(), and Context.mkReal().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2063 of file Native.java.
Referenced by Context.mkInt(), Context.mkNumeral(), and Context.mkReal().
|
inlinestatic |
Definition at line 961 of file Native.java.
|
inlinestatic |
Definition at line 925 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2477 of file Native.java.
|
inlinestatic |
Definition at line 1033 of file Native.java.
|
inlinestatic |
Definition at line 2171 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3512 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2027 of file Native.java.
Referenced by Context.mkInt(), Context.mkNumeral(), and Context.mkReal().
|
inlinestatic |
Definition at line 5678 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 790 of file Native.java.
|
inlinestatic |
Definition at line 2486 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2495 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4129 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 970 of file Native.java.
|
inlinestatic |
Definition at line 1146 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2333 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 2306 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 1910 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 1919 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 934 of file Native.java.
|
inlinestatic |
Definition at line 2270 of file Native.java.
|
inlinestatic |
Definition at line 2261 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4104 of file Native.java.
|
inlinestatic |
Definition at line 2513 of file Native.java.
|
inlinestatic |
Definition at line 2504 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 1015 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 943 of file Native.java.
|
inlinestatic |
Definition at line 2054 of file Native.java.
|
inlinestatic |
Definition at line 2072 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3529 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 6703 of file Native.java.
|
inlinestatic |
Definition at line 3582 of file Native.java.
Referenced by Model.getConstDecls(), and Model.getDecls().
|
inlinestatic |
Definition at line 3546 of file Native.java.
Referenced by Model.getConstInterp(), and Model.getFuncInterp().
|
inlinestatic |
Definition at line 3600 of file Native.java.
Referenced by Model.getDecls(), and Model.getFuncDecls().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3555 of file Native.java.
|
inlinestatic |
Definition at line 3521 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 3636 of file Native.java.
|
inlinestatic |
Definition at line 3791 of file Native.java.
Referenced by Log.open().
|
inlinestatic |
|
inlinestatic |
Definition at line 5711 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 5695 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 5815 of file Native.java.
|
inlinestatic |
Definition at line 5833 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 5824 of file Native.java.
|
inlinestatic |
Definition at line 5842 of file Native.java.
|
inlinestatic |
Definition at line 5687 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 872 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 864 of file Native.java.
|
inlinestatic |
Definition at line 889 of file Native.java.
Referenced by ParamDescrs.getNames(), and ParamDescrs.size().
|
inlinestatic |
|
inlinestatic |
Definition at line 807 of file Native.java.
|
inlinestatic |
Definition at line 799 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3296 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 5249 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4146 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4138 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 6712 of file Native.java.
|
inlinestatic |
Definition at line 6685 of file Native.java.
|
inlinestatic |
Definition at line 6694 of file Native.java.
|
inlinestatic |
Definition at line 1093 of file Native.java.
Referenced by Constructor.ConstructorDecl(), Constructor.getAccessorDecls(), and Constructor.getTesterDecl().
|
inlinestatic |
Definition at line 5320 of file Native.java.
|
inlinestatic |
Definition at line 5258 of file Native.java.
|
inlinestatic |
Definition at line 5347 of file Native.java.
|
inlinestatic |
Definition at line 5419 of file Native.java.
|
inlinestatic |
Definition at line 5410 of file Native.java.
|
inlinestatic |
Definition at line 5455 of file Native.java.
|
inlinestatic |
Definition at line 5392 of file Native.java.
|
inlinestatic |
Definition at line 5365 of file Native.java.
|
inlinestatic |
Definition at line 5401 of file Native.java.
|
inlinestatic |
Definition at line 5383 of file Native.java.
|
inlinestatic |
Definition at line 5293 of file Native.java.
|
inlinestatic |
Definition at line 5302 of file Native.java.
|
inlinestatic |
Definition at line 5284 of file Native.java.
|
inlinestatic |
Definition at line 5266 of file Native.java.
|
inlinestatic |
Definition at line 5311 of file Native.java.
|
inlinestatic |
Definition at line 5275 of file Native.java.
|
inlinestatic |
Definition at line 5338 of file Native.java.
|
inlinestatic |
Definition at line 5356 of file Native.java.
|
inlinestatic |
Definition at line 5428 of file Native.java.
|
inlinestatic |
Definition at line 5446 of file Native.java.
|
inlinestatic |
Definition at line 5437 of file Native.java.
|
inlinestatic |
Definition at line 5374 of file Native.java.
|
inlinestatic |
Definition at line 5329 of file Native.java.
|
inlinestatic |
Definition at line 3945 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 3907 of file Native.java.
|
static |
|
inlinestatic |
Definition at line 732 of file Native.java.
Referenced by Context.Context().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3467 of file Native.java.
Referenced by Context.getSimplifyParameterDescriptions().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4742 of file Native.java.
|
inlinestatic |
Definition at line 4581 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4662 of file Native.java.
Referenced by Solver.getAssertions(), and Solver.getNumAssertions().
|
inlinestatic |
Definition at line 4733 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4698 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4689 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4680 of file Native.java.
|
inlinestatic |
Definition at line 4671 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4539 of file Native.java.
|
inlinestatic |
Definition at line 4573 of file Native.java.
|
inlinestatic |
Definition at line 4589 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4805 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2675 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4831 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4848 of file Native.java.
Referenced by Statistics.getEntries(), and Statistics.getKeys().
|
inlinestatic |
|
inlinestatic |
Definition at line 4823 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4121 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4113 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3161 of file Native.java.
|
inlinestatic |
Definition at line 3170 of file Native.java.
|
inlinestatic |
Definition at line 3807 of file Native.java.
Referenced by Global.ToggleWarningMessages().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |