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 | 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 | 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 | 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 | mkReSort (long a0, long a1) throws Z3Exception |
static boolean | isReSort (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 boolean | isString (long a0, long a1) throws Z3Exception |
static String | getString (long a0, long a1) 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 | 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 | mkSeqLength (long a0, long a1) throws Z3Exception |
static long | mkSeqIndex (long a0, long a1, long a2, long a3) 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 | 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 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 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 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 String | getParserError (long a0) 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 String | goalToString (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 | applyResultConvertModel (long a0, long a1, int a2, long a3) 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 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 | 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 long | solverGetAssertions (long a0, long a1) 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 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 | 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 | 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 void | fixedpointPush (long a0, long a1) throws Z3Exception |
static void | fixedpointPop (long a0, long a1) 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 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) throws Z3Exception |
static String | optimizeGetReasonUnknown (long a0, long a1) throws Z3Exception |
static long | optimizeGetModel (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 | mkInterpolant (long a0, long a1) throws Z3Exception |
static long | mkInterpolationContext (long a0) throws Z3Exception |
static long | getInterpolant (long a0, long a1, long a2, long a3) throws Z3Exception |
static int | computeInterpolant (long a0, long a1, long a2, LongPtr a3, LongPtr a4) throws Z3Exception |
static String | interpolationProfile (long a0) throws Z3Exception |
static int | readInterpolationProblem (long a0, IntPtr a1, ObjArrayPtr a2, UIntArrayPtr a3, String a4, StringPtr a5, IntPtr a6, ObjArrayPtr a7) throws Z3Exception |
static int | checkInterpolant (long a0, int a1, long[] a2, int[] a3, long[] a4, StringPtr a5, int a6, long[] a7) throws Z3Exception |
static void | writeInterpolationProblem (long a0, int a1, long[] a2, int[] a3, String a4, int a5, long[] a6) 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 | 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 | 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 | 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 | INTERNALmkReSort (long a0, long a1) |
static native boolean | INTERNALisReSort (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 boolean | INTERNALisString (long a0, long a1) |
static native String | INTERNALgetString (long a0, long a1) |
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 | 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 | INTERNALmkSeqLength (long a0, long a1) |
static native long | INTERNALmkSeqIndex (long a0, long a1, long a2, long a3) |
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 | 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 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 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 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 String | INTERNALgetParserError (long a0) |
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 String | INTERNALgoalToString (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 | INTERNALapplyResultConvertModel (long a0, long a1, int a2, long a3) |
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 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 | 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 long | INTERNALsolverGetAssertions (long a0, long a1) |
static native void | INTERNALsolverFromFile (long a0, long a1, String a2) |
static native void | INTERNALsolverFromString (long a0, long a1, String a2) |
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 | 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 | 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 void | INTERNALfixedpointPush (long a0, long a1) |
static native void | INTERNALfixedpointPop (long a0, long a1) |
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 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) |
static native String | INTERNALoptimizeGetReasonUnknown (long a0, long a1) |
static native long | INTERNALoptimizeGetModel (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 | INTERNALmkInterpolant (long a0, long a1) |
static native long | INTERNALmkInterpolationContext (long a0) |
static native long | INTERNALgetInterpolant (long a0, long a1, long a2, long a3) |
static native int | INTERNALcomputeInterpolant (long a0, long a1, long a2, LongPtr a3, LongPtr a4) |
static native String | INTERNALinterpolationProfile (long a0) |
static native int | INTERNALreadInterpolationProblem (long a0, IntPtr a1, ObjArrayPtr a2, UIntArrayPtr a3, String a4, StringPtr a5, IntPtr a6, ObjArrayPtr a7) |
static native int | INTERNALcheckInterpolant (long a0, int a1, long[] a2, int[] a3, long[] a4, StringPtr a5, int a6, long[] a7) |
static native void | INTERNALwriteInterpolationProblem (long a0, int a1, long[] a2, int[] a3, String a4, int a5, long[] a6) |
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 3453 of file Native.java.
|
inlinestatic |
Definition at line 3444 of file Native.java.
|
inlinestatic |
Definition at line 4835 of file Native.java.
|
inlinestatic |
Definition at line 4862 of file Native.java.
|
inlinestatic |
Definition at line 4925 of file Native.java.
|
inlinestatic |
Definition at line 4952 of file Native.java.
|
inlinestatic |
Definition at line 4916 of file Native.java.
|
inlinestatic |
Definition at line 4898 of file Native.java.
|
inlinestatic |
Definition at line 4808 of file Native.java.
|
inlinestatic |
Definition at line 4799 of file Native.java.
|
inlinestatic |
Definition at line 4790 of file Native.java.
|
inlinestatic |
Definition at line 4817 of file Native.java.
|
inlinestatic |
Definition at line 4907 of file Native.java.
|
inlinestatic |
Definition at line 4889 of file Native.java.
|
inlinestatic |
Definition at line 4853 of file Native.java.
|
inlinestatic |
Definition at line 4934 of file Native.java.
|
inlinestatic |
Definition at line 4880 of file Native.java.
|
inlinestatic |
Definition at line 4871 of file Native.java.
|
inlinestatic |
Definition at line 4943 of file Native.java.
|
inlinestatic |
Definition at line 4826 of file Native.java.
|
inlinestatic |
Definition at line 4844 of file Native.java.
|
inlinestatic |
Definition at line 3578 of file Native.java.
Referenced by Log.append().
|
inlinestatic |
Definition at line 4266 of file Native.java.
Referenced by ApplyResult.convertModel().
|
inlinestatic |
Definition at line 4231 of file Native.java.
|
inlinestatic |
Definition at line 4248 of file Native.java.
Referenced by ApplyResult.getNumSubgoals().
|
inlinestatic |
Definition at line 4257 of file Native.java.
Referenced by ApplyResult.getSubgoals().
|
inlinestatic |
Definition at line 4223 of file Native.java.
|
inlinestatic |
Definition at line 4239 of file Native.java.
Referenced by ApplyResult.toString().
|
inlinestatic |
Definition at line 2843 of file Native.java.
|
inlinestatic |
Definition at line 4721 of file Native.java.
|
inlinestatic |
Definition at line 4713 of file Native.java.
|
inlinestatic |
Definition at line 4747 of file Native.java.
|
inlinestatic |
Definition at line 4730 of file Native.java.
|
inlinestatic |
Definition at line 4705 of file Native.java.
|
inlinestatic |
Definition at line 4739 of file Native.java.
|
inlinestatic |
Definition at line 4772 of file Native.java.
|
inlinestatic |
Definition at line 4755 of file Native.java.
|
inlinestatic |
Definition at line 4763 of file Native.java.
|
inlinestatic |
Definition at line 4781 of file Native.java.
|
inlinestatic |
Definition at line 3601 of file Native.java.
Referenced by AST.getSExpr(), and AST.toString().
|
inlinestatic |
Definition at line 4628 of file Native.java.
|
inlinestatic |
Definition at line 4645 of file Native.java.
Referenced by ASTVector.get().
|
inlinestatic |
Definition at line 4620 of file Native.java.
|
inlinestatic |
Definition at line 4670 of file Native.java.
Referenced by ASTVector.push().
|
inlinestatic |
Definition at line 4662 of file Native.java.
Referenced by ASTVector.resize().
|
inlinestatic |
Definition at line 4654 of file Native.java.
Referenced by ASTVector.set().
|
inlinestatic |
Definition at line 4636 of file Native.java.
Referenced by ASTVector.size().
|
inlinestatic |
Definition at line 4687 of file Native.java.
Referenced by ASTVector.toString().
|
inlinestatic |
Definition at line 4678 of file Native.java.
Referenced by ASTVector.translate().
|
inlinestatic |
Definition at line 3646 of file Native.java.
Referenced by Context.benchmarkToSMTString().
|
inlinestatic |
Definition at line 5676 of file Native.java.
Referenced by InterpolationContext.CheckInterpolant().
|
inlinestatic |
Definition at line 3583 of file Native.java.
Referenced by Log.close().
|
inlinestatic |
Definition at line 5649 of file Native.java.
Referenced by InterpolationContext.ComputeInterpolant().
|
inlinestatic |
Definition at line 2609 of file Native.java.
Referenced by Context.mkUpdateField().
|
inlinestatic |
Definition at line 744 of file Native.java.
|
inlinestatic |
Definition at line 705 of file Native.java.
Referenced by Context.Context(), and InterpolationContext.mkContext().
|
inlinestatic |
Definition at line 1029 of file Native.java.
Referenced by ConstructorDecRefQueue.decRef().
|
inlinestatic |
Definition at line 1055 of file Native.java.
Referenced by ConstructorListDecRefQueue.decRef().
|
inlinestatic |
Definition at line 731 of file Native.java.
Referenced by Context.close().
|
inlinestatic |
Definition at line 3730 of file Native.java.
Referenced by Global.disableTrace().
|
inlinestatic |
Definition at line 3725 of file Native.java.
Referenced by Global.enableTrace().
|
inlinestatic |
Definition at line 3673 of file Native.java.
|
inlinestatic |
Definition at line 3740 of file Native.java.
|
inlinestatic |
Definition at line 5286 of file Native.java.
Referenced by Fixedpoint.addCover().
|
inlinestatic |
Definition at line 5208 of file Native.java.
Referenced by Fixedpoint.addFact().
|
inlinestatic |
Definition at line 6449 of file Native.java.
|
inlinestatic |
Definition at line 5200 of file Native.java.
Referenced by Fixedpoint.addRule().
|
inlinestatic |
Definition at line 5216 of file Native.java.
Referenced by Fixedpoint.add().
|
inlinestatic |
Definition at line 5192 of file Native.java.
|
inlinestatic |
Definition at line 5381 of file Native.java.
Referenced by Fixedpoint.ParseFile().
|
inlinestatic |
Definition at line 5372 of file Native.java.
Referenced by Fixedpoint.ParseString().
|
inlinestatic |
Definition at line 5242 of file Native.java.
Referenced by Fixedpoint.getAnswer().
|
inlinestatic |
Definition at line 5328 of file Native.java.
Referenced by Fixedpoint.getAssertions().
|
inlinestatic |
Definition at line 5277 of file Native.java.
Referenced by Fixedpoint.getCoverDelta().
|
inlinestatic |
Definition at line 6422 of file Native.java.
|
inlinestatic |
Definition at line 5345 of file Native.java.
Referenced by Fixedpoint.getHelp().
|
inlinestatic |
Definition at line 5268 of file Native.java.
Referenced by Fixedpoint.getNumLevels().
|
inlinestatic |
Definition at line 5354 of file Native.java.
Referenced by Fixedpoint.getParameterDescriptions().
|
inlinestatic |
Definition at line 6457 of file Native.java.
|
inlinestatic |
Definition at line 5251 of file Native.java.
Referenced by Fixedpoint.getReasonUnknown().
|
inlinestatic |
Definition at line 6440 of file Native.java.
|
inlinestatic |
Definition at line 5319 of file Native.java.
Referenced by Fixedpoint.getRules().
|
inlinestatic |
Definition at line 6431 of file Native.java.
|
inlinestatic |
Definition at line 5294 of file Native.java.
Referenced by Fixedpoint.getStatistics().
|
inlinestatic |
Definition at line 5184 of file Native.java.
|
inlinestatic |
Definition at line 5398 of file Native.java.
Referenced by Fixedpoint.pop().
|
inlinestatic |
Definition at line 5390 of file Native.java.
Referenced by Fixedpoint.push().
|
inlinestatic |
Definition at line 5224 of file Native.java.
Referenced by Fixedpoint.query().
|
inlinestatic |
Definition at line 6413 of file Native.java.
|
inlinestatic |
Definition at line 5233 of file Native.java.
Referenced by Fixedpoint.query().
|
inlinestatic |
Definition at line 5303 of file Native.java.
Referenced by Fixedpoint.registerRelation().
|
inlinestatic |
Definition at line 5337 of file Native.java.
Referenced by Fixedpoint.setParameters().
|
inlinestatic |
Definition at line 5311 of file Native.java.
Referenced by Fixedpoint.setPredicateRepresentation().
|
inlinestatic |
Definition at line 5363 of file Native.java.
Referenced by Fixedpoint.toString().
|
inlinestatic |
Definition at line 5260 of file Native.java.
Referenced by Fixedpoint.updateRule().
|
inlinestatic |
Definition at line 6242 of file Native.java.
Referenced by FPSort.getEBits().
|
inlinestatic |
Definition at line 6386 of file Native.java.
Referenced by FPNum.getExponentBV().
|
inlinestatic |
Definition at line 6377 of file Native.java.
Referenced by FPNum.getExponentInt64().
|
inlinestatic |
Definition at line 6368 of file Native.java.
Referenced by FPNum.getExponent().
|
inlinestatic |
Definition at line 6341 of file Native.java.
Referenced by FPNum.getSign().
|
inlinestatic |
Definition at line 6323 of file Native.java.
Referenced by FPNum.getSignBV().
|
inlinestatic |
Definition at line 6332 of file Native.java.
Referenced by FPNum.getSignificandBV().
|
inlinestatic |
Definition at line 6350 of file Native.java.
Referenced by FPNum.getSignificand().
|
inlinestatic |
Definition at line 6359 of file Native.java.
Referenced by FPNum.getSignificandUInt64().
|
inlinestatic |
Definition at line 6251 of file Native.java.
Referenced by FPSort.getSBits().
|
inlinestatic |
Definition at line 6269 of file Native.java.
Referenced by FPNum.isInf().
|
inlinestatic |
Definition at line 6260 of file Native.java.
Referenced by FPNum.isNaN().
|
inlinestatic |
Definition at line 6314 of file Native.java.
Referenced by FPNum.isNegative().
|
inlinestatic |
Definition at line 6287 of file Native.java.
Referenced by FPNum.isNormal().
|
inlinestatic |
Definition at line 6305 of file Native.java.
Referenced by FPNum.isPositive().
|
inlinestatic |
Definition at line 6296 of file Native.java.
Referenced by FPNum.isSubnormal().
|
inlinestatic |
Definition at line 6278 of file Native.java.
Referenced by FPNum.isZero().
|
inlinestatic |
Definition at line 2681 of file Native.java.
|
inlinestatic |
Definition at line 3628 of file Native.java.
Referenced by FuncDecl.toString().
|
inlinestatic |
Definition at line 3537 of file Native.java.
|
inlinestatic |
Definition at line 3563 of file Native.java.
|
inlinestatic |
Definition at line 3554 of file Native.java.
|
inlinestatic |
Definition at line 3545 of file Native.java.
|
inlinestatic |
Definition at line 3529 of file Native.java.
|
inlinestatic |
Definition at line 3521 of file Native.java.
|
inlinestatic |
Definition at line 3469 of file Native.java.
|
inlinestatic |
Definition at line 3512 of file Native.java.
Referenced by FuncInterp.getArity().
|
inlinestatic |
Definition at line 3495 of file Native.java.
Referenced by FuncInterp.getElse().
|
inlinestatic |
Definition at line 3486 of file Native.java.
Referenced by FuncInterp.getEntries().
|
inlinestatic |
Definition at line 3477 of file Native.java.
Referenced by FuncInterp.getNumEntries().
|
inlinestatic |
Definition at line 3461 of file Native.java.
|
inlinestatic |
Definition at line 3504 of file Native.java.
|
inlinestatic |
Definition at line 3077 of file Native.java.
Referenced by AlgebraicNum.toLower().
|
inlinestatic |
Definition at line 3086 of file Native.java.
Referenced by AlgebraicNum.toUpper().
|
inlinestatic |
Definition at line 2870 of file Native.java.
Referenced by Expr.getArgs().
|
inlinestatic |
Definition at line 2852 of file Native.java.
Referenced by Expr.getFuncDecl().
|
inlinestatic |
Definition at line 2861 of file Native.java.
Referenced by Expr.getNumArgs().
|
inlinestatic |
Definition at line 2735 of file Native.java.
Referenced by FuncDecl.getArity().
|
inlinestatic |
Definition at line 2528 of file Native.java.
Referenced by ArraySort.getDomain().
|
inlinestatic |
Definition at line 2537 of file Native.java.
Referenced by ArraySort.getRange().
|
inlinestatic |
Definition at line 3435 of file Native.java.
Referenced by Model.getFuncInterp().
|
inlinestatic |
Definition at line 2897 of file Native.java.
Referenced by AST.hashCode().
|
inlinestatic |
Definition at line 2888 of file Native.java.
Referenced by AST.getId().
|
inlinestatic |
Definition at line 2933 of file Native.java.
Referenced by AST.getASTKind().
|
inlinestatic |
Definition at line 2924 of file Native.java.
Referenced by Expr.getBoolValue().
|
inlinestatic |
Definition at line 2510 of file Native.java.
Referenced by BitVecSort.getSize().
|
inlinestatic |
Definition at line 2582 of file Native.java.
Referenced by DatatypeSort.getAccessors(), ListSort.getConsDecl(), EnumSort.getConstDecl(), EnumSort.getConstDecls(), DatatypeSort.getConstructors(), and ListSort.getNilDecl().
|
inlinestatic |
Definition at line 2600 of file Native.java.
Referenced by DatatypeSort.getAccessors(), ListSort.getHeadDecl(), and ListSort.getTailDecl().
|
inlinestatic |
Definition at line 2573 of file Native.java.
Referenced by EnumSort.getConstDecls(), DatatypeSort.getNumConstructors(), and EnumSort.getTesterDecls().
|
inlinestatic |
Definition at line 2591 of file Native.java.
Referenced by ListSort.getIsConsDecl(), ListSort.getIsNilDecl(), DatatypeSort.getRecognizers(), EnumSort.getTesterDecl(), and EnumSort.getTesterDecls().
|
inlinestatic |
Definition at line 2816 of file Native.java.
Referenced by FuncDecl.getParameters().
|
inlinestatic |
Definition at line 2789 of file Native.java.
Referenced by FuncDecl.getParameters().
|
inlinestatic |
Definition at line 2825 of file Native.java.
Referenced by FuncDecl.getParameters().
|
inlinestatic |
Definition at line 2780 of file Native.java.
Referenced by FuncDecl.getParameters().
|
inlinestatic |
Definition at line 2717 of file Native.java.
Referenced by FuncDecl.getDeclKind().
|
inlinestatic |
Definition at line 2708 of file Native.java.
Referenced by FuncDecl.getName().
|
inlinestatic |
Definition at line 2762 of file Native.java.
Referenced by FuncDecl.getNumParameters().
|
inlinestatic |
Definition at line 2771 of file Native.java.
|
inlinestatic |
Definition at line 2834 of file Native.java.
Referenced by FuncDecl.getParameters().
|
inlinestatic |
Definition at line 2807 of file Native.java.
|
inlinestatic |
Definition at line 2798 of file Native.java.
|
inlinestatic |
Definition at line 3014 of file Native.java.
Referenced by RatNum.getDenominator().
|
inlinestatic |
Definition at line 2744 of file Native.java.
Referenced by FuncDecl.getDomain().
|
inlinestatic |
Definition at line 2726 of file Native.java.
Referenced by FuncDecl.getDomainSize().
|
inlinestatic |
Definition at line 3691 of file Native.java.
|
inlinestatic |
Definition at line 3705 of file Native.java.
|
inlinestatic |
Definition at line 4605 of file Native.java.
|
inlinestatic |
Definition at line 2519 of file Native.java.
Referenced by FiniteDomainSort.getSize().
|
inlinestatic |
Definition at line 3719 of file Native.java.
Referenced by Version.getFullVersion().
|
inlinestatic |
Definition at line 2699 of file Native.java.
Referenced by FuncDecl.getId().
|
inlinestatic |
Definition at line 4454 of file Native.java.
|
inlinestatic |
Definition at line 3122 of file Native.java.
Referenced by Expr.getIndex().
|
inlinestatic |
Definition at line 5640 of file Native.java.
Referenced by InterpolationContext.GetInterpolant().
|
inlinestatic |
Definition at line 2996 of file Native.java.
Referenced by AlgebraicNum.toDecimal(), and RatNum.toDecimalString().
|
inlinestatic |
Definition at line 3032 of file Native.java.
Referenced by BitVecNum.getInt(), IntNum.getInt(), and FiniteDomainNum.getInt().
|
inlinestatic |
Definition at line 3059 of file Native.java.
Referenced by IntNum.getInt64(), FiniteDomainNum.getInt64(), and BitVecNum.getLong().
|
inlinestatic |
Definition at line 3068 of file Native.java.
|
inlinestatic |
Definition at line 3023 of file Native.java.
|
inlinestatic |
Definition at line 2987 of file Native.java.
Referenced by IntNum.toString(), BitVecNum.toString(), FiniteDomainNum.toString(), RatNum.toString(), and FPNum.toString().
|
inlinestatic |
Definition at line 3041 of file Native.java.
|
inlinestatic |
Definition at line 3050 of file Native.java.
|
inlinestatic |
Definition at line 3005 of file Native.java.
Referenced by RatNum.getNumerator().
|
inlinestatic |
Definition at line 4142 of file Native.java.
Referenced by Context.getNumProbes().
|
inlinestatic |
Definition at line 4124 of file Native.java.
Referenced by Context.getNumTactics().
|
inlinestatic |
Definition at line 3682 of file Native.java.
|
inlinestatic |
Definition at line 3113 of file Native.java.
Referenced by Pattern.getTerms().
|
inlinestatic |
Definition at line 3104 of file Native.java.
Referenced by Pattern.getNumTerms().
|
inlinestatic |
Definition at line 4151 of file Native.java.
Referenced by Context.getProbeNames().
|
inlinestatic |
Definition at line 3212 of file Native.java.
Referenced by Quantifier.getBody().
|
inlinestatic |
Definition at line 3194 of file Native.java.
Referenced by Quantifier.getBoundVariableNames().
|
inlinestatic |
Definition at line 3203 of file Native.java.
Referenced by Quantifier.getBoundVariableSorts().
|
inlinestatic |
Definition at line 3176 of file Native.java.
Referenced by Quantifier.getNoPatterns().
|
inlinestatic |
Definition at line 3185 of file Native.java.
Referenced by Quantifier.getNumBound().
|
inlinestatic |
Definition at line 3167 of file Native.java.
Referenced by Quantifier.getNumNoPatterns().
|
inlinestatic |
Definition at line 3149 of file Native.java.
Referenced by Quantifier.getNumPatterns().
|
inlinestatic |
Definition at line 3158 of file Native.java.
Referenced by Quantifier.getPatterns().
|
inlinestatic |
Definition at line 3140 of file Native.java.
Referenced by Quantifier.getWeight().
|
inlinestatic |
Definition at line 2753 of file Native.java.
Referenced by Model.getConstInterp(), Model.getFuncInterp(), and FuncDecl.getRange().
|
inlinestatic |
Definition at line 2618 of file Native.java.
Referenced by RelationSort.getArity().
|
inlinestatic |
Definition at line 2627 of file Native.java.
Referenced by RelationSort.getColumnSorts().
|
inlinestatic |
Definition at line 2906 of file Native.java.
Referenced by Expr.getSort(), Expr.isArray(), Expr.isBool(), Expr.isBV(), Expr.isFiniteDomain(), Expr.isInt(), Expr.isReal(), and Expr.isRelation().
|
inlinestatic |
Definition at line 2474 of file Native.java.
Referenced by Sort.getId().
|
inlinestatic |
Definition at line 2501 of file Native.java.
Referenced by Model.getConstInterp(), Model.getFuncInterp(), Sort.getSortKind(), Expr.isArray(), Expr.isBV(), Expr.isFiniteDomain(), Expr.isInt(), Expr.isReal(), and Expr.isRelation().
|
inlinestatic |
Definition at line 2465 of file Native.java.
Referenced by Sort.getName().
|
inlinestatic |
Definition at line 2105 of file Native.java.
Referenced by Expr.getString().
|
inlinestatic |
Definition at line 2447 of file Native.java.
Referenced by IntSymbol.getInt().
|
inlinestatic |
Definition at line 2438 of file Native.java.
Referenced by Symbol.getKind().
|
inlinestatic |
Definition at line 2456 of file Native.java.
Referenced by StringSymbol.getString().
|
inlinestatic |
Definition at line 4133 of file Native.java.
Referenced by Context.getTacticNames().
|
inlinestatic |
Definition at line 2564 of file Native.java.
Referenced by TupleSort.getFieldDecls().
|
inlinestatic |
Definition at line 2546 of file Native.java.
Referenced by TupleSort.mkDecl().
|
inlinestatic |
Definition at line 2555 of file Native.java.
Referenced by TupleSort.getNumFields().
|
inlinestatic |
Definition at line 3714 of file Native.java.
Referenced by Version.getBuild(), Version.getMajor(), Version.getMinor(), Version.getRevision(), and Version.getString().
|
inlinestatic |
Definition at line 693 of file Native.java.
Referenced by Global.getParameter().
|
inlinestatic |
Definition at line 688 of file Native.java.
Referenced by Global.resetParameters().
|
inlinestatic |
Definition at line 683 of file Native.java.
Referenced by Global.setParameter().
|
inlinestatic |
Definition at line 3779 of file Native.java.
Referenced by Goal.add().
|
inlinestatic |
Definition at line 3762 of file Native.java.
|
inlinestatic |
Definition at line 3796 of file Native.java.
Referenced by Goal.getDepth().
|
inlinestatic |
Definition at line 3822 of file Native.java.
Referenced by Goal.getFormulas().
|
inlinestatic |
Definition at line 3787 of file Native.java.
Referenced by Goal.inconsistent().
|
inlinestatic |
Definition at line 3754 of file Native.java.
|
inlinestatic |
Definition at line 3840 of file Native.java.
Referenced by Goal.isDecidedSat().
|
inlinestatic |
Definition at line 3849 of file Native.java.
Referenced by Goal.isDecidedUnsat().
|
inlinestatic |
Definition at line 3831 of file Native.java.
Referenced by Goal.getNumExprs().
|
inlinestatic |
Definition at line 3770 of file Native.java.
Referenced by Goal.getPrecision().
|
inlinestatic |
Definition at line 3805 of file Native.java.
Referenced by Goal.reset().
|
inlinestatic |
Definition at line 3813 of file Native.java.
Referenced by Goal.size().
|
inlinestatic |
Definition at line 3867 of file Native.java.
Referenced by Goal.toString().
|
inlinestatic |
Definition at line 3858 of file Native.java.
Referenced by Goal.translate().
|
inlinestatic |
Definition at line 736 of file Native.java.
|
staticprotected |
Referenced by Native.addConstInterp().
|
staticprotected |
Referenced by Native.addFuncInterp().
|
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.applyResultConvertModel().
|
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.checkInterpolant().
|
staticprotected |
Referenced by Native.closeLog().
|
staticprotected |
Referenced by Native.computeInterpolant().
|
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.fixedpointPop().
|
staticprotected |
Referenced by Native.fixedpointPush().
|
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.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.applyResultConvertModel(), 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.checkInterpolant(), Native.computeInterpolant(), 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.fixedpointPop(), Native.fixedpointPush(), 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.getInterpolant(), Native.getNumeralDecimalString(), Native.getNumeralInt(), Native.getNumeralInt64(), Native.getNumeralRationalInt64(), Native.getNumeralSmall(), Native.getNumeralString(), Native.getNumeralUint(), Native.getNumeralUint64(), Native.getNumerator(), Native.getNumProbes(), Native.getNumTactics(), Native.getParserError(), 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.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.goalDecRef(), Native.goalDepth(), Native.goalFormula(), Native.goalInconsistent(), Native.goalIncRef(), Native.goalIsDecidedSat(), Native.goalIsDecidedUnsat(), Native.goalNumExprs(), Native.goalPrecision(), Native.goalReset(), Native.goalSize(), Native.goalToString(), Native.goalTranslate(), Native.incRef(), Native.interpolationProfile(), Native.interrupt(), Native.isAlgebraicNumber(), Native.isApp(), Native.isAsArray(), Native.isEqAst(), Native.isEqFuncDecl(), Native.isEqSort(), Native.isNumeralAst(), 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.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.mkInterpolant(), Native.mkIntSort(), Native.mkIntSymbol(), Native.mkIntToStr(), Native.mkIsInt(), Native.mkIte(), Native.mkLe(), Native.mkListSort(), Native.mkLt(), Native.mkMap(), Native.mkMod(), Native.mkModel(), Native.mkMul(), Native.mkNot(), Native.mkNumeral(), Native.mkOptimize(), Native.mkOr(), Native.mkParams(), Native.mkPattern(), Native.mkPbeq(), Native.mkPbge(), Native.mkPble(), Native.mkPower(), Native.mkProbe(), Native.mkQuantifier(), Native.mkQuantifierConst(), Native.mkQuantifierConstEx(), Native.mkQuantifierEx(), Native.mkReal(), Native.mkReal2int(), Native.mkRealSort(), 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.mkSeqLength(), Native.mkSeqPrefix(), Native.mkSeqReplace(), Native.mkSeqSort(), Native.mkSeqSuffix(), Native.mkSeqToRe(), Native.mkSeqUnit(), Native.mkSetAdd(), Native.mkSetComplement(), Native.mkSetDel(), Native.mkSetDifference(), 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.mkStrToInt(), Native.mkSub(), Native.mkTactic(), 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.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.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.readInterpolationProblem(), Native.setAstPrintMode(), Native.setError(), Native.simplify(), Native.simplifyEx(), Native.simplifyGetHelp(), Native.simplifyGetParamDescrs(), Native.solverAssert(), Native.solverAssertAndTrack(), Native.solverCheck(), Native.solverCheckAssumptions(), Native.solverDecRef(), Native.solverFromFile(), Native.solverFromString(), Native.solverGetAssertions(), Native.solverGetConsequences(), Native.solverGetHelp(), Native.solverGetModel(), Native.solverGetNumScopes(), Native.solverGetParamDescrs(), Native.solverGetProof(), Native.solverGetReasonUnknown(), Native.solverGetStatistics(), Native.solverGetUnsatCore(), Native.solverIncRef(), Native.solverPop(), Native.solverPush(), Native.solverReset(), Native.solverSetParams(), 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(), Native.updateTerm(), and Native.writeInterpolationProblem().
|
staticprotected |
Referenced by Native.addConstInterp(), Native.addFuncInterp(), 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.applyResultConvertModel(), 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.checkInterpolant(), Native.computeInterpolant(), 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.fixedpointPop(), Native.fixedpointPush(), 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.getInterpolant(), Native.getNumeralDecimalString(), Native.getNumeralInt(), Native.getNumeralInt64(), Native.getNumeralRationalInt64(), Native.getNumeralSmall(), Native.getNumeralString(), Native.getNumeralUint(), Native.getNumeralUint64(), Native.getNumerator(), Native.getNumProbes(), Native.getNumTactics(), Native.getParserError(), 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.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.goalDecRef(), Native.goalDepth(), Native.goalFormula(), Native.goalInconsistent(), Native.goalIncRef(), Native.goalIsDecidedSat(), Native.goalIsDecidedUnsat(), Native.goalNumExprs(), Native.goalPrecision(), Native.goalReset(), Native.goalSize(), Native.goalToString(), Native.goalTranslate(), Native.incRef(), Native.interpolationProfile(), Native.interrupt(), Native.isAlgebraicNumber(), Native.isApp(), Native.isAsArray(), Native.isEqAst(), Native.isEqFuncDecl(), Native.isEqSort(), Native.isNumeralAst(), 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.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.mkInterpolant(), Native.mkIntSort(), Native.mkIntSymbol(), Native.mkIntToStr(), Native.mkIsInt(), Native.mkIte(), Native.mkLe(), Native.mkListSort(), Native.mkLt(), Native.mkMap(), Native.mkMod(), Native.mkModel(), Native.mkMul(), Native.mkNot(), Native.mkNumeral(), Native.mkOptimize(), Native.mkOr(), Native.mkParams(), Native.mkPattern(), Native.mkPbeq(), Native.mkPbge(), Native.mkPble(), Native.mkPower(), Native.mkProbe(), Native.mkQuantifier(), Native.mkQuantifierConst(), Native.mkQuantifierConstEx(), Native.mkQuantifierEx(), Native.mkReal(), Native.mkReal2int(), Native.mkRealSort(), 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.mkSeqLength(), Native.mkSeqPrefix(), Native.mkSeqReplace(), Native.mkSeqSort(), Native.mkSeqSuffix(), Native.mkSeqToRe(), Native.mkSeqUnit(), Native.mkSetAdd(), Native.mkSetComplement(), Native.mkSetDel(), Native.mkSetDifference(), 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.mkStrToInt(), Native.mkSub(), Native.mkTactic(), 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.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.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.readInterpolationProblem(), Native.setAstPrintMode(), Native.setError(), Native.simplify(), Native.simplifyEx(), Native.simplifyGetHelp(), Native.simplifyGetParamDescrs(), Native.solverAssert(), Native.solverAssertAndTrack(), Native.solverCheck(), Native.solverCheckAssumptions(), Native.solverDecRef(), Native.solverFromFile(), Native.solverFromString(), Native.solverGetAssertions(), Native.solverGetConsequences(), Native.solverGetHelp(), Native.solverGetModel(), Native.solverGetNumScopes(), Native.solverGetParamDescrs(), Native.solverGetProof(), Native.solverGetReasonUnknown(), Native.solverGetStatistics(), Native.solverGetUnsatCore(), Native.solverIncRef(), Native.solverPop(), Native.solverPush(), Native.solverReset(), Native.solverSetParams(), 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(), Native.updateTerm(), and Native.writeInterpolationProblem().
|
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.getInterpolant().
|
staticprotected |
Referenced by Native.getNumeralDecimalString().
|
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.getParserError().
|
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.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.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.goalToString().
|
staticprotected |
Referenced by Native.goalTranslate().
|
staticprotected |
Referenced by Native.incRef().
|
staticprotected |
Referenced by Native.interpolationProfile().
|
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.isNumeralAst().
|
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.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.mkInterpolant().
|
staticprotected |
Referenced by Native.mkInterpolationContext().
|
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.mkLe().
|
staticprotected |
Referenced by Native.mkListSort().
|
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.mkPattern().
|
staticprotected |
Referenced by Native.mkPbeq().
|
staticprotected |
Referenced by Native.mkPbge().
|
staticprotected |
Referenced by Native.mkPble().
|
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.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.mkSeqLength().
|
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.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.mkStrToInt().
|
staticprotected |
Referenced by Native.mkSub().
|
staticprotected |
Referenced by Native.mkTactic().
|
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.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.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.readInterpolationProblem().
|
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.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.solverGetModel().
|
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.solverGetUnsatCore().
|
staticprotected |
Referenced by Native.solverIncRef().
|
staticprotected |
Referenced by Native.solverPop().
|
staticprotected |
Referenced by Native.solverPush().
|
staticprotected |
Referenced by Native.solverReset().
|
staticprotected |
Referenced by Native.solverSetParams().
|
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().
|
staticprotected |
Referenced by Native.writeInterpolationProblem().
|
inlinestatic |
Definition at line 5658 of file Native.java.
Referenced by InterpolationContext.InterpolationProfile().
|
inlinestatic |
Definition at line 760 of file Native.java.
Referenced by Context.interrupt().
|
inlinestatic |
Definition at line 2960 of file Native.java.
Referenced by Expr.isAlgebraicNumber().
|
inlinestatic |
Definition at line 2942 of file Native.java.
Referenced by Expr.isArray(), Expr.isFiniteDomain(), and Expr.isRelation().
|
inlinestatic |
Definition at line 3426 of file Native.java.
Referenced by Model.getFuncInterp().
|
inlinestatic |
Definition at line 2879 of file Native.java.
Referenced by AST.equals().
|
inlinestatic |
Definition at line 2690 of file Native.java.
Referenced by FuncDecl.equals().
|
inlinestatic |
Definition at line 2492 of file Native.java.
Referenced by Sort.equals(), and Expr.isBool().
|
inlinestatic |
Definition at line 2951 of file Native.java.
Referenced by Expr.isNumeral().
|
inlinestatic |
Definition at line 3131 of file Native.java.
Referenced by Quantifier.isUniversal().
|
inlinestatic |
Definition at line 2060 of file Native.java.
|
inlinestatic |
Definition at line 2042 of file Native.java.
|
inlinestatic |
Definition at line 2096 of file Native.java.
Referenced by Expr.isString().
|
inlinestatic |
Definition at line 2078 of file Native.java.
|
inlinestatic |
Definition at line 2915 of file Native.java.
Referenced by Expr.isWellSorted().
|
inlinestatic |
Definition at line 1223 of file Native.java.
Referenced by Context.mkAdd().
|
inlinestatic |
Definition at line 1205 of file Native.java.
Referenced by Context.mkAnd().
|
inlinestatic |
Definition at line 1088 of file Native.java.
|
inlinestatic |
Definition at line 1844 of file Native.java.
Referenced by Context.mkTermArray().
|
inlinestatic |
Definition at line 1961 of file Native.java.
Referenced by Context.mkArrayExt().
|
inlinestatic |
Definition at line 975 of file Native.java.
|
inlinestatic |
Definition at line 984 of file Native.java.
|
inlinestatic |
Definition at line 1853 of file Native.java.
|
inlinestatic |
Definition at line 4696 of file Native.java.
|
inlinestatic |
Definition at line 4611 of file Native.java.
|
inlinestatic |
Definition at line 2645 of file Native.java.
Referenced by Context.mkAtLeast().
|
inlinestatic |
Definition at line 2636 of file Native.java.
Referenced by Context.mkAtMost().
|
inlinestatic |
Definition at line 930 of file Native.java.
Referenced by Expr.isBool().
|
inlinestatic |
Definition at line 2357 of file Native.java.
Referenced by Context.mkBound().
|
inlinestatic |
Definition at line 1709 of file Native.java.
Referenced by Context.mkBV2Int().
|
inlinestatic |
Definition at line 1448 of file Native.java.
Referenced by Context.mkBVAdd().
|
inlinestatic |
Definition at line 1718 of file Native.java.
Referenced by Context.mkBVAddNoOverflow().
|
inlinestatic |
Definition at line 1727 of file Native.java.
Referenced by Context.mkBVAddNoUnderflow().
|
inlinestatic |
Definition at line 1385 of file Native.java.
Referenced by Context.mkBVAND().
|
inlinestatic |
Definition at line 1655 of file Native.java.
Referenced by Context.mkBVASHR().
|
inlinestatic |
Definition at line 1646 of file Native.java.
Referenced by Context.mkBVLSHR().
|
inlinestatic |
Definition at line 1466 of file Native.java.
Referenced by Context.mkBVMul().
|
inlinestatic |
Definition at line 1772 of file Native.java.
Referenced by Context.mkBVMulNoOverflow().
|
inlinestatic |
Definition at line 1781 of file Native.java.
Referenced by Context.mkBVMulNoUnderflow().
|
inlinestatic |
Definition at line 1412 of file Native.java.
Referenced by Context.mkBVNAND().
|
inlinestatic |
Definition at line 1439 of file Native.java.
Referenced by Context.mkBVNeg().
|
inlinestatic |
Definition at line 1763 of file Native.java.
Referenced by Context.mkBVNegNoOverflow().
|
inlinestatic |
Definition at line 1421 of file Native.java.
Referenced by Context.mkBVNOR().
|
inlinestatic |
Definition at line 1358 of file Native.java.
Referenced by Context.mkBVNot().
|
inlinestatic |
Definition at line 2024 of file Native.java.
|
inlinestatic |
Definition at line 1394 of file Native.java.
Referenced by Context.mkBVOR().
|
inlinestatic |
Definition at line 1367 of file Native.java.
Referenced by Context.mkBVRedAND().
|
inlinestatic |
Definition at line 1376 of file Native.java.
Referenced by Context.mkBVRedOR().
|
inlinestatic |
Definition at line 1484 of file Native.java.
Referenced by Context.mkBVSDiv().
|
inlinestatic |
Definition at line 1754 of file Native.java.
Referenced by Context.mkBVSDivNoOverflow().
|
inlinestatic |
Definition at line 1565 of file Native.java.
Referenced by Context.mkBVSGE().
|
inlinestatic |
Definition at line 1583 of file Native.java.
Referenced by Context.mkBVSGT().
|
inlinestatic |
Definition at line 1637 of file Native.java.
Referenced by Context.mkBVSHL().
|
inlinestatic |
Definition at line 1547 of file Native.java.
Referenced by Context.mkBVSLE().
|
inlinestatic |
Definition at line 1529 of file Native.java.
Referenced by Context.mkBVSLT().
|
inlinestatic |
Definition at line 1511 of file Native.java.
Referenced by Context.mkBVSMod().
|
inlinestatic |
Definition at line 957 of file Native.java.
Referenced by Context.mkBitVecSort().
|
inlinestatic |
Definition at line 1502 of file Native.java.
Referenced by Context.mkBVSRem().
|
inlinestatic |
Definition at line 1457 of file Native.java.
Referenced by Context.mkBVSub().
|
inlinestatic |
Definition at line 1736 of file Native.java.
Referenced by Context.mkBVSubNoOverflow().
|
inlinestatic |
Definition at line 1745 of file Native.java.
Referenced by Context.mkBVSubNoUnderflow().
|
inlinestatic |
Definition at line 1475 of file Native.java.
Referenced by Context.mkBVUDiv().
|
inlinestatic |
Definition at line 1556 of file Native.java.
Referenced by Context.mkBVUGE().
|
inlinestatic |
Definition at line 1574 of file Native.java.
Referenced by Context.mkBVUGT().
|
inlinestatic |
Definition at line 1538 of file Native.java.
Referenced by Context.mkBVULE().
|
inlinestatic |
Definition at line 1520 of file Native.java.
Referenced by Context.mkBVULT().
|
inlinestatic |
Definition at line 1493 of file Native.java.
Referenced by Context.mkBVURem().
|
inlinestatic |
Definition at line 1430 of file Native.java.
Referenced by Context.mkBVXNOR().
|
inlinestatic |
Definition at line 1403 of file Native.java.
Referenced by Context.mkBVXOR().
|
inlinestatic |
Definition at line 1592 of file Native.java.
Referenced by Context.mkConcat().
|
inlinestatic |
Definition at line 699 of file Native.java.
Referenced by Context.Context(), and InterpolationContext.mkContext().
|
inlinestatic |
Definition at line 1097 of file Native.java.
Referenced by Context.mkConst().
|
inlinestatic |
Definition at line 1826 of file Native.java.
Referenced by Context.mkConstArray().
|
inlinestatic |
Definition at line 1020 of file Native.java.
|
inlinestatic |
Definition at line 1046 of file Native.java.
|
inlinestatic |
Definition at line 715 of file Native.java.
|
inlinestatic |
Definition at line 723 of file Native.java.
Referenced by Context.Context().
|
inlinestatic |
Definition at line 1037 of file Native.java.
|
inlinestatic |
Definition at line 1063 of file Native.java.
Referenced by Context.mkDatatypeSorts().
|
inlinestatic |
Definition at line 1151 of file Native.java.
Referenced by Context.mkDistinct().
|
inlinestatic |
Definition at line 1259 of file Native.java.
Referenced by Context.mkDiv().
|
inlinestatic |
Definition at line 1871 of file Native.java.
Referenced by Context.mkEmptySet().
|
inlinestatic |
Definition at line 1002 of file Native.java.
|
inlinestatic |
Definition at line 1142 of file Native.java.
Referenced by Context.mkEq().
|
inlinestatic |
Definition at line 2375 of file Native.java.
|
inlinestatic |
Definition at line 2411 of file Native.java.
|
inlinestatic |
Definition at line 1601 of file Native.java.
Referenced by Context.mkExtract().
|
inlinestatic |
Definition at line 1682 of file Native.java.
Referenced by Context.mkBVRotateLeft().
|
inlinestatic |
Definition at line 1691 of file Native.java.
Referenced by Context.mkBVRotateRight().
|
inlinestatic |
Definition at line 1133 of file Native.java.
Referenced by Context.mkFalse().
|
inlinestatic |
Definition at line 966 of file Native.java.
|
inlinestatic |
Definition at line 5175 of file Native.java.
|
inlinestatic |
Definition at line 2366 of file Native.java.
|
inlinestatic |
Definition at line 2402 of file Native.java.
|
inlinestatic |
Definition at line 5954 of file Native.java.
Referenced by Context.mkFPAbs().
|
inlinestatic |
Definition at line 5972 of file Native.java.
Referenced by Context.mkFPAdd().
|
inlinestatic |
Definition at line 5999 of file Native.java.
Referenced by Context.mkFPDiv().
|
inlinestatic |
Definition at line 6098 of file Native.java.
Referenced by Context.mkFPEq().
|
inlinestatic |
Definition at line 6008 of file Native.java.
Referenced by Context.mkFPFMA().
|
inlinestatic |
Definition at line 5900 of file Native.java.
Referenced by Context.mkFP().
|
inlinestatic |
Definition at line 6080 of file Native.java.
Referenced by Context.mkFPGEq().
|
inlinestatic |
Definition at line 6089 of file Native.java.
Referenced by Context.mkFPGt().
|
inlinestatic |
Definition at line 5882 of file Native.java.
Referenced by Context.mkFPInf().
|
inlinestatic |
Definition at line 6134 of file Native.java.
Referenced by Context.mkFPIsInfinite().
|
inlinestatic |
Definition at line 6143 of file Native.java.
Referenced by Context.mkFPIsNaN().
|
inlinestatic |
Definition at line 6152 of file Native.java.
Referenced by Context.mkFPIsNegative().
|
inlinestatic |
Definition at line 6107 of file Native.java.
Referenced by Context.mkFPIsNormal().
|
inlinestatic |
Definition at line 6161 of file Native.java.
Referenced by Context.mkFPIsPositive().
|
inlinestatic |
Definition at line 6116 of file Native.java.
Referenced by Context.mkFPIsSubnormal().
|
inlinestatic |
Definition at line 6125 of file Native.java.
Referenced by Context.mkFPIsZero().
|
inlinestatic |
Definition at line 6062 of file Native.java.
Referenced by Context.mkFPLEq().
|
inlinestatic |
Definition at line 6071 of file Native.java.
Referenced by Context.mkFPLt().
|
inlinestatic |
Definition at line 6053 of file Native.java.
Referenced by Context.mkFPMax().
|
inlinestatic |
Definition at line 6044 of file Native.java.
Referenced by Context.mkFPMin().
|
inlinestatic |
Definition at line 5990 of file Native.java.
Referenced by Context.mkFPMul().
|
inlinestatic |
Definition at line 5873 of file Native.java.
Referenced by Context.mkFPNaN().
|
inlinestatic |
Definition at line 5963 of file Native.java.
Referenced by Context.mkFPNeg().
|
inlinestatic |
Definition at line 5918 of file Native.java.
Referenced by Context.mkFPNumeral().
|
inlinestatic |
Definition at line 5909 of file Native.java.
Referenced by Context.mkFPNumeral().
|
inlinestatic |
Definition at line 5927 of file Native.java.
Referenced by Context.mkFPNumeral().
|
inlinestatic |
Definition at line 5945 of file Native.java.
Referenced by Context.mkFPNumeral().
|
inlinestatic |
Definition at line 5936 of file Native.java.
Referenced by Context.mkFPNumeral().
|
inlinestatic |
Definition at line 6026 of file Native.java.
Referenced by Context.mkFPRem().
|
inlinestatic |
Definition at line 5729 of file Native.java.
Referenced by Context.mkFPRNA().
|
inlinestatic |
Definition at line 5711 of file Native.java.
Referenced by Context.mkFPRNE().
|
inlinestatic |
Definition at line 5693 of file Native.java.
Referenced by FPRMSort.FPRMSort().
|
inlinestatic |
Definition at line 5720 of file Native.java.
Referenced by Context.mkFPRoundNearestTiesToAway().
|
inlinestatic |
Definition at line 5702 of file Native.java.
Referenced by Context.mkFPRoundNearestTiesToEven().
|
inlinestatic |
Definition at line 6035 of file Native.java.
Referenced by Context.mkFPRoundToIntegral().
|
inlinestatic |
Definition at line 5756 of file Native.java.
Referenced by Context.mkFPRoundTowardNegative().
|
inlinestatic |
Definition at line 5738 of file Native.java.
Referenced by Context.mkFPRoundTowardPositive().
|
inlinestatic |
Definition at line 5774 of file Native.java.
Referenced by Context.mkFPRoundTowardZero().
|
inlinestatic |
Definition at line 5765 of file Native.java.
Referenced by Context.mkFPRTN().
|
inlinestatic |
Definition at line 5747 of file Native.java.
Referenced by Context.mkFPRTP().
|
inlinestatic |
Definition at line 5783 of file Native.java.
Referenced by Context.mkFPRTZ().
|
inlinestatic |
Definition at line 5792 of file Native.java.
Referenced by FPSort.FPSort().
|
inlinestatic |
Definition at line 5864 of file Native.java.
Referenced by Context.mkFPSort128().
|
inlinestatic |
Definition at line 5810 of file Native.java.
Referenced by Context.mkFPSort16().
|
inlinestatic |
Definition at line 5828 of file Native.java.
Referenced by Context.mkFPSort32().
|
inlinestatic |
Definition at line 5846 of file Native.java.
Referenced by Context.mkFPSort64().
|
inlinestatic |
Definition at line 5837 of file Native.java.
Referenced by Context.mkFPSortDouble().
|
inlinestatic |
Definition at line 5801 of file Native.java.
Referenced by Context.mkFPSortHalf().
|
inlinestatic |
Definition at line 5855 of file Native.java.
Referenced by Context.mkFPSortQuadruple().
|
inlinestatic |
Definition at line 5819 of file Native.java.
Referenced by Context.mkFPSortSingle().
|
inlinestatic |
Definition at line 6017 of file Native.java.
Referenced by Context.mkFPSqrt().
|
inlinestatic |
Definition at line 5981 of file Native.java.
Referenced by Context.mkFPSub().
|
inlinestatic |
Definition at line 6170 of file Native.java.
Referenced by Context.mkFPToFP().
|
inlinestatic |
Definition at line 6179 of file Native.java.
Referenced by Context.mkFPToFP().
|
inlinestatic |
Definition at line 6404 of file Native.java.
Referenced by Context.mkFPToFP().
|
inlinestatic |
Definition at line 6188 of file Native.java.
Referenced by Context.mkFPToFP().
|
inlinestatic |
Definition at line 6197 of file Native.java.
Referenced by Context.mkFPToFP().
|
inlinestatic |
Definition at line 6206 of file Native.java.
Referenced by Context.mkFPToFP().
|
inlinestatic |
Definition at line 6395 of file Native.java.
Referenced by Context.mkFPToIEEEBV().
|
inlinestatic |
Definition at line 6233 of file Native.java.
Referenced by Context.mkFPToReal().
|
inlinestatic |
Definition at line 6224 of file Native.java.
Referenced by Context.mkFPToBV().
|
inlinestatic |
Definition at line 6215 of file Native.java.
Referenced by Context.mkFPToBV().
|
inlinestatic |
Definition at line 5891 of file Native.java.
Referenced by Context.mkFPZero().
|
inlinestatic |
Definition at line 1115 of file Native.java.
Referenced by Context.mkFreshConst().
|
inlinestatic |
Definition at line 1106 of file Native.java.
|
inlinestatic |
Definition at line 1880 of file Native.java.
Referenced by Context.mkFullSet().
|
inlinestatic |
Definition at line 1079 of file Native.java.
|
inlinestatic |
Definition at line 1322 of file Native.java.
Referenced by Context.mkGe().
|
inlinestatic |
Definition at line 3745 of file Native.java.
|
inlinestatic |
Definition at line 1313 of file Native.java.
Referenced by Context.mkGt().
|
inlinestatic |
Definition at line 1178 of file Native.java.
Referenced by Context.mkIff().
|
inlinestatic |
Definition at line 1187 of file Native.java.
Referenced by Context.mkImplies().
|
inlinestatic |
Definition at line 1988 of file Native.java.
Referenced by Context.mkInt(), Context.mkNumeral(), and Context.mkReal().
|
inlinestatic |
Definition at line 1700 of file Native.java.
Referenced by Context.mkInt2BV().
|
inlinestatic |
Definition at line 1331 of file Native.java.
Referenced by Context.mkInt2Real().
|
inlinestatic |
Definition at line 2006 of file Native.java.
Referenced by Context.mkInt(), Context.mkNumeral(), and Context.mkReal().
|
inlinestatic |
Definition at line 5623 of file Native.java.
Referenced by InterpolationContext.MkInterpolant().
|
inlinestatic |
Definition at line 5632 of file Native.java.
Referenced by InterpolationContext.mkContext().
|
inlinestatic |
Definition at line 939 of file Native.java.
|
inlinestatic |
Definition at line 903 of file Native.java.
|
inlinestatic |
Definition at line 2222 of file Native.java.
|
inlinestatic |
Definition at line 1349 of file Native.java.
Referenced by Context.mkIsInteger().
|
inlinestatic |
Definition at line 1169 of file Native.java.
Referenced by Context.mkITE().
|
inlinestatic |
Definition at line 1304 of file Native.java.
Referenced by Context.mkLe().
|
inlinestatic |
Definition at line 1011 of file Native.java.
|
inlinestatic |
Definition at line 1295 of file Native.java.
Referenced by Context.mkLt().
|
inlinestatic |
Definition at line 1835 of file Native.java.
Referenced by Context.mkMap().
|
inlinestatic |
Definition at line 1268 of file Native.java.
Referenced by Context.mkMod().
|
inlinestatic |
Definition at line 3293 of file Native.java.
|
inlinestatic |
Definition at line 1232 of file Native.java.
Referenced by Context.mkMul().
|
inlinestatic |
Definition at line 1160 of file Native.java.
Referenced by Context.mkNot().
|
inlinestatic |
Definition at line 1970 of file Native.java.
Referenced by Context.mkInt(), Context.mkNumeral(), and Context.mkReal().
|
inlinestatic |
Definition at line 5406 of file Native.java.
|
inlinestatic |
Definition at line 1214 of file Native.java.
Referenced by Context.mkOr().
|
inlinestatic |
Definition at line 768 of file Native.java.
|
inlinestatic |
Definition at line 2348 of file Native.java.
Referenced by Context.mkPattern().
|
inlinestatic |
Definition at line 2672 of file Native.java.
Referenced by Context.mkPBEq().
|
inlinestatic |
Definition at line 2663 of file Native.java.
Referenced by Context.mkPBGe().
|
inlinestatic |
Definition at line 2654 of file Native.java.
Referenced by Context.mkPBLe().
|
inlinestatic |
Definition at line 1286 of file Native.java.
Referenced by Context.mkPower().
|
inlinestatic |
Definition at line 3901 of file Native.java.
|
inlinestatic |
Definition at line 2384 of file Native.java.
Referenced by Quantifier.of().
|
inlinestatic |
Definition at line 2420 of file Native.java.
Referenced by Quantifier.of().
|
inlinestatic |
Definition at line 2429 of file Native.java.
Referenced by Quantifier.of().
|
inlinestatic |
Definition at line 2393 of file Native.java.
Referenced by Quantifier.of().
|
inlinestatic |
Definition at line 1979 of file Native.java.
Referenced by Context.mkReal().
|
inlinestatic |
Definition at line 1340 of file Native.java.
Referenced by Context.mkReal2Int().
|
inlinestatic |
Definition at line 948 of file Native.java.
|
inlinestatic |
Definition at line 2321 of file Native.java.
Referenced by Context.mkComplement().
|
inlinestatic |
Definition at line 2285 of file Native.java.
Referenced by Context.mkConcat().
|
inlinestatic |
Definition at line 2330 of file Native.java.
|
inlinestatic |
Definition at line 2339 of file Native.java.
|
inlinestatic |
Definition at line 2312 of file Native.java.
Referenced by Context.mkIntersect().
|
inlinestatic |
Definition at line 2303 of file Native.java.
Referenced by Context.mkLoop().
|
inlinestatic |
Definition at line 1277 of file Native.java.
Referenced by Context.mkRem().
|
inlinestatic |
Definition at line 2267 of file Native.java.
Referenced by Context.mkOption().
|
inlinestatic |
Definition at line 1628 of file Native.java.
Referenced by Context.mkRepeat().
|
inlinestatic |
Definition at line 2249 of file Native.java.
Referenced by Context.mkPlus().
|
inlinestatic |
Definition at line 2294 of file Native.java.
Referenced by Context.mkRange().
|
inlinestatic |
Definition at line 2051 of file Native.java.
Referenced by Context.mkReSort().
|
inlinestatic |
Definition at line 2258 of file Native.java.
Referenced by Context.mkStar().
|
inlinestatic |
Definition at line 2276 of file Native.java.
Referenced by Context.mkUnion().
|
inlinestatic |
Definition at line 1664 of file Native.java.
Referenced by Context.mkBVRotateLeft().
|
inlinestatic |
Definition at line 1673 of file Native.java.
Referenced by Context.mkBVRotateRight().
|
inlinestatic |
Definition at line 1790 of file Native.java.
Referenced by Context.mkSelect().
|
inlinestatic |
Definition at line 1799 of file Native.java.
Referenced by Context.mkSelect().
|
inlinestatic |
Definition at line 2186 of file Native.java.
Referenced by Context.mkAt().
|
inlinestatic |
Definition at line 2132 of file Native.java.
Referenced by Context.mkConcat().
|
inlinestatic |
Definition at line 2159 of file Native.java.
Referenced by Context.mkContains().
|
inlinestatic |
Definition at line 2114 of file Native.java.
Referenced by Context.mkEmptySeq().
|
inlinestatic |
Definition at line 2168 of file Native.java.
Referenced by Context.mkExtract().
|
inlinestatic |
Definition at line 2204 of file Native.java.
Referenced by Context.mkIndexOf().
|
inlinestatic |
Definition at line 2240 of file Native.java.
Referenced by Context.mkInRe().
|
inlinestatic |
Definition at line 2195 of file Native.java.
Referenced by Context.mkLength().
|
inlinestatic |
Definition at line 2141 of file Native.java.
Referenced by Context.mkPrefixOf().
|
inlinestatic |
Definition at line 2177 of file Native.java.
Referenced by Context.mkReplace().
|
inlinestatic |
Definition at line 2033 of file Native.java.
Referenced by Context.mkSeqSort().
|
inlinestatic |
Definition at line 2150 of file Native.java.
Referenced by Context.mkSuffixOf().
|
inlinestatic |
Definition at line 2231 of file Native.java.
Referenced by Context.mkToRe().
|
inlinestatic |
Definition at line 2123 of file Native.java.
Referenced by Context.mkUnit().
|
inlinestatic |
Definition at line 1889 of file Native.java.
Referenced by Context.mkSetAdd().
|
inlinestatic |
Definition at line 1934 of file Native.java.
Referenced by Context.mkSetComplement().
|
inlinestatic |
Definition at line 1898 of file Native.java.
Referenced by Context.mkSetDel().
|
inlinestatic |
Definition at line 1925 of file Native.java.
Referenced by Context.mkSetDifference().
|
inlinestatic |
Definition at line 1916 of file Native.java.
Referenced by Context.mkSetIntersection().
|
inlinestatic |
Definition at line 1943 of file Native.java.
Referenced by Context.mkSetMembership().
|
inlinestatic |
Definition at line 1862 of file Native.java.
|
inlinestatic |
Definition at line 1952 of file Native.java.
Referenced by Context.mkSetSubset().
|
inlinestatic |
Definition at line 1907 of file Native.java.
Referenced by Context.mkSetUnion().
|
inlinestatic |
Definition at line 1610 of file Native.java.
Referenced by Context.mkSignExt().
|
inlinestatic |
Definition at line 4284 of file Native.java.
Referenced by Context.mkSimpleSolver().
|
inlinestatic |
Definition at line 4275 of file Native.java.
Referenced by Context.mkSolver().
|
inlinestatic |
Definition at line 4293 of file Native.java.
Referenced by Context.mkSolver().
|
inlinestatic |
Definition at line 4302 of file Native.java.
Referenced by Context.mkSolver().
|
inlinestatic |
Definition at line 1808 of file Native.java.
Referenced by Context.mkStore().
|
inlinestatic |
Definition at line 1817 of file Native.java.
Referenced by Context.mkStore().
|
inlinestatic |
Definition at line 2087 of file Native.java.
Referenced by Context.mkString().
|
inlinestatic |
Definition at line 2069 of file Native.java.
Referenced by Context.mkStringSort().
|
inlinestatic |
Definition at line 912 of file Native.java.
|
inlinestatic |
Definition at line 2213 of file Native.java.
|
inlinestatic |
Definition at line 1241 of file Native.java.
Referenced by Context.mkSub().
|
inlinestatic |
Definition at line 3876 of file Native.java.
|
inlinestatic |
Definition at line 1124 of file Native.java.
Referenced by Context.mkTrue().
|
inlinestatic |
Definition at line 993 of file Native.java.
|
inlinestatic |
Definition at line 1250 of file Native.java.
Referenced by Context.mkUnaryMinus().
|
inlinestatic |
Definition at line 921 of file Native.java.
|
inlinestatic |
Definition at line 1997 of file Native.java.
|
inlinestatic |
Definition at line 2015 of file Native.java.
|
inlinestatic |
Definition at line 1196 of file Native.java.
Referenced by Context.mkXor().
|
inlinestatic |
Definition at line 1619 of file Native.java.
Referenced by Context.mkZeroExt().
|
inlinestatic |
Definition at line 3310 of file Native.java.
|
inlinestatic |
Definition at line 3318 of file Native.java.
Referenced by Model.eval().
|
inlinestatic |
Definition at line 6484 of file Native.java.
|
inlinestatic |
Definition at line 3363 of file Native.java.
Referenced by Model.getConstDecls(), and Model.getDecls().
|
inlinestatic |
Definition at line 3327 of file Native.java.
Referenced by Model.getConstInterp(), and Model.getFuncInterp().
|
inlinestatic |
Definition at line 3381 of file Native.java.
Referenced by Model.getDecls(), and Model.getFuncDecls().
|
inlinestatic |
Definition at line 3345 of file Native.java.
Referenced by Model.getFuncInterp().
|
inlinestatic |
Definition at line 3354 of file Native.java.
Referenced by Model.getNumConsts().
|
inlinestatic |
Definition at line 3372 of file Native.java.
Referenced by Model.getNumFuncs().
|
inlinestatic |
Definition at line 3390 of file Native.java.
Referenced by Model.getNumSorts().
|
inlinestatic |
Definition at line 3399 of file Native.java.
Referenced by Model.getSorts().
|
inlinestatic |
Definition at line 3408 of file Native.java.
Referenced by Model.getSortUniverse().
|
inlinestatic |
Definition at line 3336 of file Native.java.
|
inlinestatic |
Definition at line 3302 of file Native.java.
|
inlinestatic |
Definition at line 3637 of file Native.java.
Referenced by Model.toString().
|
inlinestatic |
Definition at line 3417 of file Native.java.
|
inlinestatic |
Definition at line 3572 of file Native.java.
Referenced by Log.open().
|
inlinestatic |
Definition at line 5431 of file Native.java.
Referenced by Optimize.Assert().
|
inlinestatic |
Definition at line 5439 of file Native.java.
Referenced by Optimize.AssertSoft().
|
inlinestatic |
Definition at line 5482 of file Native.java.
Referenced by Optimize.Check().
|
inlinestatic |
Definition at line 5423 of file Native.java.
|
inlinestatic |
Definition at line 5579 of file Native.java.
Referenced by Optimize.fromFile().
|
inlinestatic |
Definition at line 5571 of file Native.java.
Referenced by Optimize.fromString().
|
inlinestatic |
Definition at line 5605 of file Native.java.
|
inlinestatic |
Definition at line 5587 of file Native.java.
Referenced by Optimize.getHelp().
|
inlinestatic |
Definition at line 5526 of file Native.java.
|
inlinestatic |
Definition at line 5544 of file Native.java.
|
inlinestatic |
Definition at line 5500 of file Native.java.
Referenced by Optimize.getModel().
|
inlinestatic |
Definition at line 5614 of file Native.java.
|
inlinestatic |
Definition at line 5517 of file Native.java.
Referenced by Optimize.getParameterDescriptions().
|
inlinestatic |
Definition at line 5491 of file Native.java.
Referenced by Optimize.getReasonUnknown().
|
inlinestatic |
Definition at line 5596 of file Native.java.
Referenced by Optimize.getStatistics().
|
inlinestatic |
Definition at line 5535 of file Native.java.
|
inlinestatic |
Definition at line 5553 of file Native.java.
|
inlinestatic |
Definition at line 5415 of file Native.java.
|
inlinestatic |
Definition at line 5448 of file Native.java.
Referenced by Optimize.MkMaximize().
|
inlinestatic |
Definition at line 5457 of file Native.java.
Referenced by Optimize.MkMinimize().
|
inlinestatic |
Definition at line 5474 of file Native.java.
Referenced by Optimize.Pop().
|
inlinestatic |
Definition at line 5466 of file Native.java.
Referenced by Optimize.Push().
|
inlinestatic |
Definition at line 5509 of file Native.java.
Referenced by Optimize.setParameters().
|
inlinestatic |
Definition at line 5562 of file Native.java.
Referenced by Optimize.toString().
|
inlinestatic |
Definition at line 850 of file Native.java.
|
inlinestatic |
Definition at line 885 of file Native.java.
Referenced by ParamDescrs.getDocumentation().
|
inlinestatic |
Definition at line 858 of file Native.java.
Referenced by ParamDescrs.getKind().
|
inlinestatic |
Definition at line 876 of file Native.java.
Referenced by ParamDescrs.getNames().
|
inlinestatic |
Definition at line 842 of file Native.java.
|
inlinestatic |
Definition at line 867 of file Native.java.
Referenced by ParamDescrs.getNames(), and ParamDescrs.size().
|
inlinestatic |
Definition at line 894 of file Native.java.
Referenced by ParamDescrs.toString().
|
inlinestatic |
Definition at line 785 of file Native.java.
|
inlinestatic |
Definition at line 777 of file Native.java.
|
inlinestatic |
Definition at line 793 of file Native.java.
Referenced by Params.add().
|
inlinestatic |
Definition at line 809 of file Native.java.
Referenced by Params.add().
|
inlinestatic |
Definition at line 817 of file Native.java.
Referenced by Params.add().
|
inlinestatic |
Definition at line 801 of file Native.java.
Referenced by Params.add().
|
inlinestatic |
Definition at line 825 of file Native.java.
Referenced by Params.toString().
|
inlinestatic |
Definition at line 834 of file Native.java.
Referenced by ParamDescrs.validate().
|
inlinestatic |
Definition at line 3664 of file Native.java.
Referenced by Context.parseSMTLIB2File().
|
inlinestatic |
Definition at line 3655 of file Native.java.
Referenced by Context.parseSMTLIB2String().
|
inlinestatic |
Definition at line 3095 of file Native.java.
|
inlinestatic |
Definition at line 3610 of file Native.java.
Referenced by Pattern.toString().
|
inlinestatic |
Definition at line 4961 of file Native.java.
|
inlinestatic |
Definition at line 4097 of file Native.java.
Referenced by Context.and().
|
inlinestatic |
Definition at line 4196 of file Native.java.
Referenced by Probe.apply().
|
inlinestatic |
Definition at line 4043 of file Native.java.
Referenced by Context.constProbe().
|
inlinestatic |
Definition at line 3918 of file Native.java.
|
inlinestatic |
Definition at line 4088 of file Native.java.
Referenced by Context.eq().
|
inlinestatic |
Definition at line 4079 of file Native.java.
Referenced by Context.ge().
|
inlinestatic |
Definition at line 4187 of file Native.java.
Referenced by Context.getProbeDescription().
|
inlinestatic |
Definition at line 4061 of file Native.java.
Referenced by Context.gt().
|
inlinestatic |
Definition at line 3910 of file Native.java.
|
inlinestatic |
Definition at line 4070 of file Native.java.
Referenced by Context.le().
|
inlinestatic |
Definition at line 4052 of file Native.java.
Referenced by Context.lt().
|
inlinestatic |
Definition at line 4115 of file Native.java.
Referenced by Context.not().
|
inlinestatic |
Definition at line 4106 of file Native.java.
Referenced by Context.or().
|
inlinestatic |
Definition at line 6493 of file Native.java.
|
inlinestatic |
Definition at line 6466 of file Native.java.
|
inlinestatic |
Definition at line 6475 of file Native.java.
|
inlinestatic |
Definition at line 1071 of file Native.java.
Referenced by Constructor.ConstructorDecl(), Constructor.getAccessorDecls(), and Constructor.getTesterDecl().
|
inlinestatic |
Definition at line 5032 of file Native.java.
|
inlinestatic |
Definition at line 4970 of file Native.java.
|
inlinestatic |
Definition at line 5059 of file Native.java.
|
inlinestatic |
Definition at line 5131 of file Native.java.
|
inlinestatic |
Definition at line 5122 of file Native.java.
|
inlinestatic |
Definition at line 5167 of file Native.java.
|
inlinestatic |
Definition at line 5104 of file Native.java.
|
inlinestatic |
Definition at line 5077 of file Native.java.
|
inlinestatic |
Definition at line 5113 of file Native.java.
|
inlinestatic |
Definition at line 5095 of file Native.java.
|
inlinestatic |
Definition at line 5005 of file Native.java.
|
inlinestatic |
Definition at line 5014 of file Native.java.
|
inlinestatic |
Definition at line 4996 of file Native.java.
|
inlinestatic |
Definition at line 4978 of file Native.java.
|
inlinestatic |
Definition at line 5023 of file Native.java.
|
inlinestatic |
Definition at line 4987 of file Native.java.
|
inlinestatic |
Definition at line 5050 of file Native.java.
|
inlinestatic |
Definition at line 5068 of file Native.java.
|
inlinestatic |
Definition at line 5140 of file Native.java.
|
inlinestatic |
Definition at line 5158 of file Native.java.
|
inlinestatic |
Definition at line 5149 of file Native.java.
|
inlinestatic |
Definition at line 5086 of file Native.java.
|
inlinestatic |
Definition at line 5041 of file Native.java.
|
inlinestatic |
Definition at line 5667 of file Native.java.
Referenced by InterpolationContext.ReadInterpolationProblem().
|
inlinestatic |
Definition at line 3735 of file Native.java.
|
inlinestatic |
Definition at line 3593 of file Native.java.
Referenced by Context.setPrintMode().
|
inlinestatic |
Definition at line 3697 of file Native.java.
|
static |
|
inlinestatic |
Definition at line 710 of file Native.java.
Referenced by Context.Context(), and InterpolationContext.mkContext().
|
inlinestatic |
Definition at line 3221 of file Native.java.
Referenced by Expr.simplify().
|
inlinestatic |
Definition at line 3230 of file Native.java.
Referenced by Expr.simplify().
|
inlinestatic |
Definition at line 3239 of file Native.java.
Referenced by Context.SimplifyHelp().
|
inlinestatic |
Definition at line 3248 of file Native.java.
Referenced by Context.getSimplifyParameterDescriptions().
|
inlinestatic |
Definition at line 4395 of file Native.java.
Referenced by Solver.add().
|
inlinestatic |
Definition at line 4403 of file Native.java.
Referenced by Solver.assertAndTrack().
|
inlinestatic |
Definition at line 4436 of file Native.java.
Referenced by Solver.check().
|
inlinestatic |
Definition at line 4445 of file Native.java.
Referenced by Solver.check().
|
inlinestatic |
Definition at line 4354 of file Native.java.
|
inlinestatic |
Definition at line 4420 of file Native.java.
Referenced by Solver.fromFile().
|
inlinestatic |
Definition at line 4428 of file Native.java.
Referenced by Solver.fromString().
|
inlinestatic |
Definition at line 4411 of file Native.java.
Referenced by Solver.getAssertions(), and Solver.getNumAssertions().
|
inlinestatic |
Definition at line 4463 of file Native.java.
|
inlinestatic |
Definition at line 4320 of file Native.java.
Referenced by Solver.getHelp().
|
inlinestatic |
Definition at line 4472 of file Native.java.
Referenced by Solver.getModel().
|
inlinestatic |
Definition at line 4386 of file Native.java.
Referenced by Solver.getNumScopes().
|
inlinestatic |
Definition at line 4329 of file Native.java.
Referenced by Solver.getParameterDescriptions().
|
inlinestatic |
Definition at line 4481 of file Native.java.
Referenced by Solver.getProof().
|
inlinestatic |
Definition at line 4499 of file Native.java.
Referenced by Solver.getReasonUnknown().
|
inlinestatic |
Definition at line 4508 of file Native.java.
Referenced by Solver.getStatistics().
|
inlinestatic |
Definition at line 4490 of file Native.java.
Referenced by Solver.getUnsatCore().
|
inlinestatic |
Definition at line 4346 of file Native.java.
|
inlinestatic |
Definition at line 4370 of file Native.java.
Referenced by Solver.pop().
|
inlinestatic |
Definition at line 4362 of file Native.java.
Referenced by Solver.push().
|
inlinestatic |
Definition at line 4378 of file Native.java.
Referenced by Solver.reset().
|
inlinestatic |
Definition at line 4338 of file Native.java.
Referenced by Solver.setParameters().
|
inlinestatic |
Definition at line 4517 of file Native.java.
Referenced by Solver.toString().
|
inlinestatic |
Definition at line 4311 of file Native.java.
Referenced by Solver.translate().
|
inlinestatic |
Definition at line 2483 of file Native.java.
|
inlinestatic |
Definition at line 3619 of file Native.java.
Referenced by Sort.toString().
|
inlinestatic |
Definition at line 4543 of file Native.java.
|
inlinestatic |
Definition at line 4596 of file Native.java.
Referenced by Statistics.getEntries().
|
inlinestatic |
Definition at line 4560 of file Native.java.
Referenced by Statistics.getEntries(), and Statistics.getKeys().
|
inlinestatic |
Definition at line 4587 of file Native.java.
Referenced by Statistics.getEntries().
|
inlinestatic |
Definition at line 4535 of file Native.java.
|
inlinestatic |
Definition at line 4578 of file Native.java.
Referenced by Statistics.getEntries().
|
inlinestatic |
Definition at line 4569 of file Native.java.
Referenced by Statistics.getEntries().
|
inlinestatic |
Definition at line 4551 of file Native.java.
Referenced by Statistics.size().
|
inlinestatic |
Definition at line 4526 of file Native.java.
Referenced by Statistics.toString().
|
inlinestatic |
Definition at line 3266 of file Native.java.
Referenced by Expr.substitute().
|
inlinestatic |
Definition at line 3275 of file Native.java.
Referenced by Expr.substituteVars().
|
inlinestatic |
Definition at line 3926 of file Native.java.
Referenced by Context.andThen().
|
inlinestatic |
Definition at line 4205 of file Native.java.
Referenced by Tactic.apply().
|
inlinestatic |
Definition at line 4214 of file Native.java.
Referenced by Tactic.apply().
|
inlinestatic |
Definition at line 3980 of file Native.java.
Referenced by Context.cond().
|
inlinestatic |
Definition at line 3893 of file Native.java.
|
inlinestatic |
Definition at line 4007 of file Native.java.
Referenced by Context.fail().
|
inlinestatic |
Definition at line 4016 of file Native.java.
Referenced by Context.failIf().
|
inlinestatic |
Definition at line 4025 of file Native.java.
Referenced by Context.failIfNotDecided().
|
inlinestatic |
Definition at line 4178 of file Native.java.
Referenced by Context.getTacticDescription().
|
inlinestatic |
Definition at line 4160 of file Native.java.
Referenced by Tactic.getHelp().
|
inlinestatic |
Definition at line 4169 of file Native.java.
Referenced by Tactic.getParameterDescriptions().
|
inlinestatic |
Definition at line 3885 of file Native.java.
|
inlinestatic |
Definition at line 3935 of file Native.java.
Referenced by Context.orElse().
|
inlinestatic |
Definition at line 3953 of file Native.java.
Referenced by Context.parAndThen().
|
inlinestatic |
Definition at line 3944 of file Native.java.
Referenced by Context.parOr().
|
inlinestatic |
Definition at line 3989 of file Native.java.
Referenced by Context.repeat().
|
inlinestatic |
Definition at line 3998 of file Native.java.
Referenced by Context.skip().
|
inlinestatic |
Definition at line 3962 of file Native.java.
Referenced by Context.tryFor().
|
inlinestatic |
Definition at line 4034 of file Native.java.
Referenced by Context.usingParams().
|
inlinestatic |
Definition at line 3971 of file Native.java.
Referenced by Context.when().
|
inlinestatic |
Definition at line 2969 of file Native.java.
|
inlinestatic |
Definition at line 2978 of file Native.java.
|
inlinestatic |
Definition at line 3588 of file Native.java.
Referenced by Global.ToggleWarningMessages().
|
inlinestatic |
Definition at line 3284 of file Native.java.
Referenced by AST.translate().
|
inlinestatic |
Definition at line 752 of file Native.java.
Referenced by Context.updateParamValue().
|
inlinestatic |
Definition at line 3257 of file Native.java.
Referenced by Expr.update().
|
inlinestatic |
Definition at line 5685 of file Native.java.
Referenced by InterpolationContext.WriteInterpolationProblem().