Data Structures | |
class | IntPtr |
class | LongPtr |
class | ObjArrayPtr |
class | StringPtr |
class | UIntArrayPtr |
Static Public Member Functions | |
static native void | setInternalErrorHandler (long ctx) |
static void | globalParamSet (String a0, String a1) |
static void | globalParamResetAll () |
static boolean | globalParamGet (String a0, StringPtr a1) |
static long | mkConfig () |
static void | delConfig (long a0) |
static void | setParamValue (long a0, String a1, String a2) |
static long | mkContext (long a0) throws Z3Exception |
static long | mkContextRc (long a0) throws Z3Exception |
static void | delContext (long a0) throws Z3Exception |
static void | incRef (long a0, long a1) throws Z3Exception |
static void | decRef (long a0, long a1) throws Z3Exception |
static void | updateParamValue (long a0, String a1, String a2) throws Z3Exception |
static void | interrupt (long a0) throws Z3Exception |
static long | mkParams (long a0) throws Z3Exception |
static void | paramsIncRef (long a0, long a1) throws Z3Exception |
static void | paramsDecRef (long a0, long a1) throws Z3Exception |
static void | paramsSetBool (long a0, long a1, long a2, boolean a3) throws Z3Exception |
static void | paramsSetUint (long a0, long a1, long a2, int a3) throws Z3Exception |
static void | paramsSetDouble (long a0, long a1, long a2, double a3) throws Z3Exception |
static void | paramsSetSymbol (long a0, long a1, long a2, long a3) throws Z3Exception |
static String | paramsToString (long a0, long a1) throws Z3Exception |
static void | paramsValidate (long a0, long a1, long a2) throws Z3Exception |
static void | paramDescrsIncRef (long a0, long a1) throws Z3Exception |
static void | paramDescrsDecRef (long a0, long a1) throws Z3Exception |
static int | paramDescrsGetKind (long a0, long a1, long a2) throws Z3Exception |
static int | paramDescrsSize (long a0, long a1) throws Z3Exception |
static long | paramDescrsGetName (long a0, long a1, int a2) throws Z3Exception |
static String | paramDescrsGetDocumentation (long a0, long a1, long a2) throws Z3Exception |
static String | paramDescrsToString (long a0, long a1) throws Z3Exception |
static long | mkIntSymbol (long a0, int a1) throws Z3Exception |
static long | mkStringSymbol (long a0, String a1) throws Z3Exception |
static long | mkUninterpretedSort (long a0, long a1) throws Z3Exception |
static long | mkBoolSort (long a0) throws Z3Exception |
static long | mkIntSort (long a0) throws Z3Exception |
static long | mkRealSort (long a0) throws Z3Exception |
static long | mkBvSort (long a0, int a1) throws Z3Exception |
static long | mkFiniteDomainSort (long a0, long a1, long a2) throws Z3Exception |
static long | mkArraySort (long a0, long a1, long a2) throws Z3Exception |
static long | mkArraySortN (long a0, int a1, long[] a2, long a3) throws Z3Exception |
static long | mkTupleSort (long a0, long a1, int a2, long[] a3, long[] a4, LongPtr a5, long[] a6) throws Z3Exception |
static long | mkEnumerationSort (long a0, long a1, int a2, long[] a3, long[] a4, long[] a5) throws Z3Exception |
static long | mkListSort (long a0, long a1, long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8) throws Z3Exception |
static long | mkConstructor (long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6) throws Z3Exception |
static void | delConstructor (long a0, long a1) throws Z3Exception |
static long | mkDatatype (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | mkConstructorList (long a0, int a1, long[] a2) throws Z3Exception |
static void | delConstructorList (long a0, long a1) throws Z3Exception |
static void | mkDatatypes (long a0, int a1, long[] a2, long[] a3, long[] a4) throws Z3Exception |
static void | queryConstructor (long a0, long a1, int a2, LongPtr a3, LongPtr a4, long[] a5) throws Z3Exception |
static long | mkFuncDecl (long a0, long a1, int a2, long[] a3, long a4) throws Z3Exception |
static long | mkApp (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | mkConst (long a0, long a1, long a2) throws Z3Exception |
static long | mkFreshFuncDecl (long a0, String a1, int a2, long[] a3, long a4) throws Z3Exception |
static long | mkFreshConst (long a0, String a1, long a2) throws Z3Exception |
static long | mkRecFuncDecl (long a0, long a1, int a2, long[] a3, long a4) throws Z3Exception |
static void | addRecDef (long a0, long a1, int a2, long[] a3, long a4) throws Z3Exception |
static long | mkTrue (long a0) throws Z3Exception |
static long | mkFalse (long a0) throws Z3Exception |
static long | mkEq (long a0, long a1, long a2) throws Z3Exception |
static long | mkDistinct (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkNot (long a0, long a1) throws Z3Exception |
static long | mkIte (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkIff (long a0, long a1, long a2) throws Z3Exception |
static long | mkImplies (long a0, long a1, long a2) throws Z3Exception |
static long | mkXor (long a0, long a1, long a2) throws Z3Exception |
static long | mkAnd (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkOr (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkAdd (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkMul (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkSub (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkUnaryMinus (long a0, long a1) throws Z3Exception |
static long | mkDiv (long a0, long a1, long a2) throws Z3Exception |
static long | mkMod (long a0, long a1, long a2) throws Z3Exception |
static long | mkRem (long a0, long a1, long a2) throws Z3Exception |
static long | mkPower (long a0, long a1, long a2) throws Z3Exception |
static long | mkLt (long a0, long a1, long a2) throws Z3Exception |
static long | mkLe (long a0, long a1, long a2) throws Z3Exception |
static long | mkGt (long a0, long a1, long a2) throws Z3Exception |
static long | mkGe (long a0, long a1, long a2) throws Z3Exception |
static long | 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 long | mkLambda (long a0, int a1, long[] a2, long[] a3, long a4) throws Z3Exception |
static long | mkLambdaConst (long a0, int a1, long[] a2, long a3) throws Z3Exception |
static int | getSymbolKind (long a0, long a1) throws Z3Exception |
static int | getSymbolInt (long a0, long a1) throws Z3Exception |
static String | getSymbolString (long a0, long a1) throws Z3Exception |
static long | getSortName (long a0, long a1) throws Z3Exception |
static int | getSortId (long a0, long a1) throws Z3Exception |
static long | sortToAst (long a0, long a1) throws Z3Exception |
static boolean | isEqSort (long a0, long a1, long a2) throws Z3Exception |
static int | getSortKind (long a0, long a1) throws Z3Exception |
static int | getBvSortSize (long a0, long a1) throws Z3Exception |
static boolean | getFiniteDomainSortSize (long a0, long a1, LongPtr a2) throws Z3Exception |
static long | getArraySortDomain (long a0, long a1) throws Z3Exception |
static long | getArraySortRange (long a0, long a1) throws Z3Exception |
static long | getTupleSortMkDecl (long a0, long a1) throws Z3Exception |
static int | getTupleSortNumFields (long a0, long a1) throws Z3Exception |
static long | getTupleSortFieldDecl (long a0, long a1, int a2) throws Z3Exception |
static int | getDatatypeSortNumConstructors (long a0, long a1) throws Z3Exception |
static long | getDatatypeSortConstructor (long a0, long a1, int a2) throws Z3Exception |
static long | getDatatypeSortRecognizer (long a0, long a1, int a2) throws Z3Exception |
static long | getDatatypeSortConstructorAccessor (long a0, long a1, int a2, int a3) throws Z3Exception |
static long | datatypeUpdateField (long a0, long a1, long a2, long a3) throws Z3Exception |
static int | getRelationArity (long a0, long a1) throws Z3Exception |
static long | getRelationColumn (long a0, long a1, int a2) throws Z3Exception |
static long | mkAtmost (long a0, int a1, long[] a2, int a3) throws Z3Exception |
static long | mkAtleast (long a0, int a1, long[] a2, int a3) throws Z3Exception |
static long | mkPble (long a0, int a1, long[] a2, int[] a3, int a4) throws Z3Exception |
static long | mkPbge (long a0, int a1, long[] a2, int[] a3, int a4) throws Z3Exception |
static long | mkPbeq (long a0, int a1, long[] a2, int[] a3, int a4) throws Z3Exception |
static long | funcDeclToAst (long a0, long a1) throws Z3Exception |
static boolean | isEqFuncDecl (long a0, long a1, long a2) throws Z3Exception |
static int | getFuncDeclId (long a0, long a1) throws Z3Exception |
static long | getDeclName (long a0, long a1) throws Z3Exception |
static int | getDeclKind (long a0, long a1) throws Z3Exception |
static int | getDomainSize (long a0, long a1) throws Z3Exception |
static int | getArity (long a0, long a1) throws Z3Exception |
static long | getDomain (long a0, long a1, int a2) throws Z3Exception |
static long | getRange (long a0, long a1) throws Z3Exception |
static int | getDeclNumParameters (long a0, long a1) throws Z3Exception |
static int | getDeclParameterKind (long a0, long a1, int a2) throws Z3Exception |
static int | getDeclIntParameter (long a0, long a1, int a2) throws Z3Exception |
static double | getDeclDoubleParameter (long a0, long a1, int a2) throws Z3Exception |
static long | getDeclSymbolParameter (long a0, long a1, int a2) throws Z3Exception |
static long | getDeclSortParameter (long a0, long a1, int a2) throws Z3Exception |
static long | getDeclAstParameter (long a0, long a1, int a2) throws Z3Exception |
static long | getDeclFuncDeclParameter (long a0, long a1, int a2) throws Z3Exception |
static String | getDeclRationalParameter (long a0, long a1, int a2) throws Z3Exception |
static long | appToAst (long a0, long a1) throws Z3Exception |
static long | getAppDecl (long a0, long a1) throws Z3Exception |
static int | getAppNumArgs (long a0, long a1) throws Z3Exception |
static long | getAppArg (long a0, long a1, int a2) throws Z3Exception |
static boolean | isEqAst (long a0, long a1, long a2) throws Z3Exception |
static int | getAstId (long a0, long a1) throws Z3Exception |
static int | getAstHash (long a0, long a1) throws Z3Exception |
static long | getSort (long a0, long a1) throws Z3Exception |
static boolean | isWellSorted (long a0, long a1) throws Z3Exception |
static int | getBoolValue (long a0, long a1) throws Z3Exception |
static int | getAstKind (long a0, long a1) throws Z3Exception |
static boolean | isApp (long a0, long a1) throws Z3Exception |
static boolean | isNumeralAst (long a0, long a1) throws Z3Exception |
static boolean | isAlgebraicNumber (long a0, long a1) throws Z3Exception |
static long | toApp (long a0, long a1) throws Z3Exception |
static long | toFuncDecl (long a0, long a1) throws Z3Exception |
static String | getNumeralString (long a0, long a1) throws Z3Exception |
static String | getNumeralDecimalString (long a0, long a1, int a2) throws Z3Exception |
static double | getNumeralDouble (long a0, long a1) throws Z3Exception |
static long | getNumerator (long a0, long a1) throws Z3Exception |
static long | getDenominator (long a0, long a1) throws Z3Exception |
static boolean | getNumeralSmall (long a0, long a1, LongPtr a2, LongPtr a3) throws Z3Exception |
static boolean | getNumeralInt (long a0, long a1, IntPtr a2) throws Z3Exception |
static boolean | getNumeralUint (long a0, long a1, IntPtr a2) throws Z3Exception |
static boolean | getNumeralUint64 (long a0, long a1, LongPtr a2) throws Z3Exception |
static boolean | getNumeralInt64 (long a0, long a1, LongPtr a2) throws Z3Exception |
static boolean | getNumeralRationalInt64 (long a0, long a1, LongPtr a2, LongPtr a3) throws Z3Exception |
static long | getAlgebraicNumberLower (long a0, long a1, int a2) throws Z3Exception |
static long | getAlgebraicNumberUpper (long a0, long a1, int a2) throws Z3Exception |
static long | patternToAst (long a0, long a1) throws Z3Exception |
static int | getPatternNumTerms (long a0, long a1) throws Z3Exception |
static long | getPattern (long a0, long a1, int a2) throws Z3Exception |
static int | getIndexValue (long a0, long a1) throws Z3Exception |
static boolean | isQuantifierForall (long a0, long a1) throws Z3Exception |
static boolean | isQuantifierExists (long a0, long a1) throws Z3Exception |
static boolean | isLambda (long a0, long a1) throws Z3Exception |
static int | getQuantifierWeight (long a0, long a1) throws Z3Exception |
static int | getQuantifierNumPatterns (long a0, long a1) throws Z3Exception |
static long | getQuantifierPatternAst (long a0, long a1, int a2) throws Z3Exception |
static int | getQuantifierNumNoPatterns (long a0, long a1) throws Z3Exception |
static long | getQuantifierNoPatternAst (long a0, long a1, int a2) throws Z3Exception |
static int | getQuantifierNumBound (long a0, long a1) throws Z3Exception |
static long | getQuantifierBoundName (long a0, long a1, int a2) throws Z3Exception |
static long | getQuantifierBoundSort (long a0, long a1, int a2) throws Z3Exception |
static long | getQuantifierBody (long a0, long a1) throws Z3Exception |
static long | simplify (long a0, long a1) throws Z3Exception |
static long | simplifyEx (long a0, long a1, long a2) throws Z3Exception |
static String | simplifyGetHelp (long a0) throws Z3Exception |
static long | simplifyGetParamDescrs (long a0) throws Z3Exception |
static long | updateTerm (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | substitute (long a0, long a1, int a2, long[] a3, long[] a4) throws Z3Exception |
static long | substituteVars (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | translate (long a0, long a1, long a2) throws Z3Exception |
static long | mkModel (long a0) throws Z3Exception |
static void | modelIncRef (long a0, long a1) throws Z3Exception |
static void | modelDecRef (long a0, long a1) throws Z3Exception |
static boolean | modelEval (long a0, long a1, long a2, boolean a3, LongPtr a4) throws Z3Exception |
static long | modelGetConstInterp (long a0, long a1, long a2) throws Z3Exception |
static boolean | modelHasInterp (long a0, long a1, long a2) throws Z3Exception |
static long | modelGetFuncInterp (long a0, long a1, long a2) throws Z3Exception |
static int | modelGetNumConsts (long a0, long a1) throws Z3Exception |
static long | modelGetConstDecl (long a0, long a1, int a2) throws Z3Exception |
static int | modelGetNumFuncs (long a0, long a1) throws Z3Exception |
static long | modelGetFuncDecl (long a0, long a1, int a2) throws Z3Exception |
static int | modelGetNumSorts (long a0, long a1) throws Z3Exception |
static long | modelGetSort (long a0, long a1, int a2) throws Z3Exception |
static long | modelGetSortUniverse (long a0, long a1, long a2) throws Z3Exception |
static long | modelTranslate (long a0, long a1, long a2) throws Z3Exception |
static boolean | isAsArray (long a0, long a1) throws Z3Exception |
static long | getAsArrayFuncDecl (long a0, long a1) throws Z3Exception |
static long | addFuncInterp (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | addConstInterp (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | funcInterpIncRef (long a0, long a1) throws Z3Exception |
static void | funcInterpDecRef (long a0, long a1) throws Z3Exception |
static int | funcInterpGetNumEntries (long a0, long a1) throws Z3Exception |
static long | funcInterpGetEntry (long a0, long a1, int a2) throws Z3Exception |
static long | funcInterpGetElse (long a0, long a1) throws Z3Exception |
static void | funcInterpSetElse (long a0, long a1, long a2) throws Z3Exception |
static int | funcInterpGetArity (long a0, long a1) throws Z3Exception |
static void | funcInterpAddEntry (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | funcEntryIncRef (long a0, long a1) throws Z3Exception |
static void | funcEntryDecRef (long a0, long a1) throws Z3Exception |
static long | funcEntryGetValue (long a0, long a1) throws Z3Exception |
static int | funcEntryGetNumArgs (long a0, long a1) throws Z3Exception |
static long | funcEntryGetArg (long a0, long a1, int a2) throws Z3Exception |
static int | openLog (String a0) |
static void | appendLog (String a0) |
static void | closeLog () |
static void | toggleWarningMessages (boolean a0) |
static void | setAstPrintMode (long a0, int a1) throws Z3Exception |
static String | astToString (long a0, long a1) throws Z3Exception |
static String | patternToString (long a0, long a1) throws Z3Exception |
static String | sortToString (long a0, long a1) throws Z3Exception |
static String | funcDeclToString (long a0, long a1) throws Z3Exception |
static String | modelToString (long a0, long a1) throws Z3Exception |
static String | benchmarkToSmtlibString (long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7) throws Z3Exception |
static long | parseSmtlib2String (long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7) throws Z3Exception |
static long | parseSmtlib2File (long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7) throws Z3Exception |
static String | evalSmtlib2String (long a0, String a1) throws Z3Exception |
static int | getErrorCode (long a0) throws Z3Exception |
static void | setError (long a0, int a1) throws Z3Exception |
static String | getErrorMsg (long a0, int a1) throws Z3Exception |
static void | getVersion (IntPtr a0, IntPtr a1, IntPtr a2, IntPtr a3) |
static String | getFullVersion () |
static void | enableTrace (String a0) |
static void | disableTrace (String a0) |
static void | resetMemory () |
static void | finalizeMemory () |
static long | mkGoal (long a0, boolean a1, boolean a2, boolean a3) throws Z3Exception |
static void | goalIncRef (long a0, long a1) throws Z3Exception |
static void | goalDecRef (long a0, long a1) throws Z3Exception |
static int | goalPrecision (long a0, long a1) throws Z3Exception |
static void | goalAssert (long a0, long a1, long a2) throws Z3Exception |
static boolean | goalInconsistent (long a0, long a1) throws Z3Exception |
static int | goalDepth (long a0, long a1) throws Z3Exception |
static void | goalReset (long a0, long a1) throws Z3Exception |
static int | goalSize (long a0, long a1) throws Z3Exception |
static long | goalFormula (long a0, long a1, int a2) throws Z3Exception |
static int | goalNumExprs (long a0, long a1) throws Z3Exception |
static boolean | goalIsDecidedSat (long a0, long a1) throws Z3Exception |
static boolean | goalIsDecidedUnsat (long a0, long a1) throws Z3Exception |
static long | goalTranslate (long a0, long a1, long a2) throws Z3Exception |
static long | goalConvertModel (long a0, long a1, long a2) throws Z3Exception |
static String | goalToString (long a0, long a1) throws Z3Exception |
static String | goalToDimacsString (long a0, long a1) throws Z3Exception |
static long | mkTactic (long a0, String a1) throws Z3Exception |
static void | tacticIncRef (long a0, long a1) throws Z3Exception |
static void | tacticDecRef (long a0, long a1) throws Z3Exception |
static long | mkProbe (long a0, String a1) throws Z3Exception |
static void | probeIncRef (long a0, long a1) throws Z3Exception |
static void | probeDecRef (long a0, long a1) throws Z3Exception |
static long | tacticAndThen (long a0, long a1, long a2) throws Z3Exception |
static long | tacticOrElse (long a0, long a1, long a2) throws Z3Exception |
static long | tacticParOr (long a0, int a1, long[] a2) throws Z3Exception |
static long | tacticParAndThen (long a0, long a1, long a2) throws Z3Exception |
static long | tacticTryFor (long a0, long a1, int a2) throws Z3Exception |
static long | tacticWhen (long a0, long a1, long a2) throws Z3Exception |
static long | tacticCond (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | tacticRepeat (long a0, long a1, int a2) throws Z3Exception |
static long | tacticSkip (long a0) throws Z3Exception |
static long | tacticFail (long a0) throws Z3Exception |
static long | tacticFailIf (long a0, long a1) throws Z3Exception |
static long | tacticFailIfNotDecided (long a0) throws Z3Exception |
static long | tacticUsingParams (long a0, long a1, long a2) throws Z3Exception |
static long | probeConst (long a0, double a1) throws Z3Exception |
static long | probeLt (long a0, long a1, long a2) throws Z3Exception |
static long | probeGt (long a0, long a1, long a2) throws Z3Exception |
static long | probeLe (long a0, long a1, long a2) throws Z3Exception |
static long | probeGe (long a0, long a1, long a2) throws Z3Exception |
static long | probeEq (long a0, long a1, long a2) throws Z3Exception |
static long | probeAnd (long a0, long a1, long a2) throws Z3Exception |
static long | probeOr (long a0, long a1, long a2) throws Z3Exception |
static long | probeNot (long a0, long a1) throws Z3Exception |
static int | getNumTactics (long a0) throws Z3Exception |
static String | getTacticName (long a0, int a1) throws Z3Exception |
static int | getNumProbes (long a0) throws Z3Exception |
static String | getProbeName (long a0, int a1) throws Z3Exception |
static String | tacticGetHelp (long a0, long a1) throws Z3Exception |
static long | tacticGetParamDescrs (long a0, long a1) throws Z3Exception |
static String | tacticGetDescr (long a0, String a1) throws Z3Exception |
static String | probeGetDescr (long a0, String a1) throws Z3Exception |
static double | probeApply (long a0, long a1, long a2) throws Z3Exception |
static long | tacticApply (long a0, long a1, long a2) throws Z3Exception |
static long | tacticApplyEx (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | applyResultIncRef (long a0, long a1) throws Z3Exception |
static void | applyResultDecRef (long a0, long a1) throws Z3Exception |
static String | applyResultToString (long a0, long a1) throws Z3Exception |
static int | applyResultGetNumSubgoals (long a0, long a1) throws Z3Exception |
static long | applyResultGetSubgoal (long a0, long a1, int a2) throws Z3Exception |
static long | mkSolver (long a0) throws Z3Exception |
static long | mkSimpleSolver (long a0) throws Z3Exception |
static long | mkSolverForLogic (long a0, long a1) throws Z3Exception |
static long | mkSolverFromTactic (long a0, long a1) throws Z3Exception |
static long | solverTranslate (long a0, long a1, long a2) throws Z3Exception |
static void | solverImportModelConverter (long a0, long a1, long a2) throws Z3Exception |
static String | solverGetHelp (long a0, long a1) throws Z3Exception |
static long | solverGetParamDescrs (long a0, long a1) throws Z3Exception |
static void | solverSetParams (long a0, long a1, long a2) throws Z3Exception |
static void | solverIncRef (long a0, long a1) throws Z3Exception |
static void | solverDecRef (long a0, long a1) throws Z3Exception |
static void | solverPush (long a0, long a1) throws Z3Exception |
static void | solverPop (long a0, long a1, int a2) throws Z3Exception |
static void | solverReset (long a0, long a1) throws Z3Exception |
static int | solverGetNumScopes (long a0, long a1) throws Z3Exception |
static void | solverAssert (long a0, long a1, long a2) throws Z3Exception |
static void | solverAssertAndTrack (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | solverFromFile (long a0, long a1, String a2) throws Z3Exception |
static void | solverFromString (long a0, long a1, String a2) throws Z3Exception |
static long | solverGetAssertions (long a0, long a1) throws Z3Exception |
static long | solverGetUnits (long a0, long a1) throws Z3Exception |
static long | solverGetNonUnits (long a0, long a1) throws Z3Exception |
static int | solverCheck (long a0, long a1) throws Z3Exception |
static int | solverCheckAssumptions (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static int | getImpliedEqualities (long a0, long a1, int a2, long[] a3, int[] a4) throws Z3Exception |
static int | solverGetConsequences (long a0, long a1, long a2, long a3, long a4) throws Z3Exception |
static long | solverCube (long a0, long a1, long a2, int a3) throws Z3Exception |
static long | solverGetModel (long a0, long a1) throws Z3Exception |
static long | solverGetProof (long a0, long a1) throws Z3Exception |
static long | solverGetUnsatCore (long a0, long a1) throws Z3Exception |
static String | solverGetReasonUnknown (long a0, long a1) throws Z3Exception |
static long | solverGetStatistics (long a0, long a1) throws Z3Exception |
static String | solverToString (long a0, long a1) throws Z3Exception |
static String | 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, int a2, long[] a3) throws Z3Exception |
static String | optimizeGetReasonUnknown (long a0, long a1) throws Z3Exception |
static long | optimizeGetModel (long a0, long a1) throws Z3Exception |
static long | optimizeGetUnsatCore (long a0, long a1) throws Z3Exception |
static void | optimizeSetParams (long a0, long a1, long a2) throws Z3Exception |
static long | optimizeGetParamDescrs (long a0, long a1) throws Z3Exception |
static long | optimizeGetLower (long a0, long a1, int a2) throws Z3Exception |
static long | optimizeGetUpper (long a0, long a1, int a2) throws Z3Exception |
static long | optimizeGetLowerAsVector (long a0, long a1, int a2) throws Z3Exception |
static long | optimizeGetUpperAsVector (long a0, long a1, int a2) throws Z3Exception |
static String | optimizeToString (long a0, long a1) throws Z3Exception |
static void | optimizeFromString (long a0, long a1, String a2) throws Z3Exception |
static void | optimizeFromFile (long a0, long a1, String a2) throws Z3Exception |
static String | optimizeGetHelp (long a0, long a1) throws Z3Exception |
static long | optimizeGetStatistics (long a0, long a1) throws Z3Exception |
static long | optimizeGetAssertions (long a0, long a1) throws Z3Exception |
static long | optimizeGetObjectives (long a0, long a1) throws Z3Exception |
static long | mkFpaRoundingModeSort (long a0) throws Z3Exception |
static long | mkFpaRoundNearestTiesToEven (long a0) throws Z3Exception |
static long | mkFpaRne (long a0) throws Z3Exception |
static long | mkFpaRoundNearestTiesToAway (long a0) throws Z3Exception |
static long | mkFpaRna (long a0) throws Z3Exception |
static long | mkFpaRoundTowardPositive (long a0) throws Z3Exception |
static long | mkFpaRtp (long a0) throws Z3Exception |
static long | mkFpaRoundTowardNegative (long a0) throws Z3Exception |
static long | mkFpaRtn (long a0) throws Z3Exception |
static long | mkFpaRoundTowardZero (long a0) throws Z3Exception |
static long | mkFpaRtz (long a0) throws Z3Exception |
static long | mkFpaSort (long a0, int a1, int a2) throws Z3Exception |
static long | mkFpaSortHalf (long a0) throws Z3Exception |
static long | mkFpaSort16 (long a0) throws Z3Exception |
static long | mkFpaSortSingle (long a0) throws Z3Exception |
static long | mkFpaSort32 (long a0) throws Z3Exception |
static long | mkFpaSortDouble (long a0) throws Z3Exception |
static long | mkFpaSort64 (long a0) throws Z3Exception |
static long | mkFpaSortQuadruple (long a0) throws Z3Exception |
static long | mkFpaSort128 (long a0) throws Z3Exception |
static long | mkFpaNan (long a0, long a1) throws Z3Exception |
static long | mkFpaInf (long a0, long a1, boolean a2) throws Z3Exception |
static long | mkFpaZero (long a0, long a1, boolean a2) throws Z3Exception |
static long | mkFpaFp (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaNumeralFloat (long a0, float a1, long a2) throws Z3Exception |
static long | mkFpaNumeralDouble (long a0, double a1, long a2) throws Z3Exception |
static long | mkFpaNumeralInt (long a0, int a1, long a2) throws Z3Exception |
static long | mkFpaNumeralIntUint (long a0, boolean a1, int a2, int a3, long a4) throws Z3Exception |
static long | mkFpaNumeralInt64Uint64 (long a0, boolean a1, long a2, long a3, long a4) throws Z3Exception |
static long | mkFpaAbs (long a0, long a1) throws Z3Exception |
static long | mkFpaNeg (long a0, long a1) throws Z3Exception |
static long | mkFpaAdd (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaSub (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaMul (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaDiv (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaFma (long a0, long a1, long a2, long a3, long a4) throws Z3Exception |
static long | mkFpaSqrt (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaRem (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaRoundToIntegral (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaMin (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaMax (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaLeq (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaLt (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaGeq (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaGt (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaEq (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaIsNormal (long a0, long a1) throws Z3Exception |
static long | mkFpaIsSubnormal (long a0, long a1) throws Z3Exception |
static long | mkFpaIsZero (long a0, long a1) throws Z3Exception |
static long | mkFpaIsInfinite (long a0, long a1) throws Z3Exception |
static long | mkFpaIsNan (long a0, long a1) throws Z3Exception |
static long | mkFpaIsNegative (long a0, long a1) throws Z3Exception |
static long | mkFpaIsPositive (long a0, long a1) throws Z3Exception |
static long | mkFpaToFpBv (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaToFpFloat (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaToFpReal (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaToFpSigned (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaToFpUnsigned (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaToUbv (long a0, long a1, long a2, int a3) throws Z3Exception |
static long | mkFpaToSbv (long a0, long a1, long a2, int a3) throws Z3Exception |
static long | mkFpaToReal (long a0, long a1) throws Z3Exception |
static int | fpaGetEbits (long a0, long a1) throws Z3Exception |
static int | fpaGetSbits (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralNan (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralInf (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralZero (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralNormal (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralSubnormal (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralPositive (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralNegative (long a0, long a1) throws Z3Exception |
static long | fpaGetNumeralSignBv (long a0, long a1) throws Z3Exception |
static long | fpaGetNumeralSignificandBv (long a0, long a1) throws Z3Exception |
static boolean | fpaGetNumeralSign (long a0, long a1, IntPtr a2) throws Z3Exception |
static String | fpaGetNumeralSignificandString (long a0, long a1) throws Z3Exception |
static boolean | fpaGetNumeralSignificandUint64 (long a0, long a1, LongPtr a2) throws Z3Exception |
static String | fpaGetNumeralExponentString (long a0, long a1, boolean a2) throws Z3Exception |
static boolean | fpaGetNumeralExponentInt64 (long a0, long a1, LongPtr a2, boolean a3) throws Z3Exception |
static long | fpaGetNumeralExponentBv (long a0, long a1, boolean a2) throws Z3Exception |
static long | mkFpaToIeeeBv (long a0, long a1) throws Z3Exception |
static long | mkFpaToFpIntReal (long a0, long a1, long a2, long a3, long a4) throws Z3Exception |
static int | fixedpointQueryFromLvl (long a0, long a1, long a2, int a3) throws Z3Exception |
static long | fixedpointGetGroundSatAnswer (long a0, long a1) throws Z3Exception |
static long | fixedpointGetRulesAlongTrace (long a0, long a1) throws Z3Exception |
static long | fixedpointGetRuleNamesAlongTrace (long a0, long a1) throws Z3Exception |
static void | fixedpointAddInvariant (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | fixedpointGetReachable (long a0, long a1, long a2) throws Z3Exception |
static long | qeModelProject (long a0, long a1, int a2, long[] a3, long a4) throws Z3Exception |
static long | qeModelProjectSkolem (long a0, long a1, int a2, long[] a3, long a4, long a5) throws Z3Exception |
static long | modelExtrapolate (long a0, long a1, long a2) throws Z3Exception |
static long | qeLite (long a0, long a1, long a2) throws Z3Exception |
Static Protected Member Functions | |
static native void | INTERNALglobalParamSet (String a0, String a1) |
static native void | INTERNALglobalParamResetAll () |
static native boolean | INTERNALglobalParamGet (String a0, StringPtr a1) |
static native long | INTERNALmkConfig () |
static native void | INTERNALdelConfig (long a0) |
static native void | INTERNALsetParamValue (long a0, String a1, String a2) |
static native long | INTERNALmkContext (long a0) |
static native long | INTERNALmkContextRc (long a0) |
static native void | INTERNALdelContext (long a0) |
static native void | INTERNALincRef (long a0, long a1) |
static native void | INTERNALdecRef (long a0, long a1) |
static native void | INTERNALupdateParamValue (long a0, String a1, String a2) |
static native void | INTERNALinterrupt (long a0) |
static native long | INTERNALmkParams (long a0) |
static native void | INTERNALparamsIncRef (long a0, long a1) |
static native void | INTERNALparamsDecRef (long a0, long a1) |
static native void | INTERNALparamsSetBool (long a0, long a1, long a2, boolean a3) |
static native void | INTERNALparamsSetUint (long a0, long a1, long a2, int a3) |
static native void | INTERNALparamsSetDouble (long a0, long a1, long a2, double a3) |
static native void | INTERNALparamsSetSymbol (long a0, long a1, long a2, long a3) |
static native String | INTERNALparamsToString (long a0, long a1) |
static native void | INTERNALparamsValidate (long a0, long a1, long a2) |
static native void | INTERNALparamDescrsIncRef (long a0, long a1) |
static native void | INTERNALparamDescrsDecRef (long a0, long a1) |
static native int | INTERNALparamDescrsGetKind (long a0, long a1, long a2) |
static native int | INTERNALparamDescrsSize (long a0, long a1) |
static native long | INTERNALparamDescrsGetName (long a0, long a1, int a2) |
static native String | INTERNALparamDescrsGetDocumentation (long a0, long a1, long a2) |
static native String | INTERNALparamDescrsToString (long a0, long a1) |
static native long | INTERNALmkIntSymbol (long a0, int a1) |
static native long | INTERNALmkStringSymbol (long a0, String a1) |
static native long | INTERNALmkUninterpretedSort (long a0, long a1) |
static native long | INTERNALmkBoolSort (long a0) |
static native long | INTERNALmkIntSort (long a0) |
static native long | INTERNALmkRealSort (long a0) |
static native long | INTERNALmkBvSort (long a0, int a1) |
static native long | INTERNALmkFiniteDomainSort (long a0, long a1, long a2) |
static native long | INTERNALmkArraySort (long a0, long a1, long a2) |
static native long | INTERNALmkArraySortN (long a0, int a1, long[] a2, long a3) |
static native long | INTERNALmkTupleSort (long a0, long a1, int a2, long[] a3, long[] a4, LongPtr a5, long[] a6) |
static native long | INTERNALmkEnumerationSort (long a0, long a1, int a2, long[] a3, long[] a4, long[] a5) |
static native long | INTERNALmkListSort (long a0, long a1, long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8) |
static native long | INTERNALmkConstructor (long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6) |
static native void | INTERNALdelConstructor (long a0, long a1) |
static native long | INTERNALmkDatatype (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALmkConstructorList (long a0, int a1, long[] a2) |
static native void | INTERNALdelConstructorList (long a0, long a1) |
static native void | INTERNALmkDatatypes (long a0, int a1, long[] a2, long[] a3, long[] a4) |
static native void | INTERNALqueryConstructor (long a0, long a1, int a2, LongPtr a3, LongPtr a4, long[] a5) |
static native long | INTERNALmkFuncDecl (long a0, long a1, int a2, long[] a3, long a4) |
static native long | INTERNALmkApp (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALmkConst (long a0, long a1, long a2) |
static native long | INTERNALmkFreshFuncDecl (long a0, String a1, int a2, long[] a3, long a4) |
static native long | INTERNALmkFreshConst (long a0, String a1, long a2) |
static native long | INTERNALmkRecFuncDecl (long a0, long a1, int a2, long[] a3, long a4) |
static native void | INTERNALaddRecDef (long a0, long a1, int a2, long[] a3, long a4) |
static native long | INTERNALmkTrue (long a0) |
static native long | INTERNALmkFalse (long a0) |
static native long | INTERNALmkEq (long a0, long a1, long a2) |
static native long | INTERNALmkDistinct (long a0, int a1, long[] a2) |
static native long | INTERNALmkNot (long a0, long a1) |
static native long | INTERNALmkIte (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkIff (long a0, long a1, long a2) |
static native long | INTERNALmkImplies (long a0, long a1, long a2) |
static native long | INTERNALmkXor (long a0, long a1, long a2) |
static native long | INTERNALmkAnd (long a0, int a1, long[] a2) |
static native long | INTERNALmkOr (long a0, int a1, long[] a2) |
static native long | INTERNALmkAdd (long a0, int a1, long[] a2) |
static native long | INTERNALmkMul (long a0, int a1, long[] a2) |
static native long | INTERNALmkSub (long a0, int a1, long[] a2) |
static native long | INTERNALmkUnaryMinus (long a0, long a1) |
static native long | INTERNALmkDiv (long a0, long a1, long a2) |
static native long | INTERNALmkMod (long a0, long a1, long a2) |
static native long | INTERNALmkRem (long a0, long a1, long a2) |
static native long | INTERNALmkPower (long a0, long a1, long a2) |
static native long | INTERNALmkLt (long a0, long a1, long a2) |
static native long | INTERNALmkLe (long a0, long a1, long a2) |
static native long | INTERNALmkGt (long a0, long a1, long a2) |
static native long | INTERNALmkGe (long a0, long a1, long a2) |
static native long | 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 long | INTERNALmkLambda (long a0, int a1, long[] a2, long[] a3, long a4) |
static native long | INTERNALmkLambdaConst (long a0, int a1, long[] a2, long a3) |
static native int | INTERNALgetSymbolKind (long a0, long a1) |
static native int | INTERNALgetSymbolInt (long a0, long a1) |
static native String | INTERNALgetSymbolString (long a0, long a1) |
static native long | INTERNALgetSortName (long a0, long a1) |
static native int | INTERNALgetSortId (long a0, long a1) |
static native long | INTERNALsortToAst (long a0, long a1) |
static native boolean | INTERNALisEqSort (long a0, long a1, long a2) |
static native int | INTERNALgetSortKind (long a0, long a1) |
static native int | INTERNALgetBvSortSize (long a0, long a1) |
static native boolean | INTERNALgetFiniteDomainSortSize (long a0, long a1, LongPtr a2) |
static native long | INTERNALgetArraySortDomain (long a0, long a1) |
static native long | INTERNALgetArraySortRange (long a0, long a1) |
static native long | INTERNALgetTupleSortMkDecl (long a0, long a1) |
static native int | INTERNALgetTupleSortNumFields (long a0, long a1) |
static native long | INTERNALgetTupleSortFieldDecl (long a0, long a1, int a2) |
static native int | INTERNALgetDatatypeSortNumConstructors (long a0, long a1) |
static native long | INTERNALgetDatatypeSortConstructor (long a0, long a1, int a2) |
static native long | INTERNALgetDatatypeSortRecognizer (long a0, long a1, int a2) |
static native long | INTERNALgetDatatypeSortConstructorAccessor (long a0, long a1, int a2, int a3) |
static native long | INTERNALdatatypeUpdateField (long a0, long a1, long a2, long a3) |
static native int | INTERNALgetRelationArity (long a0, long a1) |
static native long | INTERNALgetRelationColumn (long a0, long a1, int a2) |
static native long | INTERNALmkAtmost (long a0, int a1, long[] a2, int a3) |
static native long | INTERNALmkAtleast (long a0, int a1, long[] a2, int a3) |
static native long | INTERNALmkPble (long a0, int a1, long[] a2, int[] a3, int a4) |
static native long | INTERNALmkPbge (long a0, int a1, long[] a2, int[] a3, int a4) |
static native long | INTERNALmkPbeq (long a0, int a1, long[] a2, int[] a3, int a4) |
static native long | INTERNALfuncDeclToAst (long a0, long a1) |
static native boolean | INTERNALisEqFuncDecl (long a0, long a1, long a2) |
static native int | INTERNALgetFuncDeclId (long a0, long a1) |
static native long | INTERNALgetDeclName (long a0, long a1) |
static native int | INTERNALgetDeclKind (long a0, long a1) |
static native int | INTERNALgetDomainSize (long a0, long a1) |
static native int | INTERNALgetArity (long a0, long a1) |
static native long | INTERNALgetDomain (long a0, long a1, int a2) |
static native long | INTERNALgetRange (long a0, long a1) |
static native int | INTERNALgetDeclNumParameters (long a0, long a1) |
static native int | INTERNALgetDeclParameterKind (long a0, long a1, int a2) |
static native int | INTERNALgetDeclIntParameter (long a0, long a1, int a2) |
static native double | INTERNALgetDeclDoubleParameter (long a0, long a1, int a2) |
static native long | INTERNALgetDeclSymbolParameter (long a0, long a1, int a2) |
static native long | INTERNALgetDeclSortParameter (long a0, long a1, int a2) |
static native long | INTERNALgetDeclAstParameter (long a0, long a1, int a2) |
static native long | INTERNALgetDeclFuncDeclParameter (long a0, long a1, int a2) |
static native String | INTERNALgetDeclRationalParameter (long a0, long a1, int a2) |
static native long | INTERNALappToAst (long a0, long a1) |
static native long | INTERNALgetAppDecl (long a0, long a1) |
static native int | INTERNALgetAppNumArgs (long a0, long a1) |
static native long | INTERNALgetAppArg (long a0, long a1, int a2) |
static native boolean | INTERNALisEqAst (long a0, long a1, long a2) |
static native int | INTERNALgetAstId (long a0, long a1) |
static native int | INTERNALgetAstHash (long a0, long a1) |
static native long | INTERNALgetSort (long a0, long a1) |
static native boolean | INTERNALisWellSorted (long a0, long a1) |
static native int | INTERNALgetBoolValue (long a0, long a1) |
static native int | INTERNALgetAstKind (long a0, long a1) |
static native boolean | INTERNALisApp (long a0, long a1) |
static native boolean | INTERNALisNumeralAst (long a0, long a1) |
static native boolean | INTERNALisAlgebraicNumber (long a0, long a1) |
static native long | INTERNALtoApp (long a0, long a1) |
static native long | INTERNALtoFuncDecl (long a0, long a1) |
static native String | INTERNALgetNumeralString (long a0, long a1) |
static native String | INTERNALgetNumeralDecimalString (long a0, long a1, int a2) |
static native double | INTERNALgetNumeralDouble (long a0, long a1) |
static native long | INTERNALgetNumerator (long a0, long a1) |
static native long | INTERNALgetDenominator (long a0, long a1) |
static native boolean | INTERNALgetNumeralSmall (long a0, long a1, LongPtr a2, LongPtr a3) |
static native boolean | INTERNALgetNumeralInt (long a0, long a1, IntPtr a2) |
static native boolean | INTERNALgetNumeralUint (long a0, long a1, IntPtr a2) |
static native boolean | INTERNALgetNumeralUint64 (long a0, long a1, LongPtr a2) |
static native boolean | INTERNALgetNumeralInt64 (long a0, long a1, LongPtr a2) |
static native boolean | INTERNALgetNumeralRationalInt64 (long a0, long a1, LongPtr a2, LongPtr a3) |
static native long | INTERNALgetAlgebraicNumberLower (long a0, long a1, int a2) |
static native long | INTERNALgetAlgebraicNumberUpper (long a0, long a1, int a2) |
static native long | INTERNALpatternToAst (long a0, long a1) |
static native int | INTERNALgetPatternNumTerms (long a0, long a1) |
static native long | INTERNALgetPattern (long a0, long a1, int a2) |
static native int | INTERNALgetIndexValue (long a0, long a1) |
static native boolean | INTERNALisQuantifierForall (long a0, long a1) |
static native boolean | INTERNALisQuantifierExists (long a0, long a1) |
static native boolean | INTERNALisLambda (long a0, long a1) |
static native int | INTERNALgetQuantifierWeight (long a0, long a1) |
static native int | INTERNALgetQuantifierNumPatterns (long a0, long a1) |
static native long | INTERNALgetQuantifierPatternAst (long a0, long a1, int a2) |
static native int | INTERNALgetQuantifierNumNoPatterns (long a0, long a1) |
static native long | INTERNALgetQuantifierNoPatternAst (long a0, long a1, int a2) |
static native int | INTERNALgetQuantifierNumBound (long a0, long a1) |
static native long | INTERNALgetQuantifierBoundName (long a0, long a1, int a2) |
static native long | INTERNALgetQuantifierBoundSort (long a0, long a1, int a2) |
static native long | INTERNALgetQuantifierBody (long a0, long a1) |
static native long | INTERNALsimplify (long a0, long a1) |
static native long | INTERNALsimplifyEx (long a0, long a1, long a2) |
static native String | INTERNALsimplifyGetHelp (long a0) |
static native long | INTERNALsimplifyGetParamDescrs (long a0) |
static native long | INTERNALupdateTerm (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALsubstitute (long a0, long a1, int a2, long[] a3, long[] a4) |
static native long | INTERNALsubstituteVars (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALtranslate (long a0, long a1, long a2) |
static native long | INTERNALmkModel (long a0) |
static native void | INTERNALmodelIncRef (long a0, long a1) |
static native void | INTERNALmodelDecRef (long a0, long a1) |
static native boolean | INTERNALmodelEval (long a0, long a1, long a2, boolean a3, LongPtr a4) |
static native long | INTERNALmodelGetConstInterp (long a0, long a1, long a2) |
static native boolean | INTERNALmodelHasInterp (long a0, long a1, long a2) |
static native long | INTERNALmodelGetFuncInterp (long a0, long a1, long a2) |
static native int | INTERNALmodelGetNumConsts (long a0, long a1) |
static native long | INTERNALmodelGetConstDecl (long a0, long a1, int a2) |
static native int | INTERNALmodelGetNumFuncs (long a0, long a1) |
static native long | INTERNALmodelGetFuncDecl (long a0, long a1, int a2) |
static native int | INTERNALmodelGetNumSorts (long a0, long a1) |
static native long | INTERNALmodelGetSort (long a0, long a1, int a2) |
static native long | INTERNALmodelGetSortUniverse (long a0, long a1, long a2) |
static native long | INTERNALmodelTranslate (long a0, long a1, long a2) |
static native boolean | INTERNALisAsArray (long a0, long a1) |
static native long | INTERNALgetAsArrayFuncDecl (long a0, long a1) |
static native long | INTERNALaddFuncInterp (long a0, long a1, long a2, long a3) |
static native void | INTERNALaddConstInterp (long a0, long a1, long a2, long a3) |
static native void | INTERNALfuncInterpIncRef (long a0, long a1) |
static native void | INTERNALfuncInterpDecRef (long a0, long a1) |
static native int | INTERNALfuncInterpGetNumEntries (long a0, long a1) |
static native long | INTERNALfuncInterpGetEntry (long a0, long a1, int a2) |
static native long | INTERNALfuncInterpGetElse (long a0, long a1) |
static native void | INTERNALfuncInterpSetElse (long a0, long a1, long a2) |
static native int | INTERNALfuncInterpGetArity (long a0, long a1) |
static native void | INTERNALfuncInterpAddEntry (long a0, long a1, long a2, long a3) |
static native void | INTERNALfuncEntryIncRef (long a0, long a1) |
static native void | INTERNALfuncEntryDecRef (long a0, long a1) |
static native long | INTERNALfuncEntryGetValue (long a0, long a1) |
static native int | INTERNALfuncEntryGetNumArgs (long a0, long a1) |
static native long | INTERNALfuncEntryGetArg (long a0, long a1, int a2) |
static native int | INTERNALopenLog (String a0) |
static native void | INTERNALappendLog (String a0) |
static native void | INTERNALcloseLog () |
static native void | INTERNALtoggleWarningMessages (boolean a0) |
static native void | INTERNALsetAstPrintMode (long a0, int a1) |
static native String | INTERNALastToString (long a0, long a1) |
static native String | INTERNALpatternToString (long a0, long a1) |
static native String | INTERNALsortToString (long a0, long a1) |
static native String | INTERNALfuncDeclToString (long a0, long a1) |
static native String | INTERNALmodelToString (long a0, long a1) |
static native String | INTERNALbenchmarkToSmtlibString (long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7) |
static native long | INTERNALparseSmtlib2String (long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7) |
static native long | INTERNALparseSmtlib2File (long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7) |
static native String | INTERNALevalSmtlib2String (long a0, String a1) |
static native int | INTERNALgetErrorCode (long a0) |
static native void | INTERNALsetError (long a0, int a1) |
static native String | INTERNALgetErrorMsg (long a0, int a1) |
static native void | INTERNALgetVersion (IntPtr a0, IntPtr a1, IntPtr a2, IntPtr a3) |
static native String | INTERNALgetFullVersion () |
static native void | INTERNALenableTrace (String a0) |
static native void | INTERNALdisableTrace (String a0) |
static native void | INTERNALresetMemory () |
static native void | INTERNALfinalizeMemory () |
static native long | INTERNALmkGoal (long a0, boolean a1, boolean a2, boolean a3) |
static native void | INTERNALgoalIncRef (long a0, long a1) |
static native void | INTERNALgoalDecRef (long a0, long a1) |
static native int | INTERNALgoalPrecision (long a0, long a1) |
static native void | INTERNALgoalAssert (long a0, long a1, long a2) |
static native boolean | INTERNALgoalInconsistent (long a0, long a1) |
static native int | INTERNALgoalDepth (long a0, long a1) |
static native void | INTERNALgoalReset (long a0, long a1) |
static native int | INTERNALgoalSize (long a0, long a1) |
static native long | INTERNALgoalFormula (long a0, long a1, int a2) |
static native int | INTERNALgoalNumExprs (long a0, long a1) |
static native boolean | INTERNALgoalIsDecidedSat (long a0, long a1) |
static native boolean | INTERNALgoalIsDecidedUnsat (long a0, long a1) |
static native long | INTERNALgoalTranslate (long a0, long a1, long a2) |
static native long | INTERNALgoalConvertModel (long a0, long a1, long a2) |
static native String | INTERNALgoalToString (long a0, long a1) |
static native String | INTERNALgoalToDimacsString (long a0, long a1) |
static native long | INTERNALmkTactic (long a0, String a1) |
static native void | INTERNALtacticIncRef (long a0, long a1) |
static native void | INTERNALtacticDecRef (long a0, long a1) |
static native long | INTERNALmkProbe (long a0, String a1) |
static native void | INTERNALprobeIncRef (long a0, long a1) |
static native void | INTERNALprobeDecRef (long a0, long a1) |
static native long | INTERNALtacticAndThen (long a0, long a1, long a2) |
static native long | INTERNALtacticOrElse (long a0, long a1, long a2) |
static native long | INTERNALtacticParOr (long a0, int a1, long[] a2) |
static native long | INTERNALtacticParAndThen (long a0, long a1, long a2) |
static native long | INTERNALtacticTryFor (long a0, long a1, int a2) |
static native long | INTERNALtacticWhen (long a0, long a1, long a2) |
static native long | INTERNALtacticCond (long a0, long a1, long a2, long a3) |
static native long | INTERNALtacticRepeat (long a0, long a1, int a2) |
static native long | INTERNALtacticSkip (long a0) |
static native long | INTERNALtacticFail (long a0) |
static native long | INTERNALtacticFailIf (long a0, long a1) |
static native long | INTERNALtacticFailIfNotDecided (long a0) |
static native long | INTERNALtacticUsingParams (long a0, long a1, long a2) |
static native long | INTERNALprobeConst (long a0, double a1) |
static native long | INTERNALprobeLt (long a0, long a1, long a2) |
static native long | INTERNALprobeGt (long a0, long a1, long a2) |
static native long | INTERNALprobeLe (long a0, long a1, long a2) |
static native long | INTERNALprobeGe (long a0, long a1, long a2) |
static native long | INTERNALprobeEq (long a0, long a1, long a2) |
static native long | INTERNALprobeAnd (long a0, long a1, long a2) |
static native long | INTERNALprobeOr (long a0, long a1, long a2) |
static native long | INTERNALprobeNot (long a0, long a1) |
static native int | INTERNALgetNumTactics (long a0) |
static native String | INTERNALgetTacticName (long a0, int a1) |
static native int | INTERNALgetNumProbes (long a0) |
static native String | INTERNALgetProbeName (long a0, int a1) |
static native String | INTERNALtacticGetHelp (long a0, long a1) |
static native long | INTERNALtacticGetParamDescrs (long a0, long a1) |
static native String | INTERNALtacticGetDescr (long a0, String a1) |
static native String | INTERNALprobeGetDescr (long a0, String a1) |
static native double | INTERNALprobeApply (long a0, long a1, long a2) |
static native long | INTERNALtacticApply (long a0, long a1, long a2) |
static native long | INTERNALtacticApplyEx (long a0, long a1, long a2, long a3) |
static native void | INTERNALapplyResultIncRef (long a0, long a1) |
static native void | INTERNALapplyResultDecRef (long a0, long a1) |
static native String | INTERNALapplyResultToString (long a0, long a1) |
static native int | INTERNALapplyResultGetNumSubgoals (long a0, long a1) |
static native long | INTERNALapplyResultGetSubgoal (long a0, long a1, int a2) |
static native long | INTERNALmkSolver (long a0) |
static native long | INTERNALmkSimpleSolver (long a0) |
static native long | INTERNALmkSolverForLogic (long a0, long a1) |
static native long | INTERNALmkSolverFromTactic (long a0, long a1) |
static native long | INTERNALsolverTranslate (long a0, long a1, long a2) |
static native void | INTERNALsolverImportModelConverter (long a0, long a1, long a2) |
static native String | INTERNALsolverGetHelp (long a0, long a1) |
static native long | INTERNALsolverGetParamDescrs (long a0, long a1) |
static native void | INTERNALsolverSetParams (long a0, long a1, long a2) |
static native void | INTERNALsolverIncRef (long a0, long a1) |
static native void | INTERNALsolverDecRef (long a0, long a1) |
static native void | INTERNALsolverPush (long a0, long a1) |
static native void | INTERNALsolverPop (long a0, long a1, int a2) |
static native void | INTERNALsolverReset (long a0, long a1) |
static native int | INTERNALsolverGetNumScopes (long a0, long a1) |
static native void | INTERNALsolverAssert (long a0, long a1, long a2) |
static native void | INTERNALsolverAssertAndTrack (long a0, long a1, long a2, long a3) |
static native void | INTERNALsolverFromFile (long a0, long a1, String a2) |
static native void | INTERNALsolverFromString (long a0, long a1, String a2) |
static native long | INTERNALsolverGetAssertions (long a0, long a1) |
static native long | INTERNALsolverGetUnits (long a0, long a1) |
static native long | INTERNALsolverGetNonUnits (long a0, long a1) |
static native int | INTERNALsolverCheck (long a0, long a1) |
static native int | INTERNALsolverCheckAssumptions (long a0, long a1, int a2, long[] a3) |
static native int | INTERNALgetImpliedEqualities (long a0, long a1, int a2, long[] a3, int[] a4) |
static native int | INTERNALsolverGetConsequences (long a0, long a1, long a2, long a3, long a4) |
static native long | INTERNALsolverCube (long a0, long a1, long a2, int a3) |
static native long | INTERNALsolverGetModel (long a0, long a1) |
static native long | INTERNALsolverGetProof (long a0, long a1) |
static native long | INTERNALsolverGetUnsatCore (long a0, long a1) |
static native String | INTERNALsolverGetReasonUnknown (long a0, long a1) |
static native long | INTERNALsolverGetStatistics (long a0, long a1) |
static native String | INTERNALsolverToString (long a0, long a1) |
static native String | 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, int a2, long[] a3) |
static native String | INTERNALoptimizeGetReasonUnknown (long a0, long a1) |
static native long | INTERNALoptimizeGetModel (long a0, long a1) |
static native long | INTERNALoptimizeGetUnsatCore (long a0, long a1) |
static native void | INTERNALoptimizeSetParams (long a0, long a1, long a2) |
static native long | INTERNALoptimizeGetParamDescrs (long a0, long a1) |
static native long | INTERNALoptimizeGetLower (long a0, long a1, int a2) |
static native long | INTERNALoptimizeGetUpper (long a0, long a1, int a2) |
static native long | INTERNALoptimizeGetLowerAsVector (long a0, long a1, int a2) |
static native long | INTERNALoptimizeGetUpperAsVector (long a0, long a1, int a2) |
static native String | INTERNALoptimizeToString (long a0, long a1) |
static native void | INTERNALoptimizeFromString (long a0, long a1, String a2) |
static native void | INTERNALoptimizeFromFile (long a0, long a1, String a2) |
static native String | INTERNALoptimizeGetHelp (long a0, long a1) |
static native long | INTERNALoptimizeGetStatistics (long a0, long a1) |
static native long | INTERNALoptimizeGetAssertions (long a0, long a1) |
static native long | INTERNALoptimizeGetObjectives (long a0, long a1) |
static native long | INTERNALmkFpaRoundingModeSort (long a0) |
static native long | INTERNALmkFpaRoundNearestTiesToEven (long a0) |
static native long | INTERNALmkFpaRne (long a0) |
static native long | INTERNALmkFpaRoundNearestTiesToAway (long a0) |
static native long | INTERNALmkFpaRna (long a0) |
static native long | INTERNALmkFpaRoundTowardPositive (long a0) |
static native long | INTERNALmkFpaRtp (long a0) |
static native long | INTERNALmkFpaRoundTowardNegative (long a0) |
static native long | INTERNALmkFpaRtn (long a0) |
static native long | INTERNALmkFpaRoundTowardZero (long a0) |
static native long | INTERNALmkFpaRtz (long a0) |
static native long | INTERNALmkFpaSort (long a0, int a1, int a2) |
static native long | INTERNALmkFpaSortHalf (long a0) |
static native long | INTERNALmkFpaSort16 (long a0) |
static native long | INTERNALmkFpaSortSingle (long a0) |
static native long | INTERNALmkFpaSort32 (long a0) |
static native long | INTERNALmkFpaSortDouble (long a0) |
static native long | INTERNALmkFpaSort64 (long a0) |
static native long | INTERNALmkFpaSortQuadruple (long a0) |
static native long | INTERNALmkFpaSort128 (long a0) |
static native long | INTERNALmkFpaNan (long a0, long a1) |
static native long | INTERNALmkFpaInf (long a0, long a1, boolean a2) |
static native long | INTERNALmkFpaZero (long a0, long a1, boolean a2) |
static native long | INTERNALmkFpaFp (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaNumeralFloat (long a0, float a1, long a2) |
static native long | INTERNALmkFpaNumeralDouble (long a0, double a1, long a2) |
static native long | INTERNALmkFpaNumeralInt (long a0, int a1, long a2) |
static native long | INTERNALmkFpaNumeralIntUint (long a0, boolean a1, int a2, int a3, long a4) |
static native long | INTERNALmkFpaNumeralInt64Uint64 (long a0, boolean a1, long a2, long a3, long a4) |
static native long | INTERNALmkFpaAbs (long a0, long a1) |
static native long | INTERNALmkFpaNeg (long a0, long a1) |
static native long | INTERNALmkFpaAdd (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaSub (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaMul (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaDiv (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaFma (long a0, long a1, long a2, long a3, long a4) |
static native long | INTERNALmkFpaSqrt (long a0, long a1, long a2) |
static native long | INTERNALmkFpaRem (long a0, long a1, long a2) |
static native long | INTERNALmkFpaRoundToIntegral (long a0, long a1, long a2) |
static native long | INTERNALmkFpaMin (long a0, long a1, long a2) |
static native long | INTERNALmkFpaMax (long a0, long a1, long a2) |
static native long | INTERNALmkFpaLeq (long a0, long a1, long a2) |
static native long | INTERNALmkFpaLt (long a0, long a1, long a2) |
static native long | INTERNALmkFpaGeq (long a0, long a1, long a2) |
static native long | INTERNALmkFpaGt (long a0, long a1, long a2) |
static native long | INTERNALmkFpaEq (long a0, long a1, long a2) |
static native long | INTERNALmkFpaIsNormal (long a0, long a1) |
static native long | INTERNALmkFpaIsSubnormal (long a0, long a1) |
static native long | INTERNALmkFpaIsZero (long a0, long a1) |
static native long | INTERNALmkFpaIsInfinite (long a0, long a1) |
static native long | INTERNALmkFpaIsNan (long a0, long a1) |
static native long | INTERNALmkFpaIsNegative (long a0, long a1) |
static native long | INTERNALmkFpaIsPositive (long a0, long a1) |
static native long | INTERNALmkFpaToFpBv (long a0, long a1, long a2) |
static native long | INTERNALmkFpaToFpFloat (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaToFpReal (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaToFpSigned (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaToFpUnsigned (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaToUbv (long a0, long a1, long a2, int a3) |
static native long | INTERNALmkFpaToSbv (long a0, long a1, long a2, int a3) |
static native long | INTERNALmkFpaToReal (long a0, long a1) |
static native int | INTERNALfpaGetEbits (long a0, long a1) |
static native int | INTERNALfpaGetSbits (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralNan (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralInf (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralZero (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralNormal (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralSubnormal (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralPositive (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralNegative (long a0, long a1) |
static native long | INTERNALfpaGetNumeralSignBv (long a0, long a1) |
static native long | INTERNALfpaGetNumeralSignificandBv (long a0, long a1) |
static native boolean | INTERNALfpaGetNumeralSign (long a0, long a1, IntPtr a2) |
static native String | INTERNALfpaGetNumeralSignificandString (long a0, long a1) |
static native boolean | INTERNALfpaGetNumeralSignificandUint64 (long a0, long a1, LongPtr a2) |
static native String | INTERNALfpaGetNumeralExponentString (long a0, long a1, boolean a2) |
static native boolean | INTERNALfpaGetNumeralExponentInt64 (long a0, long a1, LongPtr a2, boolean a3) |
static native long | INTERNALfpaGetNumeralExponentBv (long a0, long a1, boolean a2) |
static native long | INTERNALmkFpaToIeeeBv (long a0, long a1) |
static native long | INTERNALmkFpaToFpIntReal (long a0, long a1, long a2, long a3, long a4) |
static native int | INTERNALfixedpointQueryFromLvl (long a0, long a1, long a2, int a3) |
static native long | INTERNALfixedpointGetGroundSatAnswer (long a0, long a1) |
static native long | INTERNALfixedpointGetRulesAlongTrace (long a0, long a1) |
static native long | INTERNALfixedpointGetRuleNamesAlongTrace (long a0, long a1) |
static native void | INTERNALfixedpointAddInvariant (long a0, long a1, long a2, long a3) |
static native long | INTERNALfixedpointGetReachable (long a0, long a1, long a2) |
static native long | INTERNALqeModelProject (long a0, long a1, int a2, long[] a3, long a4) |
static native long | INTERNALqeModelProjectSkolem (long a0, long a1, int a2, long[] a3, long a4, long a5) |
static native long | INTERNALmodelExtrapolate (long a0, long a1, long a2) |
static native long | INTERNALqeLite (long a0, long a1, long a2) |
Definition at line 4 of file Native.java.
|
inlinestatic |
Definition at line 3519 of file Native.java.
|
inlinestatic |
Definition at line 3510 of file Native.java.
|
inlinestatic |
Definition at line 1137 of file Native.java.
|
inlinestatic |
Definition at line 4936 of file Native.java.
|
inlinestatic |
Definition at line 4963 of file Native.java.
|
inlinestatic |
Definition at line 5026 of file Native.java.
|
inlinestatic |
Definition at line 5053 of file Native.java.
|
inlinestatic |
Definition at line 5017 of file Native.java.
|
inlinestatic |
Definition at line 4999 of file Native.java.
|
inlinestatic |
Definition at line 4909 of file Native.java.
|
inlinestatic |
Definition at line 4900 of file Native.java.
|
inlinestatic |
Definition at line 4891 of file Native.java.
|
inlinestatic |
Definition at line 4918 of file Native.java.
|
inlinestatic |
Definition at line 5008 of file Native.java.
|
inlinestatic |
Definition at line 4990 of file Native.java.
|
inlinestatic |
Definition at line 4954 of file Native.java.
|
inlinestatic |
Definition at line 5035 of file Native.java.
|
inlinestatic |
Definition at line 4981 of file Native.java.
|
inlinestatic |
Definition at line 4972 of file Native.java.
|
inlinestatic |
Definition at line 5044 of file Native.java.
|
inlinestatic |
Definition at line 4927 of file Native.java.
|
inlinestatic |
Definition at line 4945 of file Native.java.
|
inlinestatic |
Definition at line 3644 of file Native.java.
Referenced by Log.append().
|
inlinestatic |
Definition at line 4306 of file Native.java.
|
inlinestatic |
Definition at line 4323 of file Native.java.
Referenced by ApplyResult.getNumSubgoals().
|
inlinestatic |
Definition at line 4332 of file Native.java.
Referenced by ApplyResult.getSubgoals().
|
inlinestatic |
Definition at line 4298 of file Native.java.
|
inlinestatic |
Definition at line 4314 of file Native.java.
Referenced by ApplyResult.toString().
|
inlinestatic |
Definition at line 2882 of file Native.java.
|
inlinestatic |
Definition at line 4822 of file Native.java.
|
inlinestatic |
Definition at line 4814 of file Native.java.
|
inlinestatic |
Definition at line 4848 of file Native.java.
|
inlinestatic |
Definition at line 4831 of file Native.java.
|
inlinestatic |
Definition at line 4806 of file Native.java.
|
inlinestatic |
Definition at line 4840 of file Native.java.
|
inlinestatic |
Definition at line 4873 of file Native.java.
|
inlinestatic |
Definition at line 4856 of file Native.java.
|
inlinestatic |
Definition at line 4864 of file Native.java.
|
inlinestatic |
Definition at line 4882 of file Native.java.
|
inlinestatic |
Definition at line 3667 of file Native.java.
Referenced by AST.getSExpr(), and AST.toString().
|
inlinestatic |
Definition at line 4729 of file Native.java.
|
inlinestatic |
Definition at line 4746 of file Native.java.
Referenced by ASTVector.get().
|
inlinestatic |
Definition at line 4721 of file Native.java.
|
inlinestatic |
Definition at line 4771 of file Native.java.
Referenced by ASTVector.push().
|
inlinestatic |
Definition at line 4763 of file Native.java.
Referenced by ASTVector.resize().
|
inlinestatic |
Definition at line 4755 of file Native.java.
Referenced by ASTVector.set().
|
inlinestatic |
Definition at line 4737 of file Native.java.
Referenced by ASTVector.size().
|
inlinestatic |
Definition at line 4788 of file Native.java.
Referenced by ASTVector.toString().
|
inlinestatic |
Definition at line 4779 of file Native.java.
Referenced by ASTVector.translate().
|
inlinestatic |
Definition at line 3712 of file Native.java.
Referenced by Context.benchmarkToSMTString().
|
inlinestatic |
Definition at line 3649 of file Native.java.
Referenced by Log.close().
|
inlinestatic |
Definition at line 2648 of file Native.java.
Referenced by Context.mkUpdateField().
|
inlinestatic |
Definition at line 748 of file Native.java.
|
inlinestatic |
Definition at line 709 of file Native.java.
Referenced by Context.Context().
|
inlinestatic |
Definition at line 1033 of file Native.java.
Referenced by ConstructorDecRefQueue.decRef().
|
inlinestatic |
Definition at line 1059 of file Native.java.
Referenced by ConstructorListDecRefQueue.decRef().
|
inlinestatic |
Definition at line 735 of file Native.java.
Referenced by Context.close().
|
inlinestatic |
Definition at line 3787 of file Native.java.
Referenced by Global.disableTrace().
|
inlinestatic |
Definition at line 3782 of file Native.java.
Referenced by Global.enableTrace().
|
inlinestatic |
Definition at line 3739 of file Native.java.
|
inlinestatic |
Definition at line 3797 of file Native.java.
|
inlinestatic |
Definition at line 5387 of file Native.java.
Referenced by Fixedpoint.addCover().
|
inlinestatic |
Definition at line 5309 of file Native.java.
Referenced by Fixedpoint.addFact().
|
inlinestatic |
Definition at line 6489 of file Native.java.
|
inlinestatic |
Definition at line 5301 of file Native.java.
Referenced by Fixedpoint.addRule().
|
inlinestatic |
Definition at line 5317 of file Native.java.
Referenced by Fixedpoint.add().
|
inlinestatic |
Definition at line 5293 of file Native.java.
|
inlinestatic |
Definition at line 5482 of file Native.java.
Referenced by Fixedpoint.ParseFile().
|
inlinestatic |
Definition at line 5473 of file Native.java.
Referenced by Fixedpoint.ParseString().
|
inlinestatic |
Definition at line 5343 of file Native.java.
Referenced by Fixedpoint.getAnswer().
|
inlinestatic |
Definition at line 5429 of file Native.java.
Referenced by Fixedpoint.getAssertions().
|
inlinestatic |
Definition at line 5378 of file Native.java.
Referenced by Fixedpoint.getCoverDelta().
|
inlinestatic |
Definition at line 6462 of file Native.java.
|
inlinestatic |
Definition at line 5446 of file Native.java.
Referenced by Fixedpoint.getHelp().
|
inlinestatic |
Definition at line 5369 of file Native.java.
Referenced by Fixedpoint.getNumLevels().
|
inlinestatic |
Definition at line 5455 of file Native.java.
Referenced by Fixedpoint.getParameterDescriptions().
|
inlinestatic |
Definition at line 6497 of file Native.java.
|
inlinestatic |
Definition at line 5352 of file Native.java.
Referenced by Fixedpoint.getReasonUnknown().
|
inlinestatic |
Definition at line 6480 of file Native.java.
|
inlinestatic |
Definition at line 5420 of file Native.java.
Referenced by Fixedpoint.getRules().
|
inlinestatic |
Definition at line 6471 of file Native.java.
|
inlinestatic |
Definition at line 5395 of file Native.java.
Referenced by Fixedpoint.getStatistics().
|
inlinestatic |
Definition at line 5285 of file Native.java.
|
inlinestatic |
Definition at line 5499 of file Native.java.
Referenced by Fixedpoint.pop().
|
inlinestatic |
Definition at line 5491 of file Native.java.
Referenced by Fixedpoint.push().
|
inlinestatic |
Definition at line 5325 of file Native.java.
Referenced by Fixedpoint.query().
|
inlinestatic |
Definition at line 6453 of file Native.java.
|
inlinestatic |
Definition at line 5334 of file Native.java.
Referenced by Fixedpoint.query().
|
inlinestatic |
Definition at line 5404 of file Native.java.
Referenced by Fixedpoint.registerRelation().
|
inlinestatic |
Definition at line 5438 of file Native.java.
Referenced by Fixedpoint.setParameters().
|
inlinestatic |
Definition at line 5412 of file Native.java.
Referenced by Fixedpoint.setPredicateRepresentation().
|
inlinestatic |
Definition at line 5464 of file Native.java.
Referenced by Fixedpoint.toString().
|
inlinestatic |
Definition at line 5361 of file Native.java.
Referenced by Fixedpoint.updateRule().
|
inlinestatic |
Definition at line 6282 of file Native.java.
Referenced by FPSort.getEBits().
|
inlinestatic |
Definition at line 6426 of file Native.java.
Referenced by FPNum.getExponentBV().
|
inlinestatic |
Definition at line 6417 of file Native.java.
Referenced by FPNum.getExponentInt64().
|
inlinestatic |
Definition at line 6408 of file Native.java.
Referenced by FPNum.getExponent().
|
inlinestatic |
Definition at line 6381 of file Native.java.
Referenced by FPNum.getSign().
|
inlinestatic |
Definition at line 6363 of file Native.java.
Referenced by FPNum.getSignBV().
|
inlinestatic |
Definition at line 6372 of file Native.java.
Referenced by FPNum.getSignificandBV().
|
inlinestatic |
Definition at line 6390 of file Native.java.
Referenced by FPNum.getSignificand().
|
inlinestatic |
Definition at line 6399 of file Native.java.
Referenced by FPNum.getSignificandUInt64().
|
inlinestatic |
Definition at line 6291 of file Native.java.
Referenced by FPSort.getSBits().
|
inlinestatic |
Definition at line 6309 of file Native.java.
Referenced by FPNum.isInf().
|
inlinestatic |
Definition at line 6300 of file Native.java.
Referenced by FPNum.isNaN().
|
inlinestatic |
Definition at line 6354 of file Native.java.
Referenced by FPNum.isNegative().
|
inlinestatic |
Definition at line 6327 of file Native.java.
Referenced by FPNum.isNormal().
|
inlinestatic |
Definition at line 6345 of file Native.java.
Referenced by FPNum.isPositive().
|
inlinestatic |
Definition at line 6336 of file Native.java.
Referenced by FPNum.isSubnormal().
|
inlinestatic |
Definition at line 6318 of file Native.java.
Referenced by FPNum.isZero().
|
inlinestatic |
Definition at line 2720 of file Native.java.
|
inlinestatic |
Definition at line 3694 of file Native.java.
Referenced by FuncDecl.toString().
|
inlinestatic |
Definition at line 3603 of file Native.java.
|
inlinestatic |
Definition at line 3629 of file Native.java.
|
inlinestatic |
Definition at line 3620 of file Native.java.
|
inlinestatic |
Definition at line 3611 of file Native.java.
|
inlinestatic |
Definition at line 3595 of file Native.java.
|
inlinestatic |
Definition at line 3587 of file Native.java.
|
inlinestatic |
Definition at line 3535 of file Native.java.
|
inlinestatic |
Definition at line 3578 of file Native.java.
Referenced by FuncInterp.getArity().
|
inlinestatic |
Definition at line 3561 of file Native.java.
Referenced by FuncInterp.getElse().
|
inlinestatic |
Definition at line 3552 of file Native.java.
Referenced by FuncInterp.getEntries().
|
inlinestatic |
Definition at line 3543 of file Native.java.
Referenced by FuncInterp.getNumEntries().
|
inlinestatic |
Definition at line 3527 of file Native.java.
|
inlinestatic |
Definition at line 3570 of file Native.java.
|
inlinestatic |
Definition at line 3125 of file Native.java.
Referenced by AlgebraicNum.toLower().
|
inlinestatic |
Definition at line 3134 of file Native.java.
Referenced by AlgebraicNum.toUpper().
|
inlinestatic |
Definition at line 2909 of file Native.java.
Referenced by Expr.getArgs().
|
inlinestatic |
Definition at line 2891 of file Native.java.
Referenced by Expr.getFuncDecl().
|
inlinestatic |
Definition at line 2900 of file Native.java.
Referenced by Expr.getNumArgs().
|
inlinestatic |
Definition at line 2774 of file Native.java.
Referenced by FuncDecl.getArity().
|
inlinestatic |
Definition at line 2567 of file Native.java.
Referenced by ArraySort.getDomain().
|
inlinestatic |
Definition at line 2576 of file Native.java.
Referenced by ArraySort.getRange().
|
inlinestatic |
Definition at line 3501 of file Native.java.
Referenced by Model.getFuncInterp().
|
inlinestatic |
Definition at line 2936 of file Native.java.
Referenced by AST.hashCode().
|
inlinestatic |
Definition at line 2927 of file Native.java.
Referenced by AST.getId().
|
inlinestatic |
Definition at line 2972 of file Native.java.
Referenced by AST.getASTKind().
|
inlinestatic |
Definition at line 2963 of file Native.java.
Referenced by Expr.getBoolValue().
|
inlinestatic |
Definition at line 2549 of file Native.java.
Referenced by BitVecSort.getSize().
|
inlinestatic |
Definition at line 2621 of file Native.java.
Referenced by DatatypeSort.getAccessors(), ListSort.getConsDecl(), EnumSort.getConstDecl(), EnumSort.getConstDecls(), DatatypeSort.getConstructors(), and ListSort.getNilDecl().
|
inlinestatic |
Definition at line 2639 of file Native.java.
Referenced by DatatypeSort.getAccessors(), ListSort.getHeadDecl(), and ListSort.getTailDecl().
|
inlinestatic |
Definition at line 2612 of file Native.java.
Referenced by EnumSort.getConstDecls(), DatatypeSort.getNumConstructors(), and EnumSort.getTesterDecls().
|
inlinestatic |
Definition at line 2630 of file Native.java.
Referenced by ListSort.getIsConsDecl(), ListSort.getIsNilDecl(), DatatypeSort.getRecognizers(), EnumSort.getTesterDecl(), and EnumSort.getTesterDecls().
|
inlinestatic |
Definition at line 2855 of file Native.java.
Referenced by FuncDecl.getParameters().
|
inlinestatic |
Definition at line 2828 of file Native.java.
Referenced by FuncDecl.getParameters().
|
inlinestatic |
Definition at line 2864 of file Native.java.
Referenced by FuncDecl.getParameters().
|
inlinestatic |
Definition at line 2819 of file Native.java.
Referenced by FuncDecl.getParameters().
|
inlinestatic |
Definition at line 2756 of file Native.java.
Referenced by FuncDecl.getDeclKind().
|
inlinestatic |
Definition at line 2747 of file Native.java.
Referenced by FuncDecl.getName().
|
inlinestatic |
Definition at line 2801 of file Native.java.
Referenced by FuncDecl.getNumParameters().
|
inlinestatic |
Definition at line 2810 of file Native.java.
|
inlinestatic |
Definition at line 2873 of file Native.java.
Referenced by FuncDecl.getParameters().
|
inlinestatic |
Definition at line 2846 of file Native.java.
|
inlinestatic |
Definition at line 2837 of file Native.java.
|
inlinestatic |
Definition at line 3062 of file Native.java.
Referenced by RatNum.getDenominator().
|
inlinestatic |
Definition at line 2783 of file Native.java.
Referenced by FuncDecl.getDomain().
|
inlinestatic |
Definition at line 2765 of file Native.java.
Referenced by FuncDecl.getDomainSize().
|
inlinestatic |
Definition at line 3748 of file Native.java.
|
inlinestatic |
Definition at line 3762 of file Native.java.
|
inlinestatic |
Definition at line 4706 of file Native.java.
|
inlinestatic |
Definition at line 2558 of file Native.java.
Referenced by FiniteDomainSort.getSize().
|
inlinestatic |
Definition at line 3776 of file Native.java.
Referenced by Version.getFullVersion().
|
inlinestatic |
Definition at line 2738 of file Native.java.
Referenced by FuncDecl.getId().
|
inlinestatic |
Definition at line 4546 of file Native.java.
|
inlinestatic |
Definition at line 3170 of file Native.java.
Referenced by Expr.getIndex().
|
inlinestatic |
Definition at line 3035 of file Native.java.
Referenced by AlgebraicNum.toDecimal(), and RatNum.toDecimalString().
|
inlinestatic |
Definition at line 3044 of file Native.java.
|
inlinestatic |
Definition at line 3080 of file Native.java.
Referenced by BitVecNum.getInt(), IntNum.getInt(), and FiniteDomainNum.getInt().
|
inlinestatic |
Definition at line 3107 of file Native.java.
Referenced by IntNum.getInt64(), FiniteDomainNum.getInt64(), and BitVecNum.getLong().
|
inlinestatic |
Definition at line 3116 of file Native.java.
|
inlinestatic |
Definition at line 3071 of file Native.java.
|
inlinestatic |
Definition at line 3026 of file Native.java.
Referenced by IntNum.toString(), BitVecNum.toString(), FiniteDomainNum.toString(), RatNum.toString(), and FPNum.toString().
|
inlinestatic |
Definition at line 3089 of file Native.java.
|
inlinestatic |
Definition at line 3098 of file Native.java.
|
inlinestatic |
Definition at line 3053 of file Native.java.
Referenced by RatNum.getNumerator().
|
inlinestatic |
Definition at line 4217 of file Native.java.
Referenced by Context.getNumProbes().
|
inlinestatic |
Definition at line 4199 of file Native.java.
Referenced by Context.getNumTactics().
|
inlinestatic |
Definition at line 3161 of file Native.java.
Referenced by Pattern.getTerms().
|
inlinestatic |
Definition at line 3152 of file Native.java.
Referenced by Pattern.getNumTerms().
|
inlinestatic |
Definition at line 4226 of file Native.java.
Referenced by Context.getProbeNames().
|
inlinestatic |
Definition at line 3278 of file Native.java.
Referenced by Lambda.getBody(), and Quantifier.getBody().
|
inlinestatic |
Definition at line 3260 of file Native.java.
Referenced by Lambda.getBoundVariableNames(), and Quantifier.getBoundVariableNames().
|
inlinestatic |
Definition at line 3269 of file Native.java.
Referenced by Lambda.getBoundVariableSorts(), and Quantifier.getBoundVariableSorts().
|
inlinestatic |
Definition at line 3242 of file Native.java.
Referenced by Quantifier.getNoPatterns().
|
inlinestatic |
Definition at line 3251 of file Native.java.
Referenced by Lambda.getNumBound(), and Quantifier.getNumBound().
|
inlinestatic |
Definition at line 3233 of file Native.java.
Referenced by Quantifier.getNumNoPatterns().
|
inlinestatic |
Definition at line 3215 of file Native.java.
Referenced by Quantifier.getNumPatterns().
|
inlinestatic |
Definition at line 3224 of file Native.java.
Referenced by Quantifier.getPatterns().
|
inlinestatic |
Definition at line 3206 of file Native.java.
Referenced by Quantifier.getWeight().
|
inlinestatic |
Definition at line 2792 of file Native.java.
Referenced by Model.getConstInterp(), Model.getFuncInterp(), and FuncDecl.getRange().
|
inlinestatic |
Definition at line 2657 of file Native.java.
Referenced by RelationSort.getArity().
|
inlinestatic |
Definition at line 2666 of file Native.java.
Referenced by RelationSort.getColumnSorts().
|
inlinestatic |
Definition at line 2945 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 2513 of file Native.java.
Referenced by Sort.getId().
|
inlinestatic |
Definition at line 2540 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 2504 of file Native.java.
Referenced by Sort.getName().
|
inlinestatic |
Definition at line 2126 of file Native.java.
Referenced by Expr.getString().
|
inlinestatic |
Definition at line 2486 of file Native.java.
Referenced by IntSymbol.getInt().
|
inlinestatic |
Definition at line 2477 of file Native.java.
Referenced by Symbol.getKind().
|
inlinestatic |
Definition at line 2495 of file Native.java.
Referenced by StringSymbol.getString().
|
inlinestatic |
Definition at line 4208 of file Native.java.
Referenced by Context.getTacticNames().
|
inlinestatic |
Definition at line 2603 of file Native.java.
Referenced by TupleSort.getFieldDecls().
|
inlinestatic |
Definition at line 2585 of file Native.java.
Referenced by TupleSort.mkDecl().
|
inlinestatic |
Definition at line 2594 of file Native.java.
Referenced by TupleSort.getNumFields().
|
inlinestatic |
Definition at line 3771 of file Native.java.
Referenced by Version.getBuild(), Version.getMajor(), Version.getMinor(), Version.getRevision(), and Version.getString().
|
inlinestatic |
Definition at line 697 of file Native.java.
Referenced by Global.getParameter().
|
inlinestatic |
Definition at line 692 of file Native.java.
Referenced by Global.resetParameters().
|
inlinestatic |
Definition at line 687 of file Native.java.
Referenced by Global.setParameter().
|
inlinestatic |
Definition at line 3836 of file Native.java.
Referenced by Goal.add().
|
inlinestatic |
Definition at line 3924 of file Native.java.
Referenced by Goal.convertModel().
|
inlinestatic |
Definition at line 3819 of file Native.java.
|
inlinestatic |
Definition at line 3853 of file Native.java.
Referenced by Goal.getDepth().
|
inlinestatic |
Definition at line 3879 of file Native.java.
Referenced by Goal.getFormulas().
|
inlinestatic |
Definition at line 3844 of file Native.java.
Referenced by Goal.inconsistent().
|
inlinestatic |
Definition at line 3811 of file Native.java.
|
inlinestatic |
Definition at line 3897 of file Native.java.
Referenced by Goal.isDecidedSat().
|
inlinestatic |
Definition at line 3906 of file Native.java.
Referenced by Goal.isDecidedUnsat().
|
inlinestatic |
Definition at line 3888 of file Native.java.
Referenced by Goal.getNumExprs().
|
inlinestatic |
Definition at line 3827 of file Native.java.
Referenced by Goal.getPrecision().
|
inlinestatic |
Definition at line 3862 of file Native.java.
Referenced by Goal.reset().
|
inlinestatic |
Definition at line 3870 of file Native.java.
Referenced by Goal.size().
|
inlinestatic |
Definition at line 3942 of file Native.java.
|
inlinestatic |
Definition at line 3933 of file Native.java.
Referenced by Goal.toString().
|
inlinestatic |
Definition at line 3915 of file Native.java.
Referenced by Goal.translate().
|
inlinestatic |
Definition at line 740 of file Native.java.
|
staticprotected |
Referenced by Native.addConstInterp().
|
staticprotected |
Referenced by Native.addFuncInterp().
|
staticprotected |
Referenced by Native.addRecDef().
|
staticprotected |
Referenced by Native.algebraicAdd().
|
staticprotected |
Referenced by Native.algebraicDiv().
|
staticprotected |
Referenced by Native.algebraicEq().
|
staticprotected |
Referenced by Native.algebraicEval().
|
staticprotected |
Referenced by Native.algebraicGe().
|
staticprotected |
Referenced by Native.algebraicGt().
|
staticprotected |
Referenced by Native.algebraicIsNeg().
|
staticprotected |
Referenced by Native.algebraicIsPos().
|
staticprotected |
Referenced by Native.algebraicIsValue().
|
staticprotected |
Referenced by Native.algebraicIsZero().
|
staticprotected |
Referenced by Native.algebraicLe().
|
staticprotected |
Referenced by Native.algebraicLt().
|
staticprotected |
Referenced by Native.algebraicMul().
|
staticprotected |
Referenced by Native.algebraicNeq().
|
staticprotected |
Referenced by Native.algebraicPower().
|
staticprotected |
Referenced by Native.algebraicRoot().
|
staticprotected |
Referenced by Native.algebraicRoots().
|
staticprotected |
Referenced by Native.algebraicSign().
|
staticprotected |
Referenced by Native.algebraicSub().
|
staticprotected |
Referenced by Native.appendLog().
|
staticprotected |
Referenced by Native.applyResultDecRef().
|
staticprotected |
Referenced by Native.applyResultGetNumSubgoals().
|
staticprotected |
Referenced by Native.applyResultGetSubgoal().
|
staticprotected |
Referenced by Native.applyResultIncRef().
|
staticprotected |
Referenced by Native.applyResultToString().
|
staticprotected |
Referenced by Native.appToAst().
|
staticprotected |
Referenced by Native.astMapContains().
|
staticprotected |
Referenced by Native.astMapDecRef().
|
staticprotected |
Referenced by Native.astMapErase().
|
staticprotected |
Referenced by Native.astMapFind().
|
staticprotected |
Referenced by Native.astMapIncRef().
|
staticprotected |
Referenced by Native.astMapInsert().
|
staticprotected |
Referenced by Native.astMapKeys().
|
staticprotected |
Referenced by Native.astMapReset().
|
staticprotected |
Referenced by Native.astMapSize().
|
staticprotected |
Referenced by Native.astMapToString().
|
staticprotected |
Referenced by Native.astToString().
|
staticprotected |
Referenced by Native.astVectorDecRef().
|
staticprotected |
Referenced by Native.astVectorGet().
|
staticprotected |
Referenced by Native.astVectorIncRef().
|
staticprotected |
Referenced by Native.astVectorPush().
|
staticprotected |
Referenced by Native.astVectorResize().
|
staticprotected |
Referenced by Native.astVectorSet().
|
staticprotected |
Referenced by Native.astVectorSize().
|
staticprotected |
Referenced by Native.astVectorToString().
|
staticprotected |
Referenced by Native.astVectorTranslate().
|
staticprotected |
Referenced by Native.benchmarkToSmtlibString().
|
staticprotected |
Referenced by Native.closeLog().
|
staticprotected |
Referenced by Native.datatypeUpdateField().
|
staticprotected |
Referenced by Native.decRef().
|
staticprotected |
Referenced by Native.delConfig().
|
staticprotected |
Referenced by Native.delConstructor().
|
staticprotected |
Referenced by Native.delConstructorList().
|
staticprotected |
Referenced by Native.delContext().
|
staticprotected |
Referenced by Native.disableTrace().
|
staticprotected |
Referenced by Native.enableTrace().
|
staticprotected |
Referenced by Native.evalSmtlib2String().
|
staticprotected |
Referenced by Native.finalizeMemory().
|
staticprotected |
Referenced by Native.fixedpointAddCover().
|
staticprotected |
Referenced by Native.fixedpointAddFact().
|
staticprotected |
Referenced by Native.fixedpointAddInvariant().
|
staticprotected |
Referenced by Native.fixedpointAddRule().
|
staticprotected |
Referenced by Native.fixedpointAssert().
|
staticprotected |
Referenced by Native.fixedpointDecRef().
|
staticprotected |
Referenced by Native.fixedpointFromFile().
|
staticprotected |
Referenced by Native.fixedpointFromString().
|
staticprotected |
Referenced by Native.fixedpointGetAnswer().
|
staticprotected |
Referenced by Native.fixedpointGetAssertions().
|
staticprotected |
Referenced by Native.fixedpointGetCoverDelta().
|
staticprotected |
Referenced by Native.fixedpointGetGroundSatAnswer().
|
staticprotected |
Referenced by Native.fixedpointGetHelp().
|
staticprotected |
Referenced by Native.fixedpointGetNumLevels().
|
staticprotected |
Referenced by Native.fixedpointGetParamDescrs().
|
staticprotected |
Referenced by Native.fixedpointGetReachable().
|
staticprotected |
Referenced by Native.fixedpointGetReasonUnknown().
|
staticprotected |
Referenced by Native.fixedpointGetRuleNamesAlongTrace().
|
staticprotected |
Referenced by Native.fixedpointGetRules().
|
staticprotected |
Referenced by Native.fixedpointGetRulesAlongTrace().
|
staticprotected |
Referenced by Native.fixedpointGetStatistics().
|
staticprotected |
Referenced by Native.fixedpointIncRef().
|
staticprotected |
Referenced by Native.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.addRecDef(), Native.algebraicAdd(), Native.algebraicDiv(), Native.algebraicEq(), Native.algebraicEval(), Native.algebraicGe(), Native.algebraicGt(), Native.algebraicIsNeg(), Native.algebraicIsPos(), Native.algebraicIsValue(), Native.algebraicIsZero(), Native.algebraicLe(), Native.algebraicLt(), Native.algebraicMul(), Native.algebraicNeq(), Native.algebraicPower(), Native.algebraicRoot(), Native.algebraicRoots(), Native.algebraicSign(), Native.algebraicSub(), Native.applyResultDecRef(), Native.applyResultGetNumSubgoals(), Native.applyResultGetSubgoal(), Native.applyResultIncRef(), Native.applyResultToString(), Native.appToAst(), Native.astMapContains(), Native.astMapDecRef(), Native.astMapErase(), Native.astMapFind(), Native.astMapIncRef(), Native.astMapInsert(), Native.astMapKeys(), Native.astMapReset(), Native.astMapSize(), Native.astMapToString(), Native.astToString(), Native.astVectorDecRef(), Native.astVectorGet(), Native.astVectorIncRef(), Native.astVectorPush(), Native.astVectorResize(), Native.astVectorSet(), Native.astVectorSize(), Native.astVectorToString(), Native.astVectorTranslate(), Native.benchmarkToSmtlibString(), Native.datatypeUpdateField(), Native.decRef(), Native.delConstructor(), Native.delConstructorList(), Native.evalSmtlib2String(), Native.fixedpointAddCover(), Native.fixedpointAddFact(), Native.fixedpointAddInvariant(), Native.fixedpointAddRule(), Native.fixedpointAssert(), Native.fixedpointDecRef(), Native.fixedpointFromFile(), Native.fixedpointFromString(), Native.fixedpointGetAnswer(), Native.fixedpointGetAssertions(), Native.fixedpointGetCoverDelta(), Native.fixedpointGetGroundSatAnswer(), Native.fixedpointGetHelp(), Native.fixedpointGetNumLevels(), Native.fixedpointGetParamDescrs(), Native.fixedpointGetReachable(), Native.fixedpointGetReasonUnknown(), Native.fixedpointGetRuleNamesAlongTrace(), Native.fixedpointGetRules(), Native.fixedpointGetRulesAlongTrace(), Native.fixedpointGetStatistics(), Native.fixedpointIncRef(), Native.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.getNumeralDecimalString(), Native.getNumeralDouble(), Native.getNumeralInt(), Native.getNumeralInt64(), Native.getNumeralRationalInt64(), Native.getNumeralSmall(), Native.getNumeralString(), Native.getNumeralUint(), Native.getNumeralUint64(), Native.getNumerator(), Native.getNumProbes(), Native.getNumTactics(), Native.getPattern(), Native.getPatternNumTerms(), Native.getProbeName(), Native.getQuantifierBody(), Native.getQuantifierBoundName(), Native.getQuantifierBoundSort(), Native.getQuantifierNoPatternAst(), Native.getQuantifierNumBound(), Native.getQuantifierNumNoPatterns(), Native.getQuantifierNumPatterns(), Native.getQuantifierPatternAst(), Native.getQuantifierWeight(), Native.getRange(), Native.getRelationArity(), Native.getRelationColumn(), Native.getSort(), Native.getSortId(), Native.getSortKind(), Native.getSortName(), Native.getString(), Native.getSymbolInt(), Native.getSymbolKind(), Native.getSymbolString(), Native.getTacticName(), Native.getTupleSortFieldDecl(), Native.getTupleSortMkDecl(), Native.getTupleSortNumFields(), Native.goalAssert(), Native.goalConvertModel(), Native.goalDecRef(), Native.goalDepth(), Native.goalFormula(), Native.goalInconsistent(), Native.goalIncRef(), Native.goalIsDecidedSat(), Native.goalIsDecidedUnsat(), Native.goalNumExprs(), Native.goalPrecision(), Native.goalReset(), Native.goalSize(), Native.goalToDimacsString(), Native.goalToString(), Native.goalTranslate(), Native.incRef(), Native.interrupt(), Native.isAlgebraicNumber(), Native.isApp(), Native.isAsArray(), Native.isEqAst(), Native.isEqFuncDecl(), Native.isEqSort(), Native.isLambda(), Native.isNumeralAst(), Native.isQuantifierExists(), Native.isQuantifierForall(), Native.isReSort(), Native.isSeqSort(), Native.isString(), Native.isStringSort(), Native.isWellSorted(), Native.mkAdd(), Native.mkAnd(), Native.mkApp(), Native.mkArrayDefault(), Native.mkArrayExt(), Native.mkArraySort(), Native.mkArraySortN(), Native.mkAsArray(), Native.mkAstMap(), Native.mkAstVector(), Native.mkAtleast(), Native.mkAtmost(), Native.mkBoolSort(), Native.mkBound(), Native.mkBv2int(), Native.mkBvadd(), Native.mkBvaddNoOverflow(), Native.mkBvaddNoUnderflow(), Native.mkBvand(), Native.mkBvashr(), Native.mkBvlshr(), Native.mkBvmul(), Native.mkBvmulNoOverflow(), Native.mkBvmulNoUnderflow(), Native.mkBvnand(), Native.mkBvneg(), Native.mkBvnegNoOverflow(), Native.mkBvnor(), Native.mkBvnot(), Native.mkBvNumeral(), Native.mkBvor(), Native.mkBvredand(), Native.mkBvredor(), Native.mkBvsdiv(), Native.mkBvsdivNoOverflow(), Native.mkBvsge(), Native.mkBvsgt(), Native.mkBvshl(), Native.mkBvsle(), Native.mkBvslt(), Native.mkBvsmod(), Native.mkBvSort(), Native.mkBvsrem(), Native.mkBvsub(), Native.mkBvsubNoOverflow(), Native.mkBvsubNoUnderflow(), Native.mkBvudiv(), Native.mkBvuge(), Native.mkBvugt(), Native.mkBvule(), Native.mkBvult(), Native.mkBvurem(), Native.mkBvxnor(), Native.mkBvxor(), Native.mkConcat(), Native.mkConst(), Native.mkConstArray(), Native.mkConstructor(), Native.mkConstructorList(), Native.mkDatatype(), Native.mkDatatypes(), Native.mkDistinct(), Native.mkDiv(), Native.mkEmptySet(), Native.mkEnumerationSort(), Native.mkEq(), Native.mkExists(), Native.mkExistsConst(), Native.mkExtract(), Native.mkExtRotateLeft(), Native.mkExtRotateRight(), Native.mkFalse(), Native.mkFiniteDomainSort(), Native.mkFixedpoint(), Native.mkForall(), Native.mkForallConst(), Native.mkFpaAbs(), Native.mkFpaAdd(), Native.mkFpaDiv(), Native.mkFpaEq(), Native.mkFpaFma(), Native.mkFpaFp(), Native.mkFpaGeq(), Native.mkFpaGt(), Native.mkFpaInf(), Native.mkFpaIsInfinite(), Native.mkFpaIsNan(), Native.mkFpaIsNegative(), Native.mkFpaIsNormal(), Native.mkFpaIsPositive(), Native.mkFpaIsSubnormal(), Native.mkFpaIsZero(), Native.mkFpaLeq(), Native.mkFpaLt(), Native.mkFpaMax(), Native.mkFpaMin(), Native.mkFpaMul(), Native.mkFpaNan(), Native.mkFpaNeg(), Native.mkFpaNumeralDouble(), Native.mkFpaNumeralFloat(), Native.mkFpaNumeralInt(), Native.mkFpaNumeralInt64Uint64(), Native.mkFpaNumeralIntUint(), Native.mkFpaRem(), Native.mkFpaRna(), Native.mkFpaRne(), Native.mkFpaRoundingModeSort(), Native.mkFpaRoundNearestTiesToAway(), Native.mkFpaRoundNearestTiesToEven(), Native.mkFpaRoundToIntegral(), Native.mkFpaRoundTowardNegative(), Native.mkFpaRoundTowardPositive(), Native.mkFpaRoundTowardZero(), Native.mkFpaRtn(), Native.mkFpaRtp(), Native.mkFpaRtz(), Native.mkFpaSort(), Native.mkFpaSort128(), Native.mkFpaSort16(), Native.mkFpaSort32(), Native.mkFpaSort64(), Native.mkFpaSortDouble(), Native.mkFpaSortHalf(), Native.mkFpaSortQuadruple(), Native.mkFpaSortSingle(), Native.mkFpaSqrt(), Native.mkFpaSub(), Native.mkFpaToFpBv(), Native.mkFpaToFpFloat(), Native.mkFpaToFpIntReal(), Native.mkFpaToFpReal(), Native.mkFpaToFpSigned(), Native.mkFpaToFpUnsigned(), Native.mkFpaToIeeeBv(), Native.mkFpaToReal(), Native.mkFpaToSbv(), Native.mkFpaToUbv(), Native.mkFpaZero(), Native.mkFreshConst(), Native.mkFreshFuncDecl(), Native.mkFullSet(), Native.mkFuncDecl(), Native.mkGe(), Native.mkGoal(), Native.mkGt(), Native.mkIff(), Native.mkImplies(), Native.mkInt(), Native.mkInt2bv(), Native.mkInt2real(), Native.mkInt64(), Native.mkIntSort(), Native.mkIntSymbol(), Native.mkIntToStr(), Native.mkIsInt(), Native.mkIte(), Native.mkLambda(), Native.mkLambdaConst(), Native.mkLe(), Native.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.mkRecFuncDecl(), Native.mkReComplement(), Native.mkReConcat(), Native.mkReEmpty(), Native.mkReFull(), Native.mkReIntersect(), Native.mkReLoop(), Native.mkRem(), Native.mkReOption(), Native.mkRepeat(), Native.mkRePlus(), Native.mkReRange(), Native.mkReSort(), Native.mkReStar(), Native.mkReUnion(), Native.mkRotateLeft(), Native.mkRotateRight(), Native.mkSelect(), Native.mkSelectN(), Native.mkSeqAt(), Native.mkSeqConcat(), Native.mkSeqContains(), Native.mkSeqEmpty(), Native.mkSeqExtract(), Native.mkSeqIndex(), Native.mkSeqInRe(), Native.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.optimizeGetUnsatCore(), Native.optimizeGetUpper(), Native.optimizeGetUpperAsVector(), Native.optimizeIncRef(), Native.optimizeMaximize(), Native.optimizeMinimize(), Native.optimizePop(), Native.optimizePush(), Native.optimizeSetParams(), Native.optimizeToString(), Native.paramDescrsDecRef(), Native.paramDescrsGetDocumentation(), Native.paramDescrsGetKind(), Native.paramDescrsGetName(), Native.paramDescrsIncRef(), Native.paramDescrsSize(), Native.paramDescrsToString(), Native.paramsDecRef(), Native.paramsIncRef(), Native.paramsSetBool(), Native.paramsSetDouble(), Native.paramsSetSymbol(), Native.paramsSetUint(), Native.paramsToString(), Native.paramsValidate(), Native.parseSmtlib2File(), Native.parseSmtlib2String(), Native.patternToAst(), Native.patternToString(), Native.polynomialSubresultants(), Native.probeAnd(), Native.probeApply(), Native.probeConst(), Native.probeDecRef(), Native.probeEq(), Native.probeGe(), Native.probeGetDescr(), Native.probeGt(), Native.probeIncRef(), Native.probeLe(), Native.probeLt(), Native.probeNot(), Native.probeOr(), Native.qeLite(), Native.qeModelProject(), Native.qeModelProjectSkolem(), Native.queryConstructor(), Native.rcfAdd(), Native.rcfDel(), Native.rcfDiv(), Native.rcfEq(), Native.rcfGe(), Native.rcfGetNumeratorDenominator(), Native.rcfGt(), Native.rcfInv(), Native.rcfLe(), Native.rcfLt(), Native.rcfMkE(), Native.rcfMkInfinitesimal(), Native.rcfMkPi(), Native.rcfMkRational(), Native.rcfMkRoots(), Native.rcfMkSmallInt(), Native.rcfMul(), Native.rcfNeg(), Native.rcfNeq(), Native.rcfNumToDecimalString(), Native.rcfNumToString(), Native.rcfPower(), Native.rcfSub(), Native.setAstPrintMode(), Native.setError(), Native.simplify(), Native.simplifyEx(), Native.simplifyGetHelp(), Native.simplifyGetParamDescrs(), Native.solverAssert(), Native.solverAssertAndTrack(), Native.solverCheck(), Native.solverCheckAssumptions(), Native.solverCube(), Native.solverDecRef(), Native.solverFromFile(), Native.solverFromString(), Native.solverGetAssertions(), Native.solverGetConsequences(), Native.solverGetHelp(), Native.solverGetModel(), Native.solverGetNonUnits(), Native.solverGetNumScopes(), Native.solverGetParamDescrs(), Native.solverGetProof(), Native.solverGetReasonUnknown(), Native.solverGetStatistics(), Native.solverGetUnits(), Native.solverGetUnsatCore(), Native.solverImportModelConverter(), 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(), and Native.updateTerm().
|
staticprotected |
Referenced by Native.addConstInterp(), Native.addFuncInterp(), Native.addRecDef(), Native.algebraicAdd(), Native.algebraicDiv(), Native.algebraicEq(), Native.algebraicEval(), Native.algebraicGe(), Native.algebraicGt(), Native.algebraicIsNeg(), Native.algebraicIsPos(), Native.algebraicIsValue(), Native.algebraicIsZero(), Native.algebraicLe(), Native.algebraicLt(), Native.algebraicMul(), Native.algebraicNeq(), Native.algebraicPower(), Native.algebraicRoot(), Native.algebraicRoots(), Native.algebraicSign(), Native.algebraicSub(), Native.applyResultDecRef(), Native.applyResultGetNumSubgoals(), Native.applyResultGetSubgoal(), Native.applyResultIncRef(), Native.applyResultToString(), Native.appToAst(), Native.astMapContains(), Native.astMapDecRef(), Native.astMapErase(), Native.astMapFind(), Native.astMapIncRef(), Native.astMapInsert(), Native.astMapKeys(), Native.astMapReset(), Native.astMapSize(), Native.astMapToString(), Native.astToString(), Native.astVectorDecRef(), Native.astVectorGet(), Native.astVectorIncRef(), Native.astVectorPush(), Native.astVectorResize(), Native.astVectorSet(), Native.astVectorSize(), Native.astVectorToString(), Native.astVectorTranslate(), Native.benchmarkToSmtlibString(), Native.datatypeUpdateField(), Native.decRef(), Native.delConstructor(), Native.delConstructorList(), Native.evalSmtlib2String(), Native.fixedpointAddCover(), Native.fixedpointAddFact(), Native.fixedpointAddInvariant(), Native.fixedpointAddRule(), Native.fixedpointAssert(), Native.fixedpointDecRef(), Native.fixedpointFromFile(), Native.fixedpointFromString(), Native.fixedpointGetAnswer(), Native.fixedpointGetAssertions(), Native.fixedpointGetCoverDelta(), Native.fixedpointGetGroundSatAnswer(), Native.fixedpointGetHelp(), Native.fixedpointGetNumLevels(), Native.fixedpointGetParamDescrs(), Native.fixedpointGetReachable(), Native.fixedpointGetReasonUnknown(), Native.fixedpointGetRuleNamesAlongTrace(), Native.fixedpointGetRules(), Native.fixedpointGetRulesAlongTrace(), Native.fixedpointGetStatistics(), Native.fixedpointIncRef(), Native.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.getNumeralDecimalString(), Native.getNumeralDouble(), Native.getNumeralInt(), Native.getNumeralInt64(), Native.getNumeralRationalInt64(), Native.getNumeralSmall(), Native.getNumeralString(), Native.getNumeralUint(), Native.getNumeralUint64(), Native.getNumerator(), Native.getNumProbes(), Native.getNumTactics(), Native.getPattern(), Native.getPatternNumTerms(), Native.getProbeName(), Native.getQuantifierBody(), Native.getQuantifierBoundName(), Native.getQuantifierBoundSort(), Native.getQuantifierNoPatternAst(), Native.getQuantifierNumBound(), Native.getQuantifierNumNoPatterns(), Native.getQuantifierNumPatterns(), Native.getQuantifierPatternAst(), Native.getQuantifierWeight(), Native.getRange(), Native.getRelationArity(), Native.getRelationColumn(), Native.getSort(), Native.getSortId(), Native.getSortKind(), Native.getSortName(), Native.getString(), Native.getSymbolInt(), Native.getSymbolKind(), Native.getSymbolString(), Native.getTacticName(), Native.getTupleSortFieldDecl(), Native.getTupleSortMkDecl(), Native.getTupleSortNumFields(), Native.goalAssert(), Native.goalConvertModel(), Native.goalDecRef(), Native.goalDepth(), Native.goalFormula(), Native.goalInconsistent(), Native.goalIncRef(), Native.goalIsDecidedSat(), Native.goalIsDecidedUnsat(), Native.goalNumExprs(), Native.goalPrecision(), Native.goalReset(), Native.goalSize(), Native.goalToDimacsString(), Native.goalToString(), Native.goalTranslate(), Native.incRef(), Native.interrupt(), Native.isAlgebraicNumber(), Native.isApp(), Native.isAsArray(), Native.isEqAst(), Native.isEqFuncDecl(), Native.isEqSort(), Native.isLambda(), Native.isNumeralAst(), Native.isQuantifierExists(), Native.isQuantifierForall(), Native.isReSort(), Native.isSeqSort(), Native.isString(), Native.isStringSort(), Native.isWellSorted(), Native.mkAdd(), Native.mkAnd(), Native.mkApp(), Native.mkArrayDefault(), Native.mkArrayExt(), Native.mkArraySort(), Native.mkArraySortN(), Native.mkAsArray(), Native.mkAstMap(), Native.mkAstVector(), Native.mkAtleast(), Native.mkAtmost(), Native.mkBoolSort(), Native.mkBound(), Native.mkBv2int(), Native.mkBvadd(), Native.mkBvaddNoOverflow(), Native.mkBvaddNoUnderflow(), Native.mkBvand(), Native.mkBvashr(), Native.mkBvlshr(), Native.mkBvmul(), Native.mkBvmulNoOverflow(), Native.mkBvmulNoUnderflow(), Native.mkBvnand(), Native.mkBvneg(), Native.mkBvnegNoOverflow(), Native.mkBvnor(), Native.mkBvnot(), Native.mkBvNumeral(), Native.mkBvor(), Native.mkBvredand(), Native.mkBvredor(), Native.mkBvsdiv(), Native.mkBvsdivNoOverflow(), Native.mkBvsge(), Native.mkBvsgt(), Native.mkBvshl(), Native.mkBvsle(), Native.mkBvslt(), Native.mkBvsmod(), Native.mkBvSort(), Native.mkBvsrem(), Native.mkBvsub(), Native.mkBvsubNoOverflow(), Native.mkBvsubNoUnderflow(), Native.mkBvudiv(), Native.mkBvuge(), Native.mkBvugt(), Native.mkBvule(), Native.mkBvult(), Native.mkBvurem(), Native.mkBvxnor(), Native.mkBvxor(), Native.mkConcat(), Native.mkConst(), Native.mkConstArray(), Native.mkConstructor(), Native.mkConstructorList(), Native.mkDatatype(), Native.mkDatatypes(), Native.mkDistinct(), Native.mkDiv(), Native.mkEmptySet(), Native.mkEnumerationSort(), Native.mkEq(), Native.mkExists(), Native.mkExistsConst(), Native.mkExtract(), Native.mkExtRotateLeft(), Native.mkExtRotateRight(), Native.mkFalse(), Native.mkFiniteDomainSort(), Native.mkFixedpoint(), Native.mkForall(), Native.mkForallConst(), Native.mkFpaAbs(), Native.mkFpaAdd(), Native.mkFpaDiv(), Native.mkFpaEq(), Native.mkFpaFma(), Native.mkFpaFp(), Native.mkFpaGeq(), Native.mkFpaGt(), Native.mkFpaInf(), Native.mkFpaIsInfinite(), Native.mkFpaIsNan(), Native.mkFpaIsNegative(), Native.mkFpaIsNormal(), Native.mkFpaIsPositive(), Native.mkFpaIsSubnormal(), Native.mkFpaIsZero(), Native.mkFpaLeq(), Native.mkFpaLt(), Native.mkFpaMax(), Native.mkFpaMin(), Native.mkFpaMul(), Native.mkFpaNan(), Native.mkFpaNeg(), Native.mkFpaNumeralDouble(), Native.mkFpaNumeralFloat(), Native.mkFpaNumeralInt(), Native.mkFpaNumeralInt64Uint64(), Native.mkFpaNumeralIntUint(), Native.mkFpaRem(), Native.mkFpaRna(), Native.mkFpaRne(), Native.mkFpaRoundingModeSort(), Native.mkFpaRoundNearestTiesToAway(), Native.mkFpaRoundNearestTiesToEven(), Native.mkFpaRoundToIntegral(), Native.mkFpaRoundTowardNegative(), Native.mkFpaRoundTowardPositive(), Native.mkFpaRoundTowardZero(), Native.mkFpaRtn(), Native.mkFpaRtp(), Native.mkFpaRtz(), Native.mkFpaSort(), Native.mkFpaSort128(), Native.mkFpaSort16(), Native.mkFpaSort32(), Native.mkFpaSort64(), Native.mkFpaSortDouble(), Native.mkFpaSortHalf(), Native.mkFpaSortQuadruple(), Native.mkFpaSortSingle(), Native.mkFpaSqrt(), Native.mkFpaSub(), Native.mkFpaToFpBv(), Native.mkFpaToFpFloat(), Native.mkFpaToFpIntReal(), Native.mkFpaToFpReal(), Native.mkFpaToFpSigned(), Native.mkFpaToFpUnsigned(), Native.mkFpaToIeeeBv(), Native.mkFpaToReal(), Native.mkFpaToSbv(), Native.mkFpaToUbv(), Native.mkFpaZero(), Native.mkFreshConst(), Native.mkFreshFuncDecl(), Native.mkFullSet(), Native.mkFuncDecl(), Native.mkGe(), Native.mkGoal(), Native.mkGt(), Native.mkIff(), Native.mkImplies(), Native.mkInt(), Native.mkInt2bv(), Native.mkInt2real(), Native.mkInt64(), Native.mkIntSort(), Native.mkIntSymbol(), Native.mkIntToStr(), Native.mkIsInt(), Native.mkIte(), Native.mkLambda(), Native.mkLambdaConst(), Native.mkLe(), Native.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.mkRecFuncDecl(), Native.mkReComplement(), Native.mkReConcat(), Native.mkReEmpty(), Native.mkReFull(), Native.mkReIntersect(), Native.mkReLoop(), Native.mkRem(), Native.mkReOption(), Native.mkRepeat(), Native.mkRePlus(), Native.mkReRange(), Native.mkReSort(), Native.mkReStar(), Native.mkReUnion(), Native.mkRotateLeft(), Native.mkRotateRight(), Native.mkSelect(), Native.mkSelectN(), Native.mkSeqAt(), Native.mkSeqConcat(), Native.mkSeqContains(), Native.mkSeqEmpty(), Native.mkSeqExtract(), Native.mkSeqIndex(), Native.mkSeqInRe(), Native.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.optimizeGetUnsatCore(), Native.optimizeGetUpper(), Native.optimizeGetUpperAsVector(), Native.optimizeIncRef(), Native.optimizeMaximize(), Native.optimizeMinimize(), Native.optimizePop(), Native.optimizePush(), Native.optimizeSetParams(), Native.optimizeToString(), Native.paramDescrsDecRef(), Native.paramDescrsGetDocumentation(), Native.paramDescrsGetKind(), Native.paramDescrsGetName(), Native.paramDescrsIncRef(), Native.paramDescrsSize(), Native.paramDescrsToString(), Native.paramsDecRef(), Native.paramsIncRef(), Native.paramsSetBool(), Native.paramsSetDouble(), Native.paramsSetSymbol(), Native.paramsSetUint(), Native.paramsToString(), Native.paramsValidate(), Native.parseSmtlib2File(), Native.parseSmtlib2String(), Native.patternToAst(), Native.patternToString(), Native.polynomialSubresultants(), Native.probeAnd(), Native.probeApply(), Native.probeConst(), Native.probeDecRef(), Native.probeEq(), Native.probeGe(), Native.probeGetDescr(), Native.probeGt(), Native.probeIncRef(), Native.probeLe(), Native.probeLt(), Native.probeNot(), Native.probeOr(), Native.qeLite(), Native.qeModelProject(), Native.qeModelProjectSkolem(), Native.queryConstructor(), Native.rcfAdd(), Native.rcfDel(), Native.rcfDiv(), Native.rcfEq(), Native.rcfGe(), Native.rcfGetNumeratorDenominator(), Native.rcfGt(), Native.rcfInv(), Native.rcfLe(), Native.rcfLt(), Native.rcfMkE(), Native.rcfMkInfinitesimal(), Native.rcfMkPi(), Native.rcfMkRational(), Native.rcfMkRoots(), Native.rcfMkSmallInt(), Native.rcfMul(), Native.rcfNeg(), Native.rcfNeq(), Native.rcfNumToDecimalString(), Native.rcfNumToString(), Native.rcfPower(), Native.rcfSub(), Native.setAstPrintMode(), Native.setError(), Native.simplify(), Native.simplifyEx(), Native.simplifyGetHelp(), Native.simplifyGetParamDescrs(), Native.solverAssert(), Native.solverAssertAndTrack(), Native.solverCheck(), Native.solverCheckAssumptions(), Native.solverCube(), Native.solverDecRef(), Native.solverFromFile(), Native.solverFromString(), Native.solverGetAssertions(), Native.solverGetConsequences(), Native.solverGetHelp(), Native.solverGetModel(), Native.solverGetNonUnits(), Native.solverGetNumScopes(), Native.solverGetParamDescrs(), Native.solverGetProof(), Native.solverGetReasonUnknown(), Native.solverGetStatistics(), Native.solverGetUnits(), Native.solverGetUnsatCore(), Native.solverImportModelConverter(), 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(), and Native.updateTerm().
|
staticprotected |
Referenced by Native.getEstimatedAllocSize().
|
staticprotected |
Referenced by Native.getFiniteDomainSortSize().
|
staticprotected |
Referenced by Native.getFullVersion().
|
staticprotected |
Referenced by Native.getFuncDeclId().
|
staticprotected |
Referenced by Native.getImpliedEqualities().
|
staticprotected |
Referenced by Native.getIndexValue().
|
staticprotected |
Referenced by Native.getNumeralDecimalString().
|
staticprotected |
Referenced by Native.getNumeralDouble().
|
staticprotected |
Referenced by Native.getNumeralInt().
|
staticprotected |
Referenced by Native.getNumeralInt64().
|
staticprotected |
Referenced by Native.getNumeralRationalInt64().
|
staticprotected |
Referenced by Native.getNumeralSmall().
|
staticprotected |
Referenced by Native.getNumeralString().
|
staticprotected |
Referenced by Native.getNumeralUint().
|
staticprotected |
Referenced by Native.getNumeralUint64().
|
staticprotected |
Referenced by Native.getNumerator().
|
staticprotected |
Referenced by Native.getNumProbes().
|
staticprotected |
Referenced by Native.getNumTactics().
|
staticprotected |
Referenced by Native.getPattern().
|
staticprotected |
Referenced by Native.getPatternNumTerms().
|
staticprotected |
Referenced by Native.getProbeName().
|
staticprotected |
Referenced by Native.getQuantifierBody().
|
staticprotected |
Referenced by Native.getQuantifierBoundName().
|
staticprotected |
Referenced by Native.getQuantifierBoundSort().
|
staticprotected |
Referenced by Native.getQuantifierNoPatternAst().
|
staticprotected |
Referenced by Native.getQuantifierNumBound().
|
staticprotected |
Referenced by Native.getQuantifierNumNoPatterns().
|
staticprotected |
Referenced by Native.getQuantifierNumPatterns().
|
staticprotected |
Referenced by Native.getQuantifierPatternAst().
|
staticprotected |
Referenced by Native.getQuantifierWeight().
|
staticprotected |
Referenced by Native.getRange().
|
staticprotected |
Referenced by Native.getRelationArity().
|
staticprotected |
Referenced by Native.getRelationColumn().
|
staticprotected |
Referenced by Native.getSort().
|
staticprotected |
Referenced by Native.getSortId().
|
staticprotected |
Referenced by Native.getSortKind().
|
staticprotected |
Referenced by Native.getSortName().
|
staticprotected |
Referenced by Native.getString().
|
staticprotected |
Referenced by Native.getSymbolInt().
|
staticprotected |
Referenced by Native.getSymbolKind().
|
staticprotected |
Referenced by Native.getSymbolString().
|
staticprotected |
Referenced by Native.getTacticName().
|
staticprotected |
Referenced by Native.getTupleSortFieldDecl().
|
staticprotected |
Referenced by Native.getTupleSortMkDecl().
|
staticprotected |
Referenced by Native.getTupleSortNumFields().
|
staticprotected |
Referenced by Native.getVersion().
|
staticprotected |
Referenced by Native.globalParamGet().
|
staticprotected |
Referenced by Native.globalParamResetAll().
|
staticprotected |
Referenced by Native.globalParamSet().
|
staticprotected |
Referenced by Native.goalAssert().
|
staticprotected |
Referenced by Native.goalConvertModel().
|
staticprotected |
Referenced by Native.goalDecRef().
|
staticprotected |
Referenced by Native.goalDepth().
|
staticprotected |
Referenced by Native.goalFormula().
|
staticprotected |
Referenced by Native.goalInconsistent().
|
staticprotected |
Referenced by Native.goalIncRef().
|
staticprotected |
Referenced by Native.goalIsDecidedSat().
|
staticprotected |
Referenced by Native.goalIsDecidedUnsat().
|
staticprotected |
Referenced by Native.goalNumExprs().
|
staticprotected |
Referenced by Native.goalPrecision().
|
staticprotected |
Referenced by Native.goalReset().
|
staticprotected |
Referenced by Native.goalSize().
|
staticprotected |
Referenced by Native.goalToDimacsString().
|
staticprotected |
Referenced by Native.goalToString().
|
staticprotected |
Referenced by Native.goalTranslate().
|
staticprotected |
Referenced by Native.incRef().
|
staticprotected |
Referenced by Native.interrupt().
|
staticprotected |
Referenced by Native.isAlgebraicNumber().
|
staticprotected |
Referenced by Native.isApp().
|
staticprotected |
Referenced by Native.isAsArray().
|
staticprotected |
Referenced by Native.isEqAst().
|
staticprotected |
Referenced by Native.isEqFuncDecl().
|
staticprotected |
Referenced by Native.isEqSort().
|
staticprotected |
Referenced by Native.isLambda().
|
staticprotected |
Referenced by Native.isNumeralAst().
|
staticprotected |
Referenced by Native.isQuantifierExists().
|
staticprotected |
Referenced by Native.isQuantifierForall().
|
staticprotected |
Referenced by Native.isReSort().
|
staticprotected |
Referenced by Native.isSeqSort().
|
staticprotected |
Referenced by Native.isString().
|
staticprotected |
Referenced by Native.isStringSort().
|
staticprotected |
Referenced by Native.isWellSorted().
|
staticprotected |
Referenced by Native.mkAdd().
|
staticprotected |
Referenced by Native.mkAnd().
|
staticprotected |
Referenced by Native.mkApp().
|
staticprotected |
Referenced by Native.mkArrayDefault().
|
staticprotected |
Referenced by Native.mkArrayExt().
|
staticprotected |
Referenced by Native.mkArraySort().
|
staticprotected |
Referenced by Native.mkArraySortN().
|
staticprotected |
Referenced by Native.mkAsArray().
|
staticprotected |
Referenced by Native.mkAstMap().
|
staticprotected |
Referenced by Native.mkAstVector().
|
staticprotected |
Referenced by Native.mkAtleast().
|
staticprotected |
Referenced by Native.mkAtmost().
|
staticprotected |
Referenced by Native.mkBoolSort().
|
staticprotected |
Referenced by Native.mkBound().
|
staticprotected |
Referenced by Native.mkBv2int().
|
staticprotected |
Referenced by Native.mkBvadd().
|
staticprotected |
Referenced by Native.mkBvaddNoOverflow().
|
staticprotected |
Referenced by Native.mkBvaddNoUnderflow().
|
staticprotected |
Referenced by Native.mkBvand().
|
staticprotected |
Referenced by Native.mkBvashr().
|
staticprotected |
Referenced by Native.mkBvlshr().
|
staticprotected |
Referenced by Native.mkBvmul().
|
staticprotected |
Referenced by Native.mkBvmulNoOverflow().
|
staticprotected |
Referenced by Native.mkBvmulNoUnderflow().
|
staticprotected |
Referenced by Native.mkBvnand().
|
staticprotected |
Referenced by Native.mkBvneg().
|
staticprotected |
Referenced by Native.mkBvnegNoOverflow().
|
staticprotected |
Referenced by Native.mkBvnor().
|
staticprotected |
Referenced by Native.mkBvnot().
|
staticprotected |
Referenced by Native.mkBvNumeral().
|
staticprotected |
Referenced by Native.mkBvor().
|
staticprotected |
Referenced by Native.mkBvredand().
|
staticprotected |
Referenced by Native.mkBvredor().
|
staticprotected |
Referenced by Native.mkBvsdiv().
|
staticprotected |
Referenced by Native.mkBvsdivNoOverflow().
|
staticprotected |
Referenced by Native.mkBvsge().
|
staticprotected |
Referenced by Native.mkBvsgt().
|
staticprotected |
Referenced by Native.mkBvshl().
|
staticprotected |
Referenced by Native.mkBvsle().
|
staticprotected |
Referenced by Native.mkBvslt().
|
staticprotected |
Referenced by Native.mkBvsmod().
|
staticprotected |
Referenced by Native.mkBvSort().
|
staticprotected |
Referenced by Native.mkBvsrem().
|
staticprotected |
Referenced by Native.mkBvsub().
|
staticprotected |
Referenced by Native.mkBvsubNoOverflow().
|
staticprotected |
Referenced by Native.mkBvsubNoUnderflow().
|
staticprotected |
Referenced by Native.mkBvudiv().
|
staticprotected |
Referenced by Native.mkBvuge().
|
staticprotected |
Referenced by Native.mkBvugt().
|
staticprotected |
Referenced by Native.mkBvule().
|
staticprotected |
Referenced by Native.mkBvult().
|
staticprotected |
Referenced by Native.mkBvurem().
|
staticprotected |
Referenced by Native.mkBvxnor().
|
staticprotected |
Referenced by Native.mkBvxor().
|
staticprotected |
Referenced by Native.mkConcat().
|
staticprotected |
Referenced by Native.mkConfig().
|
staticprotected |
Referenced by Native.mkConst().
|
staticprotected |
Referenced by Native.mkConstArray().
|
staticprotected |
Referenced by Native.mkConstructor().
|
staticprotected |
Referenced by Native.mkConstructorList().
|
staticprotected |
Referenced by Native.mkContext().
|
staticprotected |
Referenced by Native.mkContextRc().
|
staticprotected |
Referenced by Native.mkDatatype().
|
staticprotected |
Referenced by Native.mkDatatypes().
|
staticprotected |
Referenced by Native.mkDistinct().
|
staticprotected |
Referenced by Native.mkDiv().
|
staticprotected |
Referenced by Native.mkEmptySet().
|
staticprotected |
Referenced by Native.mkEnumerationSort().
|
staticprotected |
Referenced by Native.mkEq().
|
staticprotected |
Referenced by Native.mkExists().
|
staticprotected |
Referenced by Native.mkExistsConst().
|
staticprotected |
Referenced by Native.mkExtract().
|
staticprotected |
Referenced by Native.mkExtRotateLeft().
|
staticprotected |
Referenced by Native.mkExtRotateRight().
|
staticprotected |
Referenced by Native.mkFalse().
|
staticprotected |
Referenced by Native.mkFiniteDomainSort().
|
staticprotected |
Referenced by Native.mkFixedpoint().
|
staticprotected |
Referenced by Native.mkForall().
|
staticprotected |
Referenced by Native.mkForallConst().
|
staticprotected |
Referenced by Native.mkFpaAbs().
|
staticprotected |
Referenced by Native.mkFpaAdd().
|
staticprotected |
Referenced by Native.mkFpaDiv().
|
staticprotected |
Referenced by Native.mkFpaEq().
|
staticprotected |
Referenced by Native.mkFpaFma().
|
staticprotected |
Referenced by Native.mkFpaFp().
|
staticprotected |
Referenced by Native.mkFpaGeq().
|
staticprotected |
Referenced by Native.mkFpaGt().
|
staticprotected |
Referenced by Native.mkFpaInf().
|
staticprotected |
Referenced by Native.mkFpaIsInfinite().
|
staticprotected |
Referenced by Native.mkFpaIsNan().
|
staticprotected |
Referenced by Native.mkFpaIsNegative().
|
staticprotected |
Referenced by Native.mkFpaIsNormal().
|
staticprotected |
Referenced by Native.mkFpaIsPositive().
|
staticprotected |
Referenced by Native.mkFpaIsSubnormal().
|
staticprotected |
Referenced by Native.mkFpaIsZero().
|
staticprotected |
Referenced by Native.mkFpaLeq().
|
staticprotected |
Referenced by Native.mkFpaLt().
|
staticprotected |
Referenced by Native.mkFpaMax().
|
staticprotected |
Referenced by Native.mkFpaMin().
|
staticprotected |
Referenced by Native.mkFpaMul().
|
staticprotected |
Referenced by Native.mkFpaNan().
|
staticprotected |
Referenced by Native.mkFpaNeg().
|
staticprotected |
Referenced by Native.mkFpaNumeralDouble().
|
staticprotected |
Referenced by Native.mkFpaNumeralFloat().
|
staticprotected |
Referenced by Native.mkFpaNumeralInt().
|
staticprotected |
Referenced by Native.mkFpaNumeralInt64Uint64().
|
staticprotected |
Referenced by Native.mkFpaNumeralIntUint().
|
staticprotected |
Referenced by Native.mkFpaRem().
|
staticprotected |
Referenced by Native.mkFpaRna().
|
staticprotected |
Referenced by Native.mkFpaRne().
|
staticprotected |
Referenced by Native.mkFpaRoundingModeSort().
|
staticprotected |
Referenced by Native.mkFpaRoundNearestTiesToAway().
|
staticprotected |
Referenced by Native.mkFpaRoundNearestTiesToEven().
|
staticprotected |
Referenced by Native.mkFpaRoundToIntegral().
|
staticprotected |
Referenced by Native.mkFpaRoundTowardNegative().
|
staticprotected |
Referenced by Native.mkFpaRoundTowardPositive().
|
staticprotected |
Referenced by Native.mkFpaRoundTowardZero().
|
staticprotected |
Referenced by Native.mkFpaRtn().
|
staticprotected |
Referenced by Native.mkFpaRtp().
|
staticprotected |
Referenced by Native.mkFpaRtz().
|
staticprotected |
Referenced by Native.mkFpaSort().
|
staticprotected |
Referenced by Native.mkFpaSort128().
|
staticprotected |
Referenced by Native.mkFpaSort16().
|
staticprotected |
Referenced by Native.mkFpaSort32().
|
staticprotected |
Referenced by Native.mkFpaSort64().
|
staticprotected |
Referenced by Native.mkFpaSortDouble().
|
staticprotected |
Referenced by Native.mkFpaSortHalf().
|
staticprotected |
Referenced by Native.mkFpaSortQuadruple().
|
staticprotected |
Referenced by Native.mkFpaSortSingle().
|
staticprotected |
Referenced by Native.mkFpaSqrt().
|
staticprotected |
Referenced by Native.mkFpaSub().
|
staticprotected |
Referenced by Native.mkFpaToFpBv().
|
staticprotected |
Referenced by Native.mkFpaToFpFloat().
|
staticprotected |
Referenced by Native.mkFpaToFpIntReal().
|
staticprotected |
Referenced by Native.mkFpaToFpReal().
|
staticprotected |
Referenced by Native.mkFpaToFpSigned().
|
staticprotected |
Referenced by Native.mkFpaToFpUnsigned().
|
staticprotected |
Referenced by Native.mkFpaToIeeeBv().
|
staticprotected |
Referenced by Native.mkFpaToReal().
|
staticprotected |
Referenced by Native.mkFpaToSbv().
|
staticprotected |
Referenced by Native.mkFpaToUbv().
|
staticprotected |
Referenced by Native.mkFpaZero().
|
staticprotected |
Referenced by Native.mkFreshConst().
|
staticprotected |
Referenced by Native.mkFreshFuncDecl().
|
staticprotected |
Referenced by Native.mkFullSet().
|
staticprotected |
Referenced by Native.mkFuncDecl().
|
staticprotected |
Referenced by Native.mkGe().
|
staticprotected |
Referenced by Native.mkGoal().
|
staticprotected |
Referenced by Native.mkGt().
|
staticprotected |
Referenced by Native.mkIff().
|
staticprotected |
Referenced by Native.mkImplies().
|
staticprotected |
Referenced by Native.mkInt().
|
staticprotected |
Referenced by Native.mkInt2bv().
|
staticprotected |
Referenced by Native.mkInt2real().
|
staticprotected |
Referenced by Native.mkInt64().
|
staticprotected |
Referenced by Native.mkIntSort().
|
staticprotected |
Referenced by Native.mkIntSymbol().
|
staticprotected |
Referenced by Native.mkIntToStr().
|
staticprotected |
Referenced by Native.mkIsInt().
|
staticprotected |
Referenced by Native.mkIte().
|
staticprotected |
Referenced by Native.mkLambda().
|
staticprotected |
Referenced by Native.mkLambdaConst().
|
staticprotected |
Referenced by Native.mkLe().
|
staticprotected |
Referenced by Native.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.mkRecFuncDecl().
|
staticprotected |
Referenced by Native.mkReComplement().
|
staticprotected |
Referenced by Native.mkReConcat().
|
staticprotected |
Referenced by Native.mkReEmpty().
|
staticprotected |
Referenced by Native.mkReFull().
|
staticprotected |
Referenced by Native.mkReIntersect().
|
staticprotected |
Referenced by Native.mkReLoop().
|
staticprotected |
Referenced by Native.mkRem().
|
staticprotected |
Referenced by Native.mkReOption().
|
staticprotected |
Referenced by Native.mkRepeat().
|
staticprotected |
Referenced by Native.mkRePlus().
|
staticprotected |
Referenced by Native.mkReRange().
|
staticprotected |
Referenced by Native.mkReSort().
|
staticprotected |
Referenced by Native.mkReStar().
|
staticprotected |
Referenced by Native.mkReUnion().
|
staticprotected |
Referenced by Native.mkRotateLeft().
|
staticprotected |
Referenced by Native.mkRotateRight().
|
staticprotected |
Referenced by Native.mkSelect().
|
staticprotected |
Referenced by Native.mkSelectN().
|
staticprotected |
Referenced by Native.mkSeqAt().
|
staticprotected |
Referenced by Native.mkSeqConcat().
|
staticprotected |
Referenced by Native.mkSeqContains().
|
staticprotected |
Referenced by Native.mkSeqEmpty().
|
staticprotected |
Referenced by Native.mkSeqExtract().
|
staticprotected |
Referenced by Native.mkSeqIndex().
|
staticprotected |
Referenced by Native.mkSeqInRe().
|
staticprotected |
Referenced by Native.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.optimizeGetUnsatCore().
|
staticprotected |
Referenced by Native.optimizeGetUpper().
|
staticprotected |
Referenced by Native.optimizeGetUpperAsVector().
|
staticprotected |
Referenced by Native.optimizeIncRef().
|
staticprotected |
Referenced by Native.optimizeMaximize().
|
staticprotected |
Referenced by Native.optimizeMinimize().
|
staticprotected |
Referenced by Native.optimizePop().
|
staticprotected |
Referenced by Native.optimizePush().
|
staticprotected |
Referenced by Native.optimizeSetParams().
|
staticprotected |
Referenced by Native.optimizeToString().
|
staticprotected |
Referenced by Native.paramDescrsDecRef().
|
staticprotected |
Referenced by Native.paramDescrsGetDocumentation().
|
staticprotected |
Referenced by Native.paramDescrsGetKind().
|
staticprotected |
Referenced by Native.paramDescrsGetName().
|
staticprotected |
Referenced by Native.paramDescrsIncRef().
|
staticprotected |
Referenced by Native.paramDescrsSize().
|
staticprotected |
Referenced by Native.paramDescrsToString().
|
staticprotected |
Referenced by Native.paramsDecRef().
|
staticprotected |
Referenced by Native.paramsIncRef().
|
staticprotected |
Referenced by Native.paramsSetBool().
|
staticprotected |
Referenced by Native.paramsSetDouble().
|
staticprotected |
Referenced by Native.paramsSetSymbol().
|
staticprotected |
Referenced by Native.paramsSetUint().
|
staticprotected |
Referenced by Native.paramsToString().
|
staticprotected |
Referenced by Native.paramsValidate().
|
staticprotected |
Referenced by Native.parseSmtlib2File().
|
staticprotected |
Referenced by Native.parseSmtlib2String().
|
staticprotected |
Referenced by Native.patternToAst().
|
staticprotected |
Referenced by Native.patternToString().
|
staticprotected |
Referenced by Native.polynomialSubresultants().
|
staticprotected |
Referenced by Native.probeAnd().
|
staticprotected |
Referenced by Native.probeApply().
|
staticprotected |
Referenced by Native.probeConst().
|
staticprotected |
Referenced by Native.probeDecRef().
|
staticprotected |
Referenced by Native.probeEq().
|
staticprotected |
Referenced by Native.probeGe().
|
staticprotected |
Referenced by Native.probeGetDescr().
|
staticprotected |
Referenced by Native.probeGt().
|
staticprotected |
Referenced by Native.probeIncRef().
|
staticprotected |
Referenced by Native.probeLe().
|
staticprotected |
Referenced by Native.probeLt().
|
staticprotected |
Referenced by Native.probeNot().
|
staticprotected |
Referenced by Native.probeOr().
|
staticprotected |
Referenced by Native.qeLite().
|
staticprotected |
Referenced by Native.qeModelProject().
|
staticprotected |
Referenced by Native.qeModelProjectSkolem().
|
staticprotected |
Referenced by Native.queryConstructor().
|
staticprotected |
Referenced by Native.rcfAdd().
|
staticprotected |
Referenced by Native.rcfDel().
|
staticprotected |
Referenced by Native.rcfDiv().
|
staticprotected |
Referenced by Native.rcfEq().
|
staticprotected |
Referenced by Native.rcfGe().
|
staticprotected |
Referenced by Native.rcfGetNumeratorDenominator().
|
staticprotected |
Referenced by Native.rcfGt().
|
staticprotected |
Referenced by Native.rcfInv().
|
staticprotected |
Referenced by Native.rcfLe().
|
staticprotected |
Referenced by Native.rcfLt().
|
staticprotected |
Referenced by Native.rcfMkE().
|
staticprotected |
Referenced by Native.rcfMkInfinitesimal().
|
staticprotected |
Referenced by Native.rcfMkPi().
|
staticprotected |
Referenced by Native.rcfMkRational().
|
staticprotected |
Referenced by Native.rcfMkRoots().
|
staticprotected |
Referenced by Native.rcfMkSmallInt().
|
staticprotected |
Referenced by Native.rcfMul().
|
staticprotected |
Referenced by Native.rcfNeg().
|
staticprotected |
Referenced by Native.rcfNeq().
|
staticprotected |
Referenced by Native.rcfNumToDecimalString().
|
staticprotected |
Referenced by Native.rcfNumToString().
|
staticprotected |
Referenced by Native.rcfPower().
|
staticprotected |
Referenced by Native.rcfSub().
|
staticprotected |
Referenced by Native.resetMemory().
|
staticprotected |
Referenced by Native.setAstPrintMode().
|
staticprotected |
Referenced by Native.setError().
|
staticprotected |
Referenced by Native.setParamValue().
|
staticprotected |
Referenced by Native.simplify().
|
staticprotected |
Referenced by Native.simplifyEx().
|
staticprotected |
Referenced by Native.simplifyGetHelp().
|
staticprotected |
Referenced by Native.simplifyGetParamDescrs().
|
staticprotected |
Referenced by Native.solverAssert().
|
staticprotected |
Referenced by Native.solverAssertAndTrack().
|
staticprotected |
Referenced by Native.solverCheck().
|
staticprotected |
Referenced by Native.solverCheckAssumptions().
|
staticprotected |
Referenced by Native.solverCube().
|
staticprotected |
Referenced by Native.solverDecRef().
|
staticprotected |
Referenced by Native.solverFromFile().
|
staticprotected |
Referenced by Native.solverFromString().
|
staticprotected |
Referenced by Native.solverGetAssertions().
|
staticprotected |
Referenced by Native.solverGetConsequences().
|
staticprotected |
Referenced by Native.solverGetHelp().
|
staticprotected |
Referenced by Native.solverGetModel().
|
staticprotected |
Referenced by Native.solverGetNonUnits().
|
staticprotected |
Referenced by Native.solverGetNumScopes().
|
staticprotected |
Referenced by Native.solverGetParamDescrs().
|
staticprotected |
Referenced by Native.solverGetProof().
|
staticprotected |
Referenced by Native.solverGetReasonUnknown().
|
staticprotected |
Referenced by Native.solverGetStatistics().
|
staticprotected |
Referenced by Native.solverGetUnits().
|
staticprotected |
Referenced by Native.solverGetUnsatCore().
|
staticprotected |
Referenced by Native.solverImportModelConverter().
|
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().
|
inlinestatic |
Definition at line 764 of file Native.java.
Referenced by Context.interrupt().
|
inlinestatic |
Definition at line 2999 of file Native.java.
Referenced by Expr.isAlgebraicNumber().
|
inlinestatic |
Definition at line 2981 of file Native.java.
Referenced by Expr.isArray(), Expr.isFiniteDomain(), and Expr.isRelation().
|
inlinestatic |
Definition at line 3492 of file Native.java.
Referenced by Model.getFuncInterp().
|
inlinestatic |
Definition at line 2918 of file Native.java.
Referenced by AST.equals().
|
inlinestatic |
Definition at line 2729 of file Native.java.
Referenced by FuncDecl.equals().
|
inlinestatic |
Definition at line 2531 of file Native.java.
Referenced by Sort.equals(), and Expr.isBool().
|
inlinestatic |
Definition at line 3197 of file Native.java.
|
inlinestatic |
Definition at line 2990 of file Native.java.
Referenced by Expr.isNumeral().
|
inlinestatic |
Definition at line 3188 of file Native.java.
Referenced by Quantifier.isExistential().
|
inlinestatic |
Definition at line 3179 of file Native.java.
Referenced by Quantifier.isUniversal().
|
inlinestatic |
Definition at line 2081 of file Native.java.
|
inlinestatic |
Definition at line 2063 of file Native.java.
|
inlinestatic |
Definition at line 2117 of file Native.java.
Referenced by Expr.isString().
|
inlinestatic |
Definition at line 2099 of file Native.java.
|
inlinestatic |
Definition at line 2954 of file Native.java.
Referenced by Expr.isWellSorted().
|
inlinestatic |
Definition at line 1244 of file Native.java.
Referenced by Context.mkAdd().
|
inlinestatic |
Definition at line 1226 of file Native.java.
Referenced by Context.mkAnd().
|
inlinestatic |
Definition at line 1092 of file Native.java.
|
inlinestatic |
Definition at line 1865 of file Native.java.
Referenced by Context.mkTermArray().
|
inlinestatic |
Definition at line 1982 of file Native.java.
Referenced by Context.mkArrayExt().
|
inlinestatic |
Definition at line 979 of file Native.java.
|
inlinestatic |
Definition at line 988 of file Native.java.
|
inlinestatic |
Definition at line 1874 of file Native.java.
|
inlinestatic |
Definition at line 4797 of file Native.java.
|
inlinestatic |
Definition at line 4712 of file Native.java.
|
inlinestatic |
Definition at line 2684 of file Native.java.
Referenced by Context.mkAtLeast().
|
inlinestatic |
Definition at line 2675 of file Native.java.
Referenced by Context.mkAtMost().
|
inlinestatic |
Definition at line 934 of file Native.java.
Referenced by Expr.isBool().
|
inlinestatic |
Definition at line 2378 of file Native.java.
Referenced by Context.mkBound().
|
inlinestatic |
Definition at line 1730 of file Native.java.
Referenced by Context.mkBV2Int().
|
inlinestatic |
Definition at line 1469 of file Native.java.
Referenced by Context.mkBVAdd().
|
inlinestatic |
Definition at line 1739 of file Native.java.
Referenced by Context.mkBVAddNoOverflow().
|
inlinestatic |
Definition at line 1748 of file Native.java.
Referenced by Context.mkBVAddNoUnderflow().
|
inlinestatic |
Definition at line 1406 of file Native.java.
Referenced by Context.mkBVAND().
|
inlinestatic |
Definition at line 1676 of file Native.java.
Referenced by Context.mkBVASHR().
|
inlinestatic |
Definition at line 1667 of file Native.java.
Referenced by Context.mkBVLSHR().
|
inlinestatic |
Definition at line 1487 of file Native.java.
Referenced by Context.mkBVMul().
|
inlinestatic |
Definition at line 1793 of file Native.java.
Referenced by Context.mkBVMulNoOverflow().
|
inlinestatic |
Definition at line 1802 of file Native.java.
Referenced by Context.mkBVMulNoUnderflow().
|
inlinestatic |
Definition at line 1433 of file Native.java.
Referenced by Context.mkBVNAND().
|
inlinestatic |
Definition at line 1460 of file Native.java.
Referenced by Context.mkBVNeg().
|
inlinestatic |
Definition at line 1784 of file Native.java.
Referenced by Context.mkBVNegNoOverflow().
|
inlinestatic |
Definition at line 1442 of file Native.java.
Referenced by Context.mkBVNOR().
|
inlinestatic |
Definition at line 1379 of file Native.java.
Referenced by Context.mkBVNot().
|
inlinestatic |
Definition at line 2045 of file Native.java.
|
inlinestatic |
Definition at line 1415 of file Native.java.
Referenced by Context.mkBVOR().
|
inlinestatic |
Definition at line 1388 of file Native.java.
Referenced by Context.mkBVRedAND().
|
inlinestatic |
Definition at line 1397 of file Native.java.
Referenced by Context.mkBVRedOR().
|
inlinestatic |
Definition at line 1505 of file Native.java.
Referenced by Context.mkBVSDiv().
|
inlinestatic |
Definition at line 1775 of file Native.java.
Referenced by Context.mkBVSDivNoOverflow().
|
inlinestatic |
Definition at line 1586 of file Native.java.
Referenced by Context.mkBVSGE().
|
inlinestatic |
Definition at line 1604 of file Native.java.
Referenced by Context.mkBVSGT().
|
inlinestatic |
Definition at line 1658 of file Native.java.
Referenced by Context.mkBVSHL().
|
inlinestatic |
Definition at line 1568 of file Native.java.
Referenced by Context.mkBVSLE().
|
inlinestatic |
Definition at line 1550 of file Native.java.
Referenced by Context.mkBVSLT().
|
inlinestatic |
Definition at line 1532 of file Native.java.
Referenced by Context.mkBVSMod().
|
inlinestatic |
Definition at line 961 of file Native.java.
Referenced by Context.mkBitVecSort().
|
inlinestatic |
Definition at line 1523 of file Native.java.
Referenced by Context.mkBVSRem().
|
inlinestatic |
Definition at line 1478 of file Native.java.
Referenced by Context.mkBVSub().
|
inlinestatic |
Definition at line 1757 of file Native.java.
Referenced by Context.mkBVSubNoOverflow().
|
inlinestatic |
Definition at line 1766 of file Native.java.
Referenced by Context.mkBVSubNoUnderflow().
|
inlinestatic |
Definition at line 1496 of file Native.java.
Referenced by Context.mkBVUDiv().
|
inlinestatic |
Definition at line 1577 of file Native.java.
Referenced by Context.mkBVUGE().
|
inlinestatic |
Definition at line 1595 of file Native.java.
Referenced by Context.mkBVUGT().
|
inlinestatic |
Definition at line 1559 of file Native.java.
Referenced by Context.mkBVULE().
|
inlinestatic |
Definition at line 1541 of file Native.java.
Referenced by Context.mkBVULT().
|
inlinestatic |
Definition at line 1514 of file Native.java.
Referenced by Context.mkBVURem().
|
inlinestatic |
Definition at line 1451 of file Native.java.
Referenced by Context.mkBVXNOR().
|
inlinestatic |
Definition at line 1424 of file Native.java.
Referenced by Context.mkBVXOR().
|
inlinestatic |
Definition at line 1613 of file Native.java.
Referenced by Context.mkConcat().
|
inlinestatic |
Definition at line 703 of file Native.java.
Referenced by Context.Context().
|
inlinestatic |
Definition at line 1101 of file Native.java.
Referenced by Context.mkConst().
|
inlinestatic |
Definition at line 1847 of file Native.java.
Referenced by Context.mkConstArray().
|
inlinestatic |
Definition at line 1024 of file Native.java.
|
inlinestatic |
Definition at line 1050 of file Native.java.
|
inlinestatic |
Definition at line 719 of file Native.java.
|
inlinestatic |
Definition at line 727 of file Native.java.
Referenced by Context.Context().
|
inlinestatic |
Definition at line 1041 of file Native.java.
|
inlinestatic |
Definition at line 1067 of file Native.java.
Referenced by Context.mkDatatypeSorts().
|
inlinestatic |
Definition at line 1172 of file Native.java.
Referenced by Context.mkDistinct().
|
inlinestatic |
Definition at line 1280 of file Native.java.
Referenced by Context.mkDiv().
|
inlinestatic |
Definition at line 1892 of file Native.java.
Referenced by Context.mkEmptySet().
|
inlinestatic |
Definition at line 1006 of file Native.java.
|
inlinestatic |
Definition at line 1163 of file Native.java.
Referenced by Context.mkEq().
|
inlinestatic |
Definition at line 2396 of file Native.java.
|
inlinestatic |
Definition at line 2432 of file Native.java.
|
inlinestatic |
Definition at line 1622 of file Native.java.
Referenced by Context.mkExtract().
|
inlinestatic |
Definition at line 1703 of file Native.java.
Referenced by Context.mkBVRotateLeft().
|
inlinestatic |
Definition at line 1712 of file Native.java.
Referenced by Context.mkBVRotateRight().
|
inlinestatic |
Definition at line 1154 of file Native.java.
Referenced by Context.mkFalse().
|
inlinestatic |
Definition at line 970 of file Native.java.
|
inlinestatic |
Definition at line 5276 of file Native.java.
|
inlinestatic |
Definition at line 2387 of file Native.java.
|
inlinestatic |
Definition at line 2423 of file Native.java.
|
inlinestatic |
Definition at line 5994 of file Native.java.
Referenced by Context.mkFPAbs().
|
inlinestatic |
Definition at line 6012 of file Native.java.
Referenced by Context.mkFPAdd().
|
inlinestatic |
Definition at line 6039 of file Native.java.
Referenced by Context.mkFPDiv().
|
inlinestatic |
Definition at line 6138 of file Native.java.
Referenced by Context.mkFPEq().
|
inlinestatic |
Definition at line 6048 of file Native.java.
Referenced by Context.mkFPFMA().
|
inlinestatic |
Definition at line 5940 of file Native.java.
Referenced by Context.mkFP().
|
inlinestatic |
Definition at line 6120 of file Native.java.
Referenced by Context.mkFPGEq().
|
inlinestatic |
Definition at line 6129 of file Native.java.
Referenced by Context.mkFPGt().
|
inlinestatic |
Definition at line 5922 of file Native.java.
Referenced by Context.mkFPInf().
|
inlinestatic |
Definition at line 6174 of file Native.java.
Referenced by Context.mkFPIsInfinite().
|
inlinestatic |
Definition at line 6183 of file Native.java.
Referenced by Context.mkFPIsNaN().
|
inlinestatic |
Definition at line 6192 of file Native.java.
Referenced by Context.mkFPIsNegative().
|
inlinestatic |
Definition at line 6147 of file Native.java.
Referenced by Context.mkFPIsNormal().
|
inlinestatic |
Definition at line 6201 of file Native.java.
Referenced by Context.mkFPIsPositive().
|
inlinestatic |
Definition at line 6156 of file Native.java.
Referenced by Context.mkFPIsSubnormal().
|
inlinestatic |
Definition at line 6165 of file Native.java.
Referenced by Context.mkFPIsZero().
|
inlinestatic |
Definition at line 6102 of file Native.java.
Referenced by Context.mkFPLEq().
|
inlinestatic |
Definition at line 6111 of file Native.java.
Referenced by Context.mkFPLt().
|
inlinestatic |
Definition at line 6093 of file Native.java.
Referenced by Context.mkFPMax().
|
inlinestatic |
Definition at line 6084 of file Native.java.
Referenced by Context.mkFPMin().
|
inlinestatic |
Definition at line 6030 of file Native.java.
Referenced by Context.mkFPMul().
|
inlinestatic |
Definition at line 5913 of file Native.java.
Referenced by Context.mkFPNaN().
|
inlinestatic |
Definition at line 6003 of file Native.java.
Referenced by Context.mkFPNeg().
|
inlinestatic |
Definition at line 5958 of file Native.java.
Referenced by Context.mkFPNumeral().
|
inlinestatic |
Definition at line 5949 of file Native.java.
Referenced by Context.mkFPNumeral().
|
inlinestatic |
Definition at line 5967 of file Native.java.
Referenced by Context.mkFPNumeral().
|
inlinestatic |
Definition at line 5985 of file Native.java.
Referenced by Context.mkFPNumeral().
|
inlinestatic |
Definition at line 5976 of file Native.java.
Referenced by Context.mkFPNumeral().
|
inlinestatic |
Definition at line 6066 of file Native.java.
Referenced by Context.mkFPRem().
|
inlinestatic |
Definition at line 5769 of file Native.java.
Referenced by Context.mkFPRNA().
|
inlinestatic |
Definition at line 5751 of file Native.java.
Referenced by Context.mkFPRNE().
|
inlinestatic |
Definition at line 5733 of file Native.java.
Referenced by FPRMSort.FPRMSort().
|
inlinestatic |
Definition at line 5760 of file Native.java.
Referenced by Context.mkFPRoundNearestTiesToAway().
|
inlinestatic |
Definition at line 5742 of file Native.java.
Referenced by Context.mkFPRoundNearestTiesToEven().
|
inlinestatic |
Definition at line 6075 of file Native.java.
Referenced by Context.mkFPRoundToIntegral().
|
inlinestatic |
Definition at line 5796 of file Native.java.
Referenced by Context.mkFPRoundTowardNegative().
|
inlinestatic |
Definition at line 5778 of file Native.java.
Referenced by Context.mkFPRoundTowardPositive().
|
inlinestatic |
Definition at line 5814 of file Native.java.
Referenced by Context.mkFPRoundTowardZero().
|
inlinestatic |
Definition at line 5805 of file Native.java.
Referenced by Context.mkFPRTN().
|
inlinestatic |
Definition at line 5787 of file Native.java.
Referenced by Context.mkFPRTP().
|
inlinestatic |
Definition at line 5823 of file Native.java.
Referenced by Context.mkFPRTZ().
|
inlinestatic |
Definition at line 5832 of file Native.java.
Referenced by FPSort.FPSort().
|
inlinestatic |
Definition at line 5904 of file Native.java.
Referenced by Context.mkFPSort128().
|
inlinestatic |
Definition at line 5850 of file Native.java.
Referenced by Context.mkFPSort16().
|
inlinestatic |
Definition at line 5868 of file Native.java.
Referenced by Context.mkFPSort32().
|
inlinestatic |
Definition at line 5886 of file Native.java.
Referenced by Context.mkFPSort64().
|
inlinestatic |
Definition at line 5877 of file Native.java.
Referenced by Context.mkFPSortDouble().
|
inlinestatic |
Definition at line 5841 of file Native.java.
Referenced by Context.mkFPSortHalf().
|
inlinestatic |
Definition at line 5895 of file Native.java.
Referenced by Context.mkFPSortQuadruple().
|
inlinestatic |
Definition at line 5859 of file Native.java.
Referenced by Context.mkFPSortSingle().
|
inlinestatic |
Definition at line 6057 of file Native.java.
Referenced by Context.mkFPSqrt().
|
inlinestatic |
Definition at line 6021 of file Native.java.
Referenced by Context.mkFPSub().
|
inlinestatic |
Definition at line 6210 of file Native.java.
Referenced by Context.mkFPToFP().
|
inlinestatic |
Definition at line 6219 of file Native.java.
Referenced by Context.mkFPToFP().
|
inlinestatic |
Definition at line 6444 of file Native.java.
Referenced by Context.mkFPToFP().
|
inlinestatic |
Definition at line 6228 of file Native.java.
Referenced by Context.mkFPToFP().
|
inlinestatic |
Definition at line 6237 of file Native.java.
Referenced by Context.mkFPToFP().
|
inlinestatic |
Definition at line 6246 of file Native.java.
Referenced by Context.mkFPToFP().
|
inlinestatic |
Definition at line 6435 of file Native.java.
Referenced by Context.mkFPToIEEEBV().
|
inlinestatic |
Definition at line 6273 of file Native.java.
Referenced by Context.mkFPToReal().
|
inlinestatic |
Definition at line 6264 of file Native.java.
Referenced by Context.mkFPToBV().
|
inlinestatic |
Definition at line 6255 of file Native.java.
Referenced by Context.mkFPToBV().
|
inlinestatic |
Definition at line 5931 of file Native.java.
Referenced by Context.mkFPZero().
|
inlinestatic |
Definition at line 1119 of file Native.java.
Referenced by Context.mkFreshConst().
|
inlinestatic |
Definition at line 1110 of file Native.java.
|
inlinestatic |
Definition at line 1901 of file Native.java.
Referenced by Context.mkFullSet().
|
inlinestatic |
Definition at line 1083 of file Native.java.
|
inlinestatic |
Definition at line 1343 of file Native.java.
Referenced by Context.mkGe().
|
inlinestatic |
Definition at line 3802 of file Native.java.
|
inlinestatic |
Definition at line 1334 of file Native.java.
Referenced by Context.mkGt().
|
inlinestatic |
Definition at line 1199 of file Native.java.
Referenced by Context.mkIff().
|
inlinestatic |
Definition at line 1208 of file Native.java.
Referenced by Context.mkImplies().
|
inlinestatic |
Definition at line 2009 of file Native.java.
Referenced by Context.mkInt(), Context.mkNumeral(), and Context.mkReal().
|
inlinestatic |
Definition at line 1721 of file Native.java.
Referenced by Context.mkInt2BV().
|
inlinestatic |
Definition at line 1352 of file Native.java.
Referenced by Context.mkInt2Real().
|
inlinestatic |
Definition at line 2027 of file Native.java.
Referenced by Context.mkInt(), Context.mkNumeral(), and Context.mkReal().
|
inlinestatic |
Definition at line 943 of file Native.java.
|
inlinestatic |
Definition at line 907 of file Native.java.
|
inlinestatic |
Definition at line 2243 of file Native.java.
Referenced by Context.intToString().
|
inlinestatic |
Definition at line 1370 of file Native.java.
Referenced by Context.mkIsInteger().
|
inlinestatic |
Definition at line 1190 of file Native.java.
Referenced by Context.mkITE().
|
inlinestatic |
Definition at line 2459 of file Native.java.
Referenced by Lambda.of().
|
inlinestatic |
Definition at line 2468 of file Native.java.
Referenced by Lambda.of().
|
inlinestatic |
Definition at line 1325 of file Native.java.
Referenced by Context.mkLe().
|
inlinestatic |
Definition at line 1015 of file Native.java.
|
inlinestatic |
Definition at line 1316 of file Native.java.
Referenced by Context.mkLt().
|
inlinestatic |
Definition at line 1856 of file Native.java.
Referenced by Context.mkMap().
|
inlinestatic |
Definition at line 1289 of file Native.java.
Referenced by Context.mkMod().
|
inlinestatic |
Definition at line 3359 of file Native.java.
|
inlinestatic |
Definition at line 1253 of file Native.java.
Referenced by Context.mkMul().
|
inlinestatic |
Definition at line 1181 of file Native.java.
Referenced by Context.mkNot().
|
inlinestatic |
Definition at line 1991 of file Native.java.
Referenced by Context.mkInt(), Context.mkNumeral(), and Context.mkReal().
|
inlinestatic |
Definition at line 5507 of file Native.java.
|
inlinestatic |
Definition at line 1235 of file Native.java.
Referenced by Context.mkOr().
|
inlinestatic |
Definition at line 772 of file Native.java.
|
inlinestatic |
Definition at line 2369 of file Native.java.
Referenced by Context.mkPattern().
|
inlinestatic |
Definition at line 2711 of file Native.java.
Referenced by Context.mkPBEq().
|
inlinestatic |
Definition at line 2702 of file Native.java.
Referenced by Context.mkPBGe().
|
inlinestatic |
Definition at line 2693 of file Native.java.
Referenced by Context.mkPBLe().
|
inlinestatic |
Definition at line 1307 of file Native.java.
Referenced by Context.mkPower().
|
inlinestatic |
Definition at line 3976 of file Native.java.
|
inlinestatic |
Definition at line 2405 of file Native.java.
Referenced by Quantifier.of().
|
inlinestatic |
Definition at line 2441 of file Native.java.
Referenced by Quantifier.of().
|
inlinestatic |
Definition at line 2450 of file Native.java.
Referenced by Quantifier.of().
|
inlinestatic |
Definition at line 2414 of file Native.java.
Referenced by Quantifier.of().
|
inlinestatic |
Definition at line 2000 of file Native.java.
Referenced by Context.mkReal().
|
inlinestatic |
Definition at line 1361 of file Native.java.
Referenced by Context.mkReal2Int().
|
inlinestatic |
Definition at line 952 of file Native.java.
|
inlinestatic |
Definition at line 1128 of file Native.java.
|
inlinestatic |
Definition at line 2342 of file Native.java.
Referenced by Context.mkComplement().
|
inlinestatic |
Definition at line 2306 of file Native.java.
Referenced by Context.mkConcat().
|
inlinestatic |
Definition at line 2351 of file Native.java.
Referenced by Context.mkEmptyRe().
|
inlinestatic |
Definition at line 2360 of file Native.java.
Referenced by Context.mkFullRe().
|
inlinestatic |
Definition at line 2333 of file Native.java.
Referenced by Context.mkIntersect().
|
inlinestatic |
Definition at line 2324 of file Native.java.
Referenced by Context.mkLoop().
|
inlinestatic |
Definition at line 1298 of file Native.java.
Referenced by Context.mkRem().
|
inlinestatic |
Definition at line 2288 of file Native.java.
Referenced by Context.mkOption().
|
inlinestatic |
Definition at line 1649 of file Native.java.
Referenced by Context.mkRepeat().
|
inlinestatic |
Definition at line 2270 of file Native.java.
Referenced by Context.mkPlus().
|
inlinestatic |
Definition at line 2315 of file Native.java.
Referenced by Context.mkRange().
|
inlinestatic |
Definition at line 2072 of file Native.java.
Referenced by Context.mkReSort().
|
inlinestatic |
Definition at line 2279 of file Native.java.
Referenced by Context.mkStar().
|
inlinestatic |
Definition at line 2297 of file Native.java.
Referenced by Context.mkUnion().
|
inlinestatic |
Definition at line 1685 of file Native.java.
Referenced by Context.mkBVRotateLeft().
|
inlinestatic |
Definition at line 1694 of file Native.java.
Referenced by Context.mkBVRotateRight().
|
inlinestatic |
Definition at line 1811 of file Native.java.
Referenced by Context.mkSelect().
|
inlinestatic |
Definition at line 1820 of file Native.java.
Referenced by Context.mkSelect().
|
inlinestatic |
Definition at line 2207 of file Native.java.
Referenced by Context.mkAt().
|
inlinestatic |
Definition at line 2153 of file Native.java.
Referenced by Context.mkConcat().
|
inlinestatic |
Definition at line 2180 of file Native.java.
Referenced by Context.mkContains().
|
inlinestatic |
Definition at line 2135 of file Native.java.
Referenced by Context.mkEmptySeq().
|
inlinestatic |
Definition at line 2189 of file Native.java.
Referenced by Context.mkExtract().
|
inlinestatic |
Definition at line 2225 of file Native.java.
Referenced by Context.mkIndexOf().
|
inlinestatic |
Definition at line 2261 of file Native.java.
Referenced by Context.mkInRe().
|
inlinestatic |
Definition at line 2216 of file Native.java.
Referenced by Context.mkLength().
|
inlinestatic |
Definition at line 2162 of file Native.java.
Referenced by Context.mkPrefixOf().
|
inlinestatic |
Definition at line 2198 of file Native.java.
Referenced by Context.mkReplace().
|
inlinestatic |
Definition at line 2054 of file Native.java.
Referenced by Context.mkSeqSort().
|
inlinestatic |
Definition at line 2171 of file Native.java.
Referenced by Context.mkSuffixOf().
|
inlinestatic |
Definition at line 2252 of file Native.java.
Referenced by Context.mkToRe().
|
inlinestatic |
Definition at line 2144 of file Native.java.
Referenced by Context.mkUnit().
|
inlinestatic |
Definition at line 1910 of file Native.java.
Referenced by Context.mkSetAdd().
|
inlinestatic |
Definition at line 1955 of file Native.java.
Referenced by Context.mkSetComplement().
|
inlinestatic |
Definition at line 1919 of file Native.java.
Referenced by Context.mkSetDel().
|
inlinestatic |
Definition at line 1946 of file Native.java.
Referenced by Context.mkSetDifference().
|
inlinestatic |
Definition at line 1937 of file Native.java.
Referenced by Context.mkSetIntersection().
|
inlinestatic |
Definition at line 1964 of file Native.java.
Referenced by Context.mkSetMembership().
|
inlinestatic |
Definition at line 1883 of file Native.java.
|
inlinestatic |
Definition at line 1973 of file Native.java.
Referenced by Context.mkSetSubset().
|
inlinestatic |
Definition at line 1928 of file Native.java.
Referenced by Context.mkSetUnion().
|
inlinestatic |
Definition at line 1631 of file Native.java.
Referenced by Context.mkSignExt().
|
inlinestatic |
Definition at line 4350 of file Native.java.
Referenced by Context.mkSimpleSolver().
|
inlinestatic |
Definition at line 4341 of file Native.java.
Referenced by Context.mkSolver().
|
inlinestatic |
Definition at line 4359 of file Native.java.
Referenced by Context.mkSolver().
|
inlinestatic |
Definition at line 4368 of file Native.java.
Referenced by Context.mkSolver().
|
inlinestatic |
Definition at line 1829 of file Native.java.
Referenced by Context.mkStore().
|
inlinestatic |
Definition at line 1838 of file Native.java.
Referenced by Context.mkStore().
|
inlinestatic |
Definition at line 2108 of file Native.java.
Referenced by Context.mkString().
|
inlinestatic |
Definition at line 2090 of file Native.java.
Referenced by Context.mkStringSort().
|
inlinestatic |
Definition at line 916 of file Native.java.
|
inlinestatic |
Definition at line 2234 of file Native.java.
Referenced by Context.stringToInt().
|
inlinestatic |
Definition at line 1262 of file Native.java.
Referenced by Context.mkSub().
|
inlinestatic |
Definition at line 3951 of file Native.java.
|
inlinestatic |
Definition at line 1145 of file Native.java.
Referenced by Context.mkTrue().
|
inlinestatic |
Definition at line 997 of file Native.java.
|
inlinestatic |
Definition at line 1271 of file Native.java.
Referenced by Context.mkUnaryMinus().
|
inlinestatic |
Definition at line 925 of file Native.java.
|
inlinestatic |
Definition at line 2018 of file Native.java.
|
inlinestatic |
Definition at line 2036 of file Native.java.
|
inlinestatic |
Definition at line 1217 of file Native.java.
Referenced by Context.mkXor().
|
inlinestatic |
Definition at line 1640 of file Native.java.
Referenced by Context.mkZeroExt().
|
inlinestatic |
Definition at line 3376 of file Native.java.
|
inlinestatic |
Definition at line 3384 of file Native.java.
Referenced by Model.eval().
|
inlinestatic |
Definition at line 6524 of file Native.java.
|
inlinestatic |
Definition at line 3429 of file Native.java.
Referenced by Model.getConstDecls(), and Model.getDecls().
|
inlinestatic |
Definition at line 3393 of file Native.java.
Referenced by Model.getConstInterp(), and Model.getFuncInterp().
|
inlinestatic |
Definition at line 3447 of file Native.java.
Referenced by Model.getDecls(), and Model.getFuncDecls().
|
inlinestatic |
Definition at line 3411 of file Native.java.
Referenced by Model.getFuncInterp().
|
inlinestatic |
Definition at line 3420 of file Native.java.
Referenced by Model.getNumConsts().
|
inlinestatic |
Definition at line 3438 of file Native.java.
Referenced by Model.getNumFuncs().
|
inlinestatic |
Definition at line 3456 of file Native.java.
Referenced by Model.getNumSorts().
|
inlinestatic |
Definition at line 3465 of file Native.java.
Referenced by Model.getSorts().
|
inlinestatic |
Definition at line 3474 of file Native.java.
Referenced by Model.getSortUniverse().
|
inlinestatic |
Definition at line 3402 of file Native.java.
|
inlinestatic |
Definition at line 3368 of file Native.java.
|
inlinestatic |
Definition at line 3703 of file Native.java.
Referenced by Model.toString().
|
inlinestatic |
Definition at line 3483 of file Native.java.
|
inlinestatic |
Definition at line 3638 of file Native.java.
Referenced by Log.open().
|
inlinestatic |
Definition at line 5532 of file Native.java.
Referenced by Optimize.Assert().
|
inlinestatic |
Definition at line 5540 of file Native.java.
Referenced by Optimize.AssertSoft().
|
inlinestatic |
Definition at line 5583 of file Native.java.
Referenced by Optimize.Check().
|
inlinestatic |
Definition at line 5524 of file Native.java.
|
inlinestatic |
Definition at line 5689 of file Native.java.
Referenced by Optimize.fromFile().
|
inlinestatic |
Definition at line 5681 of file Native.java.
Referenced by Optimize.fromString().
|
inlinestatic |
Definition at line 5715 of file Native.java.
Referenced by Optimize.getAssertions().
|
inlinestatic |
Definition at line 5697 of file Native.java.
Referenced by Optimize.getHelp().
|
inlinestatic |
Definition at line 5636 of file Native.java.
|
inlinestatic |
Definition at line 5654 of file Native.java.
|
inlinestatic |
Definition at line 5601 of file Native.java.
Referenced by Optimize.getModel().
|
inlinestatic |
Definition at line 5724 of file Native.java.
Referenced by Optimize.getObjectives().
|
inlinestatic |
Definition at line 5627 of file Native.java.
Referenced by Optimize.getParameterDescriptions().
|
inlinestatic |
Definition at line 5592 of file Native.java.
Referenced by Optimize.getReasonUnknown().
|
inlinestatic |
Definition at line 5706 of file Native.java.
Referenced by Optimize.getStatistics().
|
inlinestatic |
Definition at line 5610 of file Native.java.
Referenced by Optimize.getUnsatCore().
|
inlinestatic |
Definition at line 5645 of file Native.java.
|
inlinestatic |
Definition at line 5663 of file Native.java.
|
inlinestatic |
Definition at line 5516 of file Native.java.
|
inlinestatic |
Definition at line 5549 of file Native.java.
Referenced by Optimize.MkMaximize().
|
inlinestatic |
Definition at line 5558 of file Native.java.
Referenced by Optimize.MkMinimize().
|
inlinestatic |
Definition at line 5575 of file Native.java.
Referenced by Optimize.Pop().
|
inlinestatic |
Definition at line 5567 of file Native.java.
Referenced by Optimize.Push().
|
inlinestatic |
Definition at line 5619 of file Native.java.
Referenced by Optimize.setParameters().
|
inlinestatic |
Definition at line 5672 of file Native.java.
Referenced by Optimize.toString().
|
inlinestatic |
Definition at line 854 of file Native.java.
|
inlinestatic |
Definition at line 889 of file Native.java.
Referenced by ParamDescrs.getDocumentation().
|
inlinestatic |
Definition at line 862 of file Native.java.
Referenced by ParamDescrs.getKind().
|
inlinestatic |
Definition at line 880 of file Native.java.
Referenced by ParamDescrs.getNames().
|
inlinestatic |
Definition at line 846 of file Native.java.
|
inlinestatic |
Definition at line 871 of file Native.java.
Referenced by ParamDescrs.getNames(), and ParamDescrs.size().
|
inlinestatic |
Definition at line 898 of file Native.java.
Referenced by ParamDescrs.toString().
|
inlinestatic |
Definition at line 789 of file Native.java.
|
inlinestatic |
Definition at line 781 of file Native.java.
|
inlinestatic |
Definition at line 797 of file Native.java.
Referenced by Params.add().
|
inlinestatic |
Definition at line 813 of file Native.java.
Referenced by Params.add().
|
inlinestatic |
Definition at line 821 of file Native.java.
Referenced by Params.add().
|
inlinestatic |
Definition at line 805 of file Native.java.
Referenced by Params.add().
|
inlinestatic |
Definition at line 829 of file Native.java.
Referenced by Params.toString().
|
inlinestatic |
Definition at line 838 of file Native.java.
Referenced by ParamDescrs.validate().
|
inlinestatic |
Definition at line 3730 of file Native.java.
Referenced by Context.parseSMTLIB2File().
|
inlinestatic |
Definition at line 3721 of file Native.java.
Referenced by Context.parseSMTLIB2String().
|
inlinestatic |
Definition at line 3143 of file Native.java.
|
inlinestatic |
Definition at line 3676 of file Native.java.
Referenced by Pattern.toString().
|
inlinestatic |
Definition at line 5062 of file Native.java.
|
inlinestatic |
Definition at line 4172 of file Native.java.
Referenced by Context.and().
|
inlinestatic |
Definition at line 4271 of file Native.java.
Referenced by Probe.apply().
|
inlinestatic |
Definition at line 4118 of file Native.java.
Referenced by Context.constProbe().
|
inlinestatic |
Definition at line 3993 of file Native.java.
|
inlinestatic |
Definition at line 4163 of file Native.java.
Referenced by Context.eq().
|
inlinestatic |
Definition at line 4154 of file Native.java.
Referenced by Context.ge().
|
inlinestatic |
Definition at line 4262 of file Native.java.
Referenced by Context.getProbeDescription().
|
inlinestatic |
Definition at line 4136 of file Native.java.
Referenced by Context.gt().
|
inlinestatic |
Definition at line 3985 of file Native.java.
|
inlinestatic |
Definition at line 4145 of file Native.java.
Referenced by Context.le().
|
inlinestatic |
Definition at line 4127 of file Native.java.
Referenced by Context.lt().
|
inlinestatic |
Definition at line 4190 of file Native.java.
Referenced by Context.not().
|
inlinestatic |
Definition at line 4181 of file Native.java.
Referenced by Context.or().
|
inlinestatic |
Definition at line 6533 of file Native.java.
|
inlinestatic |
Definition at line 6506 of file Native.java.
|
inlinestatic |
Definition at line 6515 of file Native.java.
|
inlinestatic |
Definition at line 1075 of file Native.java.
Referenced by Constructor.ConstructorDecl(), Constructor.getAccessorDecls(), and Constructor.getTesterDecl().
|
inlinestatic |
Definition at line 5133 of file Native.java.
|
inlinestatic |
Definition at line 5071 of file Native.java.
|
inlinestatic |
Definition at line 5160 of file Native.java.
|
inlinestatic |
Definition at line 5232 of file Native.java.
|
inlinestatic |
Definition at line 5223 of file Native.java.
|
inlinestatic |
Definition at line 5268 of file Native.java.
|
inlinestatic |
Definition at line 5205 of file Native.java.
|
inlinestatic |
Definition at line 5178 of file Native.java.
|
inlinestatic |
Definition at line 5214 of file Native.java.
|
inlinestatic |
Definition at line 5196 of file Native.java.
|
inlinestatic |
Definition at line 5106 of file Native.java.
|
inlinestatic |
Definition at line 5115 of file Native.java.
|
inlinestatic |
Definition at line 5097 of file Native.java.
|
inlinestatic |
Definition at line 5079 of file Native.java.
|
inlinestatic |
Definition at line 5124 of file Native.java.
|
inlinestatic |
Definition at line 5088 of file Native.java.
|
inlinestatic |
Definition at line 5151 of file Native.java.
|
inlinestatic |
Definition at line 5169 of file Native.java.
|
inlinestatic |
Definition at line 5241 of file Native.java.
|
inlinestatic |
Definition at line 5259 of file Native.java.
|
inlinestatic |
Definition at line 5250 of file Native.java.
|
inlinestatic |
Definition at line 5187 of file Native.java.
|
inlinestatic |
Definition at line 5142 of file Native.java.
|
inlinestatic |
Definition at line 3792 of file Native.java.
|
inlinestatic |
Definition at line 3659 of file Native.java.
Referenced by Context.setPrintMode().
|
inlinestatic |
Definition at line 3754 of file Native.java.
|
static |
|
inlinestatic |
Definition at line 714 of file Native.java.
Referenced by Context.Context().
|
inlinestatic |
Definition at line 3287 of file Native.java.
Referenced by Expr.simplify().
|
inlinestatic |
Definition at line 3296 of file Native.java.
Referenced by Expr.simplify().
|
inlinestatic |
Definition at line 3305 of file Native.java.
Referenced by Context.SimplifyHelp().
|
inlinestatic |
Definition at line 3314 of file Native.java.
Referenced by Context.getSimplifyParameterDescriptions().
|
inlinestatic |
Definition at line 4469 of file Native.java.
Referenced by Solver.add().
|
inlinestatic |
Definition at line 4477 of file Native.java.
Referenced by Solver.assertAndTrack().
|
inlinestatic |
Definition at line 4528 of file Native.java.
Referenced by Solver.check().
|
inlinestatic |
Definition at line 4537 of file Native.java.
Referenced by Solver.check().
|
inlinestatic |
Definition at line 4564 of file Native.java.
|
inlinestatic |
Definition at line 4428 of file Native.java.
|
inlinestatic |
Definition at line 4485 of file Native.java.
Referenced by Solver.fromFile().
|
inlinestatic |
Definition at line 4493 of file Native.java.
Referenced by Solver.fromString().
|
inlinestatic |
Definition at line 4501 of file Native.java.
Referenced by Solver.getAssertions(), and Solver.getNumAssertions().
|
inlinestatic |
Definition at line 4555 of file Native.java.
|
inlinestatic |
Definition at line 4394 of file Native.java.
Referenced by Solver.getHelp().
|
inlinestatic |
Definition at line 4573 of file Native.java.
Referenced by Solver.getModel().
|
inlinestatic |
Definition at line 4519 of file Native.java.
|
inlinestatic |
Definition at line 4460 of file Native.java.
Referenced by Solver.getNumScopes().
|
inlinestatic |
Definition at line 4403 of file Native.java.
Referenced by Solver.getParameterDescriptions().
|
inlinestatic |
Definition at line 4582 of file Native.java.
Referenced by Solver.getProof().
|
inlinestatic |
Definition at line 4600 of file Native.java.
Referenced by Solver.getReasonUnknown().
|
inlinestatic |
Definition at line 4609 of file Native.java.
Referenced by Solver.getStatistics().
|
inlinestatic |
Definition at line 4510 of file Native.java.
|
inlinestatic |
Definition at line 4591 of file Native.java.
Referenced by Solver.getUnsatCore().
|
inlinestatic |
Definition at line 4386 of file Native.java.
|
inlinestatic |
Definition at line 4420 of file Native.java.
|
inlinestatic |
Definition at line 4444 of file Native.java.
Referenced by Solver.pop().
|
inlinestatic |
Definition at line 4436 of file Native.java.
Referenced by Solver.push().
|
inlinestatic |
Definition at line 4452 of file Native.java.
Referenced by Solver.reset().
|
inlinestatic |
Definition at line 4412 of file Native.java.
Referenced by Solver.setParameters().
|
inlinestatic |
Definition at line 4618 of file Native.java.
Referenced by Solver.toString().
|
inlinestatic |
Definition at line 4377 of file Native.java.
Referenced by Solver.translate().
|
inlinestatic |
Definition at line 2522 of file Native.java.
|
inlinestatic |
Definition at line 3685 of file Native.java.
Referenced by Sort.toString().
|
inlinestatic |
Definition at line 4644 of file Native.java.
|
inlinestatic |
Definition at line 4697 of file Native.java.
Referenced by Statistics.getEntries().
|
inlinestatic |
Definition at line 4661 of file Native.java.
Referenced by Statistics.getEntries(), and Statistics.getKeys().
|
inlinestatic |
Definition at line 4688 of file Native.java.
Referenced by Statistics.getEntries().
|
inlinestatic |
Definition at line 4636 of file Native.java.
|
inlinestatic |
Definition at line 4679 of file Native.java.
Referenced by Statistics.getEntries().
|
inlinestatic |
Definition at line 4670 of file Native.java.
Referenced by Statistics.getEntries().
|
inlinestatic |
Definition at line 4652 of file Native.java.
Referenced by Statistics.size().
|
inlinestatic |
Definition at line 4627 of file Native.java.
Referenced by Statistics.toString().
|
inlinestatic |
Definition at line 3332 of file Native.java.
Referenced by Expr.substitute().
|
inlinestatic |
Definition at line 3341 of file Native.java.
Referenced by Expr.substituteVars().
|
inlinestatic |
Definition at line 4001 of file Native.java.
Referenced by Context.andThen().
|
inlinestatic |
Definition at line 4280 of file Native.java.
Referenced by Tactic.apply().
|
inlinestatic |
Definition at line 4289 of file Native.java.
Referenced by Tactic.apply().
|
inlinestatic |
Definition at line 4055 of file Native.java.
Referenced by Context.cond().
|
inlinestatic |
Definition at line 3968 of file Native.java.
|
inlinestatic |
Definition at line 4082 of file Native.java.
Referenced by Context.fail().
|
inlinestatic |
Definition at line 4091 of file Native.java.
Referenced by Context.failIf().
|
inlinestatic |
Definition at line 4100 of file Native.java.
Referenced by Context.failIfNotDecided().
|
inlinestatic |
Definition at line 4253 of file Native.java.
Referenced by Context.getTacticDescription().
|
inlinestatic |
Definition at line 4235 of file Native.java.
Referenced by Tactic.getHelp().
|
inlinestatic |
Definition at line 4244 of file Native.java.
Referenced by Tactic.getParameterDescriptions().
|
inlinestatic |
Definition at line 3960 of file Native.java.
|
inlinestatic |
Definition at line 4010 of file Native.java.
Referenced by Context.orElse().
|
inlinestatic |
Definition at line 4028 of file Native.java.
Referenced by Context.parAndThen().
|
inlinestatic |
Definition at line 4019 of file Native.java.
Referenced by Context.parOr().
|
inlinestatic |
Definition at line 4064 of file Native.java.
Referenced by Context.repeat().
|
inlinestatic |
Definition at line 4073 of file Native.java.
Referenced by Context.skip().
|
inlinestatic |
Definition at line 4037 of file Native.java.
Referenced by Context.tryFor().
|
inlinestatic |
Definition at line 4109 of file Native.java.
Referenced by Context.usingParams().
|
inlinestatic |
Definition at line 4046 of file Native.java.
Referenced by Context.when().
|
inlinestatic |
Definition at line 3008 of file Native.java.
|
inlinestatic |
Definition at line 3017 of file Native.java.
|
inlinestatic |
Definition at line 3654 of file Native.java.
Referenced by Global.ToggleWarningMessages().
|
inlinestatic |
Definition at line 3350 of file Native.java.
Referenced by AST.translate().
|
inlinestatic |
Definition at line 756 of file Native.java.
Referenced by Context.updateParamValue().
|
inlinestatic |
Definition at line 3323 of file Native.java.
Referenced by Expr.update().