Data Structures | |
class | IntPtr |
class | LongPtr |
class | ObjArrayPtr |
class | StringPtr |
class | UIntArrayPtr |
Static Public Member Functions | |
static native void | setInternalErrorHandler (long ctx) |
static void | globalParamSet (String a0, String a1) |
static void | globalParamResetAll () |
static boolean | globalParamGet (String a0, StringPtr a1) |
static long | mkConfig () |
static void | delConfig (long a0) |
static void | setParamValue (long a0, String a1, String a2) |
static long | mkContext (long a0) throws Z3Exception |
static long | mkContextRc (long a0) throws Z3Exception |
static void | delContext (long a0) throws Z3Exception |
static void | incRef (long a0, long a1) throws Z3Exception |
static void | decRef (long a0, long a1) throws Z3Exception |
static void | updateParamValue (long a0, String a1, String a2) throws Z3Exception |
static void | interrupt (long a0) throws Z3Exception |
static long | mkParams (long a0) throws Z3Exception |
static void | paramsIncRef (long a0, long a1) throws Z3Exception |
static void | paramsDecRef (long a0, long a1) throws Z3Exception |
static void | paramsSetBool (long a0, long a1, long a2, boolean a3) throws Z3Exception |
static void | paramsSetUint (long a0, long a1, long a2, int a3) throws Z3Exception |
static void | paramsSetDouble (long a0, long a1, long a2, double a3) throws Z3Exception |
static void | paramsSetSymbol (long a0, long a1, long a2, long a3) throws Z3Exception |
static String | paramsToString (long a0, long a1) throws Z3Exception |
static void | paramsValidate (long a0, long a1, long a2) throws Z3Exception |
static void | paramDescrsIncRef (long a0, long a1) throws Z3Exception |
static void | paramDescrsDecRef (long a0, long a1) throws Z3Exception |
static int | paramDescrsGetKind (long a0, long a1, long a2) throws Z3Exception |
static int | paramDescrsSize (long a0, long a1) throws Z3Exception |
static long | paramDescrsGetName (long a0, long a1, int a2) throws Z3Exception |
static String | paramDescrsGetDocumentation (long a0, long a1, long a2) throws Z3Exception |
static String | paramDescrsToString (long a0, long a1) throws Z3Exception |
static long | mkIntSymbol (long a0, int a1) throws Z3Exception |
static long | mkStringSymbol (long a0, String a1) throws Z3Exception |
static long | mkUninterpretedSort (long a0, long a1) throws Z3Exception |
static long | mkBoolSort (long a0) throws Z3Exception |
static long | mkIntSort (long a0) throws Z3Exception |
static long | mkRealSort (long a0) throws Z3Exception |
static long | mkBvSort (long a0, int a1) throws Z3Exception |
static long | mkFiniteDomainSort (long a0, long a1, long a2) throws Z3Exception |
static long | mkArraySort (long a0, long a1, long a2) throws Z3Exception |
static long | mkArraySortN (long a0, int a1, long[] a2, long a3) throws Z3Exception |
static long | mkTupleSort (long a0, long a1, int a2, long[] a3, long[] a4, LongPtr a5, long[] a6) throws Z3Exception |
static long | mkEnumerationSort (long a0, long a1, int a2, long[] a3, long[] a4, long[] a5) throws Z3Exception |
static long | mkListSort (long a0, long a1, long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8) throws Z3Exception |
static long | mkConstructor (long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6) throws Z3Exception |
static void | delConstructor (long a0, long a1) throws Z3Exception |
static long | mkDatatype (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | mkConstructorList (long a0, int a1, long[] a2) throws Z3Exception |
static void | delConstructorList (long a0, long a1) throws Z3Exception |
static void | mkDatatypes (long a0, int a1, long[] a2, long[] a3, long[] a4) throws Z3Exception |
static void | queryConstructor (long a0, long a1, int a2, LongPtr a3, LongPtr a4, long[] a5) throws Z3Exception |
static long | mkFuncDecl (long a0, long a1, int a2, long[] a3, long a4) throws Z3Exception |
static long | mkApp (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | mkConst (long a0, long a1, long a2) throws Z3Exception |
static long | mkFreshFuncDecl (long a0, String a1, int a2, long[] a3, long a4) throws Z3Exception |
static long | mkFreshConst (long a0, String a1, long a2) throws Z3Exception |
static long | mkRecFuncDecl (long a0, long a1, int a2, long[] a3, long a4) throws Z3Exception |
static void | addRecDef (long a0, long a1, int a2, long[] a3, long a4) throws Z3Exception |
static long | mkTrue (long a0) throws Z3Exception |
static long | mkFalse (long a0) throws Z3Exception |
static long | mkEq (long a0, long a1, long a2) throws Z3Exception |
static long | mkDistinct (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkNot (long a0, long a1) throws Z3Exception |
static long | mkIte (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkIff (long a0, long a1, long a2) throws Z3Exception |
static long | mkImplies (long a0, long a1, long a2) throws Z3Exception |
static long | mkXor (long a0, long a1, long a2) throws Z3Exception |
static long | mkAnd (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkOr (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkAdd (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkMul (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkSub (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkUnaryMinus (long a0, long a1) throws Z3Exception |
static long | mkDiv (long a0, long a1, long a2) throws Z3Exception |
static long | mkMod (long a0, long a1, long a2) throws Z3Exception |
static long | mkRem (long a0, long a1, long a2) throws Z3Exception |
static long | mkPower (long a0, long a1, long a2) throws Z3Exception |
static long | mkLt (long a0, long a1, long a2) throws Z3Exception |
static long | mkLe (long a0, long a1, long a2) throws Z3Exception |
static long | mkGt (long a0, long a1, long a2) throws Z3Exception |
static long | mkGe (long a0, long a1, long a2) throws Z3Exception |
static long | mkDivides (long a0, long a1, long a2) throws Z3Exception |
static long | mkInt2real (long a0, long a1) throws Z3Exception |
static long | mkReal2int (long a0, long a1) throws Z3Exception |
static long | mkIsInt (long a0, long a1) throws Z3Exception |
static long | mkBvnot (long a0, long a1) throws Z3Exception |
static long | mkBvredand (long a0, long a1) throws Z3Exception |
static long | mkBvredor (long a0, long a1) throws Z3Exception |
static long | mkBvand (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvor (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvxor (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvnand (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvnor (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvxnor (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvneg (long a0, long a1) throws Z3Exception |
static long | mkBvadd (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsub (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvmul (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvudiv (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsdiv (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvurem (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsrem (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsmod (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvult (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvslt (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvule (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsle (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvuge (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsge (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvugt (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsgt (long a0, long a1, long a2) throws Z3Exception |
static long | mkConcat (long a0, long a1, long a2) throws Z3Exception |
static long | mkExtract (long a0, int a1, int a2, long a3) throws Z3Exception |
static long | mkSignExt (long a0, int a1, long a2) throws Z3Exception |
static long | mkZeroExt (long a0, int a1, long a2) throws Z3Exception |
static long | mkRepeat (long a0, int a1, long a2) throws Z3Exception |
static long | mkBvshl (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvlshr (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvashr (long a0, long a1, long a2) throws Z3Exception |
static long | mkRotateLeft (long a0, int a1, long a2) throws Z3Exception |
static long | mkRotateRight (long a0, int a1, long a2) throws Z3Exception |
static long | mkExtRotateLeft (long a0, long a1, long a2) throws Z3Exception |
static long | mkExtRotateRight (long a0, long a1, long a2) throws Z3Exception |
static long | mkInt2bv (long a0, int a1, long a2) throws Z3Exception |
static long | mkBv2int (long a0, long a1, boolean a2) throws Z3Exception |
static long | mkBvaddNoOverflow (long a0, long a1, long a2, boolean a3) throws Z3Exception |
static long | mkBvaddNoUnderflow (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsubNoOverflow (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvsubNoUnderflow (long a0, long a1, long a2, boolean a3) throws Z3Exception |
static long | mkBvsdivNoOverflow (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvnegNoOverflow (long a0, long a1) throws Z3Exception |
static long | mkBvmulNoOverflow (long a0, long a1, long a2, boolean a3) throws Z3Exception |
static long | mkBvmulNoUnderflow (long a0, long a1, long a2) throws Z3Exception |
static long | mkSelect (long a0, long a1, long a2) throws Z3Exception |
static long | mkSelectN (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | mkStore (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkStoreN (long a0, long a1, int a2, long[] a3, long a4) throws Z3Exception |
static long | mkConstArray (long a0, long a1, long a2) throws Z3Exception |
static long | mkMap (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | mkArrayDefault (long a0, long a1) throws Z3Exception |
static long | mkAsArray (long a0, long a1) throws Z3Exception |
static long | mkSetHasSize (long a0, long a1, long a2) throws Z3Exception |
static long | mkSetSort (long a0, long a1) throws Z3Exception |
static long | mkEmptySet (long a0, long a1) throws Z3Exception |
static long | mkFullSet (long a0, long a1) throws Z3Exception |
static long | mkSetAdd (long a0, long a1, long a2) throws Z3Exception |
static long | mkSetDel (long a0, long a1, long a2) throws Z3Exception |
static long | mkSetUnion (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkSetIntersect (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkSetDifference (long a0, long a1, long a2) throws Z3Exception |
static long | mkSetComplement (long a0, long a1) throws Z3Exception |
static long | mkSetMember (long a0, long a1, long a2) throws Z3Exception |
static long | mkSetSubset (long a0, long a1, long a2) throws Z3Exception |
static long | mkArrayExt (long a0, long a1, long a2) throws Z3Exception |
static long | mkNumeral (long a0, String a1, long a2) throws Z3Exception |
static long | mkReal (long a0, int a1, int a2) throws Z3Exception |
static long | mkInt (long a0, int a1, long a2) throws Z3Exception |
static long | mkUnsignedInt (long a0, int a1, long a2) throws Z3Exception |
static long | mkInt64 (long a0, long a1, long a2) throws Z3Exception |
static long | mkUnsignedInt64 (long a0, long a1, long a2) throws Z3Exception |
static long | mkBvNumeral (long a0, int a1, boolean[] a2) throws Z3Exception |
static long | mkSeqSort (long a0, long a1) throws Z3Exception |
static boolean | isSeqSort (long a0, long a1) throws Z3Exception |
static long | getSeqSortBasis (long a0, long a1) throws Z3Exception |
static long | mkReSort (long a0, long a1) throws Z3Exception |
static boolean | isReSort (long a0, long a1) throws Z3Exception |
static long | getReSortBasis (long a0, long a1) throws Z3Exception |
static long | mkStringSort (long a0) throws Z3Exception |
static boolean | isStringSort (long a0, long a1) throws Z3Exception |
static long | mkString (long a0, String a1) throws Z3Exception |
static long | mkLstring (long a0, int a1, String a2) throws Z3Exception |
static boolean | isString (long a0, long a1) throws Z3Exception |
static String | getString (long a0, long a1) throws Z3Exception |
static long | getLstring (long a0, long a1, IntPtr a2) throws Z3Exception |
static long | mkSeqEmpty (long a0, long a1) throws Z3Exception |
static long | mkSeqUnit (long a0, long a1) throws Z3Exception |
static long | mkSeqConcat (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkSeqPrefix (long a0, long a1, long a2) throws Z3Exception |
static long | mkSeqSuffix (long a0, long a1, long a2) throws Z3Exception |
static long | mkSeqContains (long a0, long a1, long a2) throws Z3Exception |
static long | mkStrLt (long a0, long a1, long a2) throws Z3Exception |
static long | mkStrLe (long a0, long a1, long a2) throws Z3Exception |
static long | mkSeqExtract (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkSeqReplace (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkSeqAt (long a0, long a1, long a2) throws Z3Exception |
static long | mkSeqNth (long a0, long a1, long a2) throws Z3Exception |
static long | mkSeqLength (long a0, long a1) throws Z3Exception |
static long | mkSeqIndex (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkSeqLastIndex (long a0, long a1, long a2) throws Z3Exception |
static long | mkStrToInt (long a0, long a1) throws Z3Exception |
static long | mkIntToStr (long a0, long a1) throws Z3Exception |
static long | mkSeqToRe (long a0, long a1) throws Z3Exception |
static long | mkSeqInRe (long a0, long a1, long a2) throws Z3Exception |
static long | mkRePlus (long a0, long a1) throws Z3Exception |
static long | mkReStar (long a0, long a1) throws Z3Exception |
static long | mkReOption (long a0, long a1) throws Z3Exception |
static long | mkReUnion (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkReConcat (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkReRange (long a0, long a1, long a2) throws Z3Exception |
static long | mkReLoop (long a0, long a1, int a2, int a3) throws Z3Exception |
static long | mkReIntersect (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkReComplement (long a0, long a1) throws Z3Exception |
static long | mkReEmpty (long a0, long a1) throws Z3Exception |
static long | mkReFull (long a0, long a1) throws Z3Exception |
static long | mkLinearOrder (long a0, long a1, int a2) throws Z3Exception |
static long | mkPartialOrder (long a0, long a1, int a2) throws Z3Exception |
static long | mkPiecewiseLinearOrder (long a0, long a1, int a2) throws Z3Exception |
static long | mkTreeOrder (long a0, long a1, int a2) throws Z3Exception |
static long | mkTransitiveClosure (long a0, long a1) throws Z3Exception |
static long | mkPattern (long a0, int a1, long[] a2) throws Z3Exception |
static long | mkBound (long a0, int a1, long a2) throws Z3Exception |
static long | mkForall (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7) throws Z3Exception |
static long | mkExists (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7) throws Z3Exception |
static long | mkQuantifier (long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8) throws Z3Exception |
static long | mkQuantifierEx (long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long[] a11, long a12) throws Z3Exception |
static long | mkForallConst (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6) throws Z3Exception |
static long | mkExistsConst (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6) throws Z3Exception |
static long | mkQuantifierConst (long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7) throws Z3Exception |
static long | mkQuantifierConstEx (long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long a11) throws Z3Exception |
static long | mkLambda (long a0, int a1, long[] a2, long[] a3, long a4) throws Z3Exception |
static long | mkLambdaConst (long a0, int a1, long[] a2, long a3) throws Z3Exception |
static int | getSymbolKind (long a0, long a1) throws Z3Exception |
static int | getSymbolInt (long a0, long a1) throws Z3Exception |
static String | getSymbolString (long a0, long a1) throws Z3Exception |
static long | getSortName (long a0, long a1) throws Z3Exception |
static int | getSortId (long a0, long a1) throws Z3Exception |
static long | sortToAst (long a0, long a1) throws Z3Exception |
static boolean | isEqSort (long a0, long a1, long a2) throws Z3Exception |
static int | getSortKind (long a0, long a1) throws Z3Exception |
static int | getBvSortSize (long a0, long a1) throws Z3Exception |
static boolean | getFiniteDomainSortSize (long a0, long a1, LongPtr a2) throws Z3Exception |
static long | getArraySortDomain (long a0, long a1) throws Z3Exception |
static long | getArraySortRange (long a0, long a1) throws Z3Exception |
static long | getTupleSortMkDecl (long a0, long a1) throws Z3Exception |
static int | getTupleSortNumFields (long a0, long a1) throws Z3Exception |
static long | getTupleSortFieldDecl (long a0, long a1, int a2) throws Z3Exception |
static int | getDatatypeSortNumConstructors (long a0, long a1) throws Z3Exception |
static long | getDatatypeSortConstructor (long a0, long a1, int a2) throws Z3Exception |
static long | getDatatypeSortRecognizer (long a0, long a1, int a2) throws Z3Exception |
static long | getDatatypeSortConstructorAccessor (long a0, long a1, int a2, int a3) throws Z3Exception |
static long | datatypeUpdateField (long a0, long a1, long a2, long a3) throws Z3Exception |
static int | getRelationArity (long a0, long a1) throws Z3Exception |
static long | getRelationColumn (long a0, long a1, int a2) throws Z3Exception |
static long | mkAtmost (long a0, int a1, long[] a2, int a3) throws Z3Exception |
static long | mkAtleast (long a0, int a1, long[] a2, int a3) throws Z3Exception |
static long | mkPble (long a0, int a1, long[] a2, int[] a3, int a4) throws Z3Exception |
static long | mkPbge (long a0, int a1, long[] a2, int[] a3, int a4) throws Z3Exception |
static long | mkPbeq (long a0, int a1, long[] a2, int[] a3, int a4) throws Z3Exception |
static long | funcDeclToAst (long a0, long a1) throws Z3Exception |
static boolean | isEqFuncDecl (long a0, long a1, long a2) throws Z3Exception |
static int | getFuncDeclId (long a0, long a1) throws Z3Exception |
static long | getDeclName (long a0, long a1) throws Z3Exception |
static int | getDeclKind (long a0, long a1) throws Z3Exception |
static int | getDomainSize (long a0, long a1) throws Z3Exception |
static int | getArity (long a0, long a1) throws Z3Exception |
static long | getDomain (long a0, long a1, int a2) throws Z3Exception |
static long | getRange (long a0, long a1) throws Z3Exception |
static int | getDeclNumParameters (long a0, long a1) throws Z3Exception |
static int | getDeclParameterKind (long a0, long a1, int a2) throws Z3Exception |
static int | getDeclIntParameter (long a0, long a1, int a2) throws Z3Exception |
static double | getDeclDoubleParameter (long a0, long a1, int a2) throws Z3Exception |
static long | getDeclSymbolParameter (long a0, long a1, int a2) throws Z3Exception |
static long | getDeclSortParameter (long a0, long a1, int a2) throws Z3Exception |
static long | getDeclAstParameter (long a0, long a1, int a2) throws Z3Exception |
static long | getDeclFuncDeclParameter (long a0, long a1, int a2) throws Z3Exception |
static String | getDeclRationalParameter (long a0, long a1, int a2) throws Z3Exception |
static long | appToAst (long a0, long a1) throws Z3Exception |
static long | getAppDecl (long a0, long a1) throws Z3Exception |
static int | getAppNumArgs (long a0, long a1) throws Z3Exception |
static long | getAppArg (long a0, long a1, int a2) throws Z3Exception |
static boolean | isEqAst (long a0, long a1, long a2) throws Z3Exception |
static int | getAstId (long a0, long a1) throws Z3Exception |
static int | getAstHash (long a0, long a1) throws Z3Exception |
static long | getSort (long a0, long a1) throws Z3Exception |
static boolean | isWellSorted (long a0, long a1) throws Z3Exception |
static int | getBoolValue (long a0, long a1) throws Z3Exception |
static int | getAstKind (long a0, long a1) throws Z3Exception |
static boolean | isApp (long a0, long a1) throws Z3Exception |
static boolean | isNumeralAst (long a0, long a1) throws Z3Exception |
static boolean | isAlgebraicNumber (long a0, long a1) throws Z3Exception |
static long | toApp (long a0, long a1) throws Z3Exception |
static long | toFuncDecl (long a0, long a1) throws Z3Exception |
static String | getNumeralString (long a0, long a1) throws Z3Exception |
static String | getNumeralDecimalString (long a0, long a1, int a2) throws Z3Exception |
static double | getNumeralDouble (long a0, long a1) throws Z3Exception |
static long | getNumerator (long a0, long a1) throws Z3Exception |
static long | getDenominator (long a0, long a1) throws Z3Exception |
static boolean | getNumeralSmall (long a0, long a1, LongPtr a2, LongPtr a3) throws Z3Exception |
static boolean | getNumeralInt (long a0, long a1, IntPtr a2) throws Z3Exception |
static boolean | getNumeralUint (long a0, long a1, IntPtr a2) throws Z3Exception |
static boolean | getNumeralUint64 (long a0, long a1, LongPtr a2) throws Z3Exception |
static boolean | getNumeralInt64 (long a0, long a1, LongPtr a2) throws Z3Exception |
static boolean | getNumeralRationalInt64 (long a0, long a1, LongPtr a2, LongPtr a3) throws Z3Exception |
static long | getAlgebraicNumberLower (long a0, long a1, int a2) throws Z3Exception |
static long | getAlgebraicNumberUpper (long a0, long a1, int a2) throws Z3Exception |
static long | patternToAst (long a0, long a1) throws Z3Exception |
static int | getPatternNumTerms (long a0, long a1) throws Z3Exception |
static long | getPattern (long a0, long a1, int a2) throws Z3Exception |
static int | getIndexValue (long a0, long a1) throws Z3Exception |
static boolean | isQuantifierForall (long a0, long a1) throws Z3Exception |
static boolean | isQuantifierExists (long a0, long a1) throws Z3Exception |
static boolean | isLambda (long a0, long a1) throws Z3Exception |
static int | getQuantifierWeight (long a0, long a1) throws Z3Exception |
static int | getQuantifierNumPatterns (long a0, long a1) throws Z3Exception |
static long | getQuantifierPatternAst (long a0, long a1, int a2) throws Z3Exception |
static int | getQuantifierNumNoPatterns (long a0, long a1) throws Z3Exception |
static long | getQuantifierNoPatternAst (long a0, long a1, int a2) throws Z3Exception |
static int | getQuantifierNumBound (long a0, long a1) throws Z3Exception |
static long | getQuantifierBoundName (long a0, long a1, int a2) throws Z3Exception |
static long | getQuantifierBoundSort (long a0, long a1, int a2) throws Z3Exception |
static long | getQuantifierBody (long a0, long a1) throws Z3Exception |
static long | simplify (long a0, long a1) throws Z3Exception |
static long | simplifyEx (long a0, long a1, long a2) throws Z3Exception |
static String | simplifyGetHelp (long a0) throws Z3Exception |
static long | simplifyGetParamDescrs (long a0) throws Z3Exception |
static long | updateTerm (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | substitute (long a0, long a1, int a2, long[] a3, long[] a4) throws Z3Exception |
static long | substituteVars (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | translate (long a0, long a1, long a2) throws Z3Exception |
static long | mkModel (long a0) throws Z3Exception |
static void | modelIncRef (long a0, long a1) throws Z3Exception |
static void | modelDecRef (long a0, long a1) throws Z3Exception |
static boolean | modelEval (long a0, long a1, long a2, boolean a3, LongPtr a4) throws Z3Exception |
static long | modelGetConstInterp (long a0, long a1, long a2) throws Z3Exception |
static boolean | modelHasInterp (long a0, long a1, long a2) throws Z3Exception |
static long | modelGetFuncInterp (long a0, long a1, long a2) throws Z3Exception |
static int | modelGetNumConsts (long a0, long a1) throws Z3Exception |
static long | modelGetConstDecl (long a0, long a1, int a2) throws Z3Exception |
static int | modelGetNumFuncs (long a0, long a1) throws Z3Exception |
static long | modelGetFuncDecl (long a0, long a1, int a2) throws Z3Exception |
static int | modelGetNumSorts (long a0, long a1) throws Z3Exception |
static long | modelGetSort (long a0, long a1, int a2) throws Z3Exception |
static long | modelGetSortUniverse (long a0, long a1, long a2) throws Z3Exception |
static long | modelTranslate (long a0, long a1, long a2) throws Z3Exception |
static boolean | isAsArray (long a0, long a1) throws Z3Exception |
static long | getAsArrayFuncDecl (long a0, long a1) throws Z3Exception |
static long | addFuncInterp (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | addConstInterp (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | funcInterpIncRef (long a0, long a1) throws Z3Exception |
static void | funcInterpDecRef (long a0, long a1) throws Z3Exception |
static int | funcInterpGetNumEntries (long a0, long a1) throws Z3Exception |
static long | funcInterpGetEntry (long a0, long a1, int a2) throws Z3Exception |
static long | funcInterpGetElse (long a0, long a1) throws Z3Exception |
static void | funcInterpSetElse (long a0, long a1, long a2) throws Z3Exception |
static int | funcInterpGetArity (long a0, long a1) throws Z3Exception |
static void | funcInterpAddEntry (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | funcEntryIncRef (long a0, long a1) throws Z3Exception |
static void | funcEntryDecRef (long a0, long a1) throws Z3Exception |
static long | funcEntryGetValue (long a0, long a1) throws Z3Exception |
static int | funcEntryGetNumArgs (long a0, long a1) throws Z3Exception |
static long | funcEntryGetArg (long a0, long a1, int a2) throws Z3Exception |
static int | openLog (String a0) |
static void | appendLog (String a0) |
static void | closeLog () |
static void | toggleWarningMessages (boolean a0) |
static void | setAstPrintMode (long a0, int a1) throws Z3Exception |
static String | astToString (long a0, long a1) throws Z3Exception |
static String | patternToString (long a0, long a1) throws Z3Exception |
static String | sortToString (long a0, long a1) throws Z3Exception |
static String | funcDeclToString (long a0, long a1) throws Z3Exception |
static String | modelToString (long a0, long a1) throws Z3Exception |
static String | benchmarkToSmtlibString (long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7) throws Z3Exception |
static long | parseSmtlib2String (long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7) throws Z3Exception |
static long | parseSmtlib2File (long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7) throws Z3Exception |
static String | evalSmtlib2String (long a0, String a1) throws Z3Exception |
static int | getErrorCode (long a0) throws Z3Exception |
static void | setError (long a0, int a1) throws Z3Exception |
static String | getErrorMsg (long a0, int a1) throws Z3Exception |
static void | getVersion (IntPtr a0, IntPtr a1, IntPtr a2, IntPtr a3) |
static String | getFullVersion () |
static void | enableTrace (String a0) |
static void | disableTrace (String a0) |
static void | resetMemory () |
static void | finalizeMemory () |
static long | mkGoal (long a0, boolean a1, boolean a2, boolean a3) throws Z3Exception |
static void | goalIncRef (long a0, long a1) throws Z3Exception |
static void | goalDecRef (long a0, long a1) throws Z3Exception |
static int | goalPrecision (long a0, long a1) throws Z3Exception |
static void | goalAssert (long a0, long a1, long a2) throws Z3Exception |
static boolean | goalInconsistent (long a0, long a1) throws Z3Exception |
static int | goalDepth (long a0, long a1) throws Z3Exception |
static void | goalReset (long a0, long a1) throws Z3Exception |
static int | goalSize (long a0, long a1) throws Z3Exception |
static long | goalFormula (long a0, long a1, int a2) throws Z3Exception |
static int | goalNumExprs (long a0, long a1) throws Z3Exception |
static boolean | goalIsDecidedSat (long a0, long a1) throws Z3Exception |
static boolean | goalIsDecidedUnsat (long a0, long a1) throws Z3Exception |
static long | goalTranslate (long a0, long a1, long a2) throws Z3Exception |
static long | goalConvertModel (long a0, long a1, long a2) throws Z3Exception |
static String | goalToString (long a0, long a1) throws Z3Exception |
static String | goalToDimacsString (long a0, long a1) throws Z3Exception |
static long | mkTactic (long a0, String a1) throws Z3Exception |
static void | tacticIncRef (long a0, long a1) throws Z3Exception |
static void | tacticDecRef (long a0, long a1) throws Z3Exception |
static long | mkProbe (long a0, String a1) throws Z3Exception |
static void | probeIncRef (long a0, long a1) throws Z3Exception |
static void | probeDecRef (long a0, long a1) throws Z3Exception |
static long | tacticAndThen (long a0, long a1, long a2) throws Z3Exception |
static long | tacticOrElse (long a0, long a1, long a2) throws Z3Exception |
static long | tacticParOr (long a0, int a1, long[] a2) throws Z3Exception |
static long | tacticParAndThen (long a0, long a1, long a2) throws Z3Exception |
static long | tacticTryFor (long a0, long a1, int a2) throws Z3Exception |
static long | tacticWhen (long a0, long a1, long a2) throws Z3Exception |
static long | tacticCond (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | tacticRepeat (long a0, long a1, int a2) throws Z3Exception |
static long | tacticSkip (long a0) throws Z3Exception |
static long | tacticFail (long a0) throws Z3Exception |
static long | tacticFailIf (long a0, long a1) throws Z3Exception |
static long | tacticFailIfNotDecided (long a0) throws Z3Exception |
static long | tacticUsingParams (long a0, long a1, long a2) throws Z3Exception |
static long | probeConst (long a0, double a1) throws Z3Exception |
static long | probeLt (long a0, long a1, long a2) throws Z3Exception |
static long | probeGt (long a0, long a1, long a2) throws Z3Exception |
static long | probeLe (long a0, long a1, long a2) throws Z3Exception |
static long | probeGe (long a0, long a1, long a2) throws Z3Exception |
static long | probeEq (long a0, long a1, long a2) throws Z3Exception |
static long | probeAnd (long a0, long a1, long a2) throws Z3Exception |
static long | probeOr (long a0, long a1, long a2) throws Z3Exception |
static long | probeNot (long a0, long a1) throws Z3Exception |
static int | getNumTactics (long a0) throws Z3Exception |
static String | getTacticName (long a0, int a1) throws Z3Exception |
static int | getNumProbes (long a0) throws Z3Exception |
static String | getProbeName (long a0, int a1) throws Z3Exception |
static String | tacticGetHelp (long a0, long a1) throws Z3Exception |
static long | tacticGetParamDescrs (long a0, long a1) throws Z3Exception |
static String | tacticGetDescr (long a0, String a1) throws Z3Exception |
static String | probeGetDescr (long a0, String a1) throws Z3Exception |
static double | probeApply (long a0, long a1, long a2) throws Z3Exception |
static long | tacticApply (long a0, long a1, long a2) throws Z3Exception |
static long | tacticApplyEx (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | applyResultIncRef (long a0, long a1) throws Z3Exception |
static void | applyResultDecRef (long a0, long a1) throws Z3Exception |
static String | applyResultToString (long a0, long a1) throws Z3Exception |
static int | applyResultGetNumSubgoals (long a0, long a1) throws Z3Exception |
static long | applyResultGetSubgoal (long a0, long a1, int a2) throws Z3Exception |
static long | mkSolver (long a0) throws Z3Exception |
static long | mkSimpleSolver (long a0) throws Z3Exception |
static long | mkSolverForLogic (long a0, long a1) throws Z3Exception |
static long | mkSolverFromTactic (long a0, long a1) throws Z3Exception |
static long | solverTranslate (long a0, long a1, long a2) throws Z3Exception |
static void | solverImportModelConverter (long a0, long a1, long a2) throws Z3Exception |
static String | solverGetHelp (long a0, long a1) throws Z3Exception |
static long | solverGetParamDescrs (long a0, long a1) throws Z3Exception |
static void | solverSetParams (long a0, long a1, long a2) throws Z3Exception |
static void | solverIncRef (long a0, long a1) throws Z3Exception |
static void | solverDecRef (long a0, long a1) throws Z3Exception |
static void | solverInterrupt (long a0, long a1) throws Z3Exception |
static void | solverPush (long a0, long a1) throws Z3Exception |
static void | solverPop (long a0, long a1, int a2) throws Z3Exception |
static void | solverReset (long a0, long a1) throws Z3Exception |
static int | solverGetNumScopes (long a0, long a1) throws Z3Exception |
static void | solverAssert (long a0, long a1, long a2) throws Z3Exception |
static void | solverAssertAndTrack (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | solverFromFile (long a0, long a1, String a2) throws Z3Exception |
static void | solverFromString (long a0, long a1, String a2) throws Z3Exception |
static long | solverGetAssertions (long a0, long a1) throws Z3Exception |
static long | solverGetUnits (long a0, long a1) throws Z3Exception |
static long | solverGetTrail (long a0, long a1) throws Z3Exception |
static long | solverGetNonUnits (long a0, long a1) throws Z3Exception |
static void | solverGetLevels (long a0, long a1, long a2, int a3, int[] a4) throws Z3Exception |
static int | solverCheck (long a0, long a1) throws Z3Exception |
static int | solverCheckAssumptions (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static int | getImpliedEqualities (long a0, long a1, int a2, long[] a3, int[] a4) throws Z3Exception |
static int | solverGetConsequences (long a0, long a1, long a2, long a3, long a4) throws Z3Exception |
static long | solverCube (long a0, long a1, long a2, int a3) throws Z3Exception |
static long | solverGetModel (long a0, long a1) throws Z3Exception |
static long | solverGetProof (long a0, long a1) throws Z3Exception |
static long | solverGetUnsatCore (long a0, long a1) throws Z3Exception |
static String | solverGetReasonUnknown (long a0, long a1) throws Z3Exception |
static long | solverGetStatistics (long a0, long a1) throws Z3Exception |
static String | solverToString (long a0, long a1) throws Z3Exception |
static String | solverToDimacsString (long a0, long a1, boolean a2) 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 | algebraicGetPoly (long a0, long a1) throws Z3Exception |
static int | algebraicGetI (long a0, long a1) throws Z3Exception |
static long | polynomialSubresultants (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | rcfDel (long a0, long a1) throws Z3Exception |
static long | rcfMkRational (long a0, String a1) throws Z3Exception |
static long | rcfMkSmallInt (long a0, int a1) throws Z3Exception |
static long | rcfMkPi (long a0) throws Z3Exception |
static long | rcfMkE (long a0) throws Z3Exception |
static long | rcfMkInfinitesimal (long a0) throws Z3Exception |
static int | rcfMkRoots (long a0, int a1, long[] a2, long[] a3) throws Z3Exception |
static long | rcfAdd (long a0, long a1, long a2) throws Z3Exception |
static long | rcfSub (long a0, long a1, long a2) throws Z3Exception |
static long | rcfMul (long a0, long a1, long a2) throws Z3Exception |
static long | rcfDiv (long a0, long a1, long a2) throws Z3Exception |
static long | rcfNeg (long a0, long a1) throws Z3Exception |
static long | rcfInv (long a0, long a1) throws Z3Exception |
static long | rcfPower (long a0, long a1, int a2) throws Z3Exception |
static boolean | rcfLt (long a0, long a1, long a2) throws Z3Exception |
static boolean | rcfGt (long a0, long a1, long a2) throws Z3Exception |
static boolean | rcfLe (long a0, long a1, long a2) throws Z3Exception |
static boolean | rcfGe (long a0, long a1, long a2) throws Z3Exception |
static boolean | rcfEq (long a0, long a1, long a2) throws Z3Exception |
static boolean | rcfNeq (long a0, long a1, long a2) throws Z3Exception |
static String | rcfNumToString (long a0, long a1, boolean a2, boolean a3) throws Z3Exception |
static String | rcfNumToDecimalString (long a0, long a1, int a2) throws Z3Exception |
static void | rcfGetNumeratorDenominator (long a0, long a1, LongPtr a2, LongPtr a3) throws Z3Exception |
static long | mkFixedpoint (long a0) throws Z3Exception |
static void | fixedpointIncRef (long a0, long a1) throws Z3Exception |
static void | fixedpointDecRef (long a0, long a1) throws Z3Exception |
static void | fixedpointAddRule (long a0, long a1, long a2, long a3) throws Z3Exception |
static void | fixedpointAddFact (long a0, long a1, long a2, int a3, int[] a4) throws Z3Exception |
static void | fixedpointAssert (long a0, long a1, long a2) throws Z3Exception |
static int | fixedpointQuery (long a0, long a1, long a2) throws Z3Exception |
static int | fixedpointQueryRelations (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | fixedpointGetAnswer (long a0, long a1) throws Z3Exception |
static String | fixedpointGetReasonUnknown (long a0, long a1) throws Z3Exception |
static void | fixedpointUpdateRule (long a0, long a1, long a2, long a3) throws Z3Exception |
static int | fixedpointGetNumLevels (long a0, long a1, long a2) throws Z3Exception |
static long | fixedpointGetCoverDelta (long a0, long a1, int a2, long a3) throws Z3Exception |
static void | fixedpointAddCover (long a0, long a1, int a2, long a3, long a4) throws Z3Exception |
static long | fixedpointGetStatistics (long a0, long a1) throws Z3Exception |
static void | fixedpointRegisterRelation (long a0, long a1, long a2) throws Z3Exception |
static void | fixedpointSetPredicateRepresentation (long a0, long a1, long a2, int a3, long[] a4) throws Z3Exception |
static long | fixedpointGetRules (long a0, long a1) throws Z3Exception |
static long | fixedpointGetAssertions (long a0, long a1) throws Z3Exception |
static void | fixedpointSetParams (long a0, long a1, long a2) throws Z3Exception |
static String | fixedpointGetHelp (long a0, long a1) throws Z3Exception |
static long | fixedpointGetParamDescrs (long a0, long a1) throws Z3Exception |
static String | fixedpointToString (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static long | fixedpointFromString (long a0, long a1, String a2) throws Z3Exception |
static long | fixedpointFromFile (long a0, long a1, String a2) throws Z3Exception |
static long | mkOptimize (long a0) throws Z3Exception |
static void | optimizeIncRef (long a0, long a1) throws Z3Exception |
static void | optimizeDecRef (long a0, long a1) throws Z3Exception |
static void | optimizeAssert (long a0, long a1, long a2) throws Z3Exception |
static void | optimizeAssertAndTrack (long a0, long a1, long a2, long a3) throws Z3Exception |
static int | optimizeAssertSoft (long a0, long a1, long a2, String a3, long a4) throws Z3Exception |
static int | optimizeMaximize (long a0, long a1, long a2) throws Z3Exception |
static int | optimizeMinimize (long a0, long a1, long a2) throws Z3Exception |
static void | optimizePush (long a0, long a1) throws Z3Exception |
static void | optimizePop (long a0, long a1) throws Z3Exception |
static int | optimizeCheck (long a0, long a1, int a2, long[] a3) throws Z3Exception |
static String | optimizeGetReasonUnknown (long a0, long a1) throws Z3Exception |
static long | optimizeGetModel (long a0, long a1) throws Z3Exception |
static long | optimizeGetUnsatCore (long a0, long a1) throws Z3Exception |
static void | optimizeSetParams (long a0, long a1, long a2) throws Z3Exception |
static long | optimizeGetParamDescrs (long a0, long a1) throws Z3Exception |
static long | optimizeGetLower (long a0, long a1, int a2) throws Z3Exception |
static long | optimizeGetUpper (long a0, long a1, int a2) throws Z3Exception |
static long | optimizeGetLowerAsVector (long a0, long a1, int a2) throws Z3Exception |
static long | optimizeGetUpperAsVector (long a0, long a1, int a2) throws Z3Exception |
static String | optimizeToString (long a0, long a1) throws Z3Exception |
static void | optimizeFromString (long a0, long a1, String a2) throws Z3Exception |
static void | optimizeFromFile (long a0, long a1, String a2) throws Z3Exception |
static String | optimizeGetHelp (long a0, long a1) throws Z3Exception |
static long | optimizeGetStatistics (long a0, long a1) throws Z3Exception |
static long | optimizeGetAssertions (long a0, long a1) throws Z3Exception |
static long | optimizeGetObjectives (long a0, long a1) throws Z3Exception |
static long | mkFpaRoundingModeSort (long a0) throws Z3Exception |
static long | mkFpaRoundNearestTiesToEven (long a0) throws Z3Exception |
static long | mkFpaRne (long a0) throws Z3Exception |
static long | mkFpaRoundNearestTiesToAway (long a0) throws Z3Exception |
static long | mkFpaRna (long a0) throws Z3Exception |
static long | mkFpaRoundTowardPositive (long a0) throws Z3Exception |
static long | mkFpaRtp (long a0) throws Z3Exception |
static long | mkFpaRoundTowardNegative (long a0) throws Z3Exception |
static long | mkFpaRtn (long a0) throws Z3Exception |
static long | mkFpaRoundTowardZero (long a0) throws Z3Exception |
static long | mkFpaRtz (long a0) throws Z3Exception |
static long | mkFpaSort (long a0, int a1, int a2) throws Z3Exception |
static long | mkFpaSortHalf (long a0) throws Z3Exception |
static long | mkFpaSort16 (long a0) throws Z3Exception |
static long | mkFpaSortSingle (long a0) throws Z3Exception |
static long | mkFpaSort32 (long a0) throws Z3Exception |
static long | mkFpaSortDouble (long a0) throws Z3Exception |
static long | mkFpaSort64 (long a0) throws Z3Exception |
static long | mkFpaSortQuadruple (long a0) throws Z3Exception |
static long | mkFpaSort128 (long a0) throws Z3Exception |
static long | mkFpaNan (long a0, long a1) throws Z3Exception |
static long | mkFpaInf (long a0, long a1, boolean a2) throws Z3Exception |
static long | mkFpaZero (long a0, long a1, boolean a2) throws Z3Exception |
static long | mkFpaFp (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaNumeralFloat (long a0, float a1, long a2) throws Z3Exception |
static long | mkFpaNumeralDouble (long a0, double a1, long a2) throws Z3Exception |
static long | mkFpaNumeralInt (long a0, int a1, long a2) throws Z3Exception |
static long | mkFpaNumeralIntUint (long a0, boolean a1, int a2, int a3, long a4) throws Z3Exception |
static long | mkFpaNumeralInt64Uint64 (long a0, boolean a1, long a2, long a3, long a4) throws Z3Exception |
static long | mkFpaAbs (long a0, long a1) throws Z3Exception |
static long | mkFpaNeg (long a0, long a1) throws Z3Exception |
static long | mkFpaAdd (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaSub (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaMul (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaDiv (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaFma (long a0, long a1, long a2, long a3, long a4) throws Z3Exception |
static long | mkFpaSqrt (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaRem (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaRoundToIntegral (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaMin (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaMax (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaLeq (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaLt (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaGeq (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaGt (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaEq (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaIsNormal (long a0, long a1) throws Z3Exception |
static long | mkFpaIsSubnormal (long a0, long a1) throws Z3Exception |
static long | mkFpaIsZero (long a0, long a1) throws Z3Exception |
static long | mkFpaIsInfinite (long a0, long a1) throws Z3Exception |
static long | mkFpaIsNan (long a0, long a1) throws Z3Exception |
static long | mkFpaIsNegative (long a0, long a1) throws Z3Exception |
static long | mkFpaIsPositive (long a0, long a1) throws Z3Exception |
static long | mkFpaToFpBv (long a0, long a1, long a2) throws Z3Exception |
static long | mkFpaToFpFloat (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaToFpReal (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaToFpSigned (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaToFpUnsigned (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | mkFpaToUbv (long a0, long a1, long a2, int a3) throws Z3Exception |
static long | mkFpaToSbv (long a0, long a1, long a2, int a3) throws Z3Exception |
static long | mkFpaToReal (long a0, long a1) throws Z3Exception |
static int | fpaGetEbits (long a0, long a1) throws Z3Exception |
static int | fpaGetSbits (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralNan (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralInf (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralZero (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralNormal (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralSubnormal (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralPositive (long a0, long a1) throws Z3Exception |
static boolean | fpaIsNumeralNegative (long a0, long a1) throws Z3Exception |
static long | fpaGetNumeralSignBv (long a0, long a1) throws Z3Exception |
static long | fpaGetNumeralSignificandBv (long a0, long a1) throws Z3Exception |
static boolean | fpaGetNumeralSign (long a0, long a1, IntPtr a2) throws Z3Exception |
static String | fpaGetNumeralSignificandString (long a0, long a1) throws Z3Exception |
static boolean | fpaGetNumeralSignificandUint64 (long a0, long a1, LongPtr a2) throws Z3Exception |
static String | fpaGetNumeralExponentString (long a0, long a1, boolean a2) throws Z3Exception |
static boolean | fpaGetNumeralExponentInt64 (long a0, long a1, LongPtr a2, boolean a3) throws Z3Exception |
static long | fpaGetNumeralExponentBv (long a0, long a1, boolean a2) throws Z3Exception |
static long | mkFpaToIeeeBv (long a0, long a1) throws Z3Exception |
static long | mkFpaToFpIntReal (long a0, long a1, long a2, long a3, long a4) throws Z3Exception |
static int | fixedpointQueryFromLvl (long a0, long a1, long a2, int a3) throws Z3Exception |
static long | fixedpointGetGroundSatAnswer (long a0, long a1) throws Z3Exception |
static long | fixedpointGetRulesAlongTrace (long a0, long a1) throws Z3Exception |
static long | fixedpointGetRuleNamesAlongTrace (long a0, long a1) throws Z3Exception |
static void | fixedpointAddInvariant (long a0, long a1, long a2, long a3) throws Z3Exception |
static long | fixedpointGetReachable (long a0, long a1, long a2) throws Z3Exception |
static long | qeModelProject (long a0, long a1, int a2, long[] a3, long a4) throws Z3Exception |
static long | qeModelProjectSkolem (long a0, long a1, int a2, long[] a3, long a4, long a5) throws Z3Exception |
static long | modelExtrapolate (long a0, long a1, long a2) throws Z3Exception |
static long | qeLite (long a0, long a1, long a2) throws Z3Exception |
Static Protected Member Functions | |
static native void | INTERNALglobalParamSet (String a0, String a1) |
static native void | INTERNALglobalParamResetAll () |
static native boolean | INTERNALglobalParamGet (String a0, StringPtr a1) |
static native long | INTERNALmkConfig () |
static native void | INTERNALdelConfig (long a0) |
static native void | INTERNALsetParamValue (long a0, String a1, String a2) |
static native long | INTERNALmkContext (long a0) |
static native long | INTERNALmkContextRc (long a0) |
static native void | INTERNALdelContext (long a0) |
static native void | INTERNALincRef (long a0, long a1) |
static native void | INTERNALdecRef (long a0, long a1) |
static native void | INTERNALupdateParamValue (long a0, String a1, String a2) |
static native void | INTERNALinterrupt (long a0) |
static native long | INTERNALmkParams (long a0) |
static native void | INTERNALparamsIncRef (long a0, long a1) |
static native void | INTERNALparamsDecRef (long a0, long a1) |
static native void | INTERNALparamsSetBool (long a0, long a1, long a2, boolean a3) |
static native void | INTERNALparamsSetUint (long a0, long a1, long a2, int a3) |
static native void | INTERNALparamsSetDouble (long a0, long a1, long a2, double a3) |
static native void | INTERNALparamsSetSymbol (long a0, long a1, long a2, long a3) |
static native String | INTERNALparamsToString (long a0, long a1) |
static native void | INTERNALparamsValidate (long a0, long a1, long a2) |
static native void | INTERNALparamDescrsIncRef (long a0, long a1) |
static native void | INTERNALparamDescrsDecRef (long a0, long a1) |
static native int | INTERNALparamDescrsGetKind (long a0, long a1, long a2) |
static native int | INTERNALparamDescrsSize (long a0, long a1) |
static native long | INTERNALparamDescrsGetName (long a0, long a1, int a2) |
static native String | INTERNALparamDescrsGetDocumentation (long a0, long a1, long a2) |
static native String | INTERNALparamDescrsToString (long a0, long a1) |
static native long | INTERNALmkIntSymbol (long a0, int a1) |
static native long | INTERNALmkStringSymbol (long a0, String a1) |
static native long | INTERNALmkUninterpretedSort (long a0, long a1) |
static native long | INTERNALmkBoolSort (long a0) |
static native long | INTERNALmkIntSort (long a0) |
static native long | INTERNALmkRealSort (long a0) |
static native long | INTERNALmkBvSort (long a0, int a1) |
static native long | INTERNALmkFiniteDomainSort (long a0, long a1, long a2) |
static native long | INTERNALmkArraySort (long a0, long a1, long a2) |
static native long | INTERNALmkArraySortN (long a0, int a1, long[] a2, long a3) |
static native long | INTERNALmkTupleSort (long a0, long a1, int a2, long[] a3, long[] a4, LongPtr a5, long[] a6) |
static native long | INTERNALmkEnumerationSort (long a0, long a1, int a2, long[] a3, long[] a4, long[] a5) |
static native long | INTERNALmkListSort (long a0, long a1, long a2, LongPtr a3, LongPtr a4, LongPtr a5, LongPtr a6, LongPtr a7, LongPtr a8) |
static native long | INTERNALmkConstructor (long a0, long a1, long a2, int a3, long[] a4, long[] a5, int[] a6) |
static native void | INTERNALdelConstructor (long a0, long a1) |
static native long | INTERNALmkDatatype (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALmkConstructorList (long a0, int a1, long[] a2) |
static native void | INTERNALdelConstructorList (long a0, long a1) |
static native void | INTERNALmkDatatypes (long a0, int a1, long[] a2, long[] a3, long[] a4) |
static native void | INTERNALqueryConstructor (long a0, long a1, int a2, LongPtr a3, LongPtr a4, long[] a5) |
static native long | INTERNALmkFuncDecl (long a0, long a1, int a2, long[] a3, long a4) |
static native long | INTERNALmkApp (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALmkConst (long a0, long a1, long a2) |
static native long | INTERNALmkFreshFuncDecl (long a0, String a1, int a2, long[] a3, long a4) |
static native long | INTERNALmkFreshConst (long a0, String a1, long a2) |
static native long | INTERNALmkRecFuncDecl (long a0, long a1, int a2, long[] a3, long a4) |
static native void | INTERNALaddRecDef (long a0, long a1, int a2, long[] a3, long a4) |
static native long | INTERNALmkTrue (long a0) |
static native long | INTERNALmkFalse (long a0) |
static native long | INTERNALmkEq (long a0, long a1, long a2) |
static native long | INTERNALmkDistinct (long a0, int a1, long[] a2) |
static native long | INTERNALmkNot (long a0, long a1) |
static native long | INTERNALmkIte (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkIff (long a0, long a1, long a2) |
static native long | INTERNALmkImplies (long a0, long a1, long a2) |
static native long | INTERNALmkXor (long a0, long a1, long a2) |
static native long | INTERNALmkAnd (long a0, int a1, long[] a2) |
static native long | INTERNALmkOr (long a0, int a1, long[] a2) |
static native long | INTERNALmkAdd (long a0, int a1, long[] a2) |
static native long | INTERNALmkMul (long a0, int a1, long[] a2) |
static native long | INTERNALmkSub (long a0, int a1, long[] a2) |
static native long | INTERNALmkUnaryMinus (long a0, long a1) |
static native long | INTERNALmkDiv (long a0, long a1, long a2) |
static native long | INTERNALmkMod (long a0, long a1, long a2) |
static native long | INTERNALmkRem (long a0, long a1, long a2) |
static native long | INTERNALmkPower (long a0, long a1, long a2) |
static native long | INTERNALmkLt (long a0, long a1, long a2) |
static native long | INTERNALmkLe (long a0, long a1, long a2) |
static native long | INTERNALmkGt (long a0, long a1, long a2) |
static native long | INTERNALmkGe (long a0, long a1, long a2) |
static native long | INTERNALmkDivides (long a0, long a1, long a2) |
static native long | INTERNALmkInt2real (long a0, long a1) |
static native long | INTERNALmkReal2int (long a0, long a1) |
static native long | INTERNALmkIsInt (long a0, long a1) |
static native long | INTERNALmkBvnot (long a0, long a1) |
static native long | INTERNALmkBvredand (long a0, long a1) |
static native long | INTERNALmkBvredor (long a0, long a1) |
static native long | INTERNALmkBvand (long a0, long a1, long a2) |
static native long | INTERNALmkBvor (long a0, long a1, long a2) |
static native long | INTERNALmkBvxor (long a0, long a1, long a2) |
static native long | INTERNALmkBvnand (long a0, long a1, long a2) |
static native long | INTERNALmkBvnor (long a0, long a1, long a2) |
static native long | INTERNALmkBvxnor (long a0, long a1, long a2) |
static native long | INTERNALmkBvneg (long a0, long a1) |
static native long | INTERNALmkBvadd (long a0, long a1, long a2) |
static native long | INTERNALmkBvsub (long a0, long a1, long a2) |
static native long | INTERNALmkBvmul (long a0, long a1, long a2) |
static native long | INTERNALmkBvudiv (long a0, long a1, long a2) |
static native long | INTERNALmkBvsdiv (long a0, long a1, long a2) |
static native long | INTERNALmkBvurem (long a0, long a1, long a2) |
static native long | INTERNALmkBvsrem (long a0, long a1, long a2) |
static native long | INTERNALmkBvsmod (long a0, long a1, long a2) |
static native long | INTERNALmkBvult (long a0, long a1, long a2) |
static native long | INTERNALmkBvslt (long a0, long a1, long a2) |
static native long | INTERNALmkBvule (long a0, long a1, long a2) |
static native long | INTERNALmkBvsle (long a0, long a1, long a2) |
static native long | INTERNALmkBvuge (long a0, long a1, long a2) |
static native long | INTERNALmkBvsge (long a0, long a1, long a2) |
static native long | INTERNALmkBvugt (long a0, long a1, long a2) |
static native long | INTERNALmkBvsgt (long a0, long a1, long a2) |
static native long | INTERNALmkConcat (long a0, long a1, long a2) |
static native long | INTERNALmkExtract (long a0, int a1, int a2, long a3) |
static native long | INTERNALmkSignExt (long a0, int a1, long a2) |
static native long | INTERNALmkZeroExt (long a0, int a1, long a2) |
static native long | INTERNALmkRepeat (long a0, int a1, long a2) |
static native long | INTERNALmkBvshl (long a0, long a1, long a2) |
static native long | INTERNALmkBvlshr (long a0, long a1, long a2) |
static native long | INTERNALmkBvashr (long a0, long a1, long a2) |
static native long | INTERNALmkRotateLeft (long a0, int a1, long a2) |
static native long | INTERNALmkRotateRight (long a0, int a1, long a2) |
static native long | INTERNALmkExtRotateLeft (long a0, long a1, long a2) |
static native long | INTERNALmkExtRotateRight (long a0, long a1, long a2) |
static native long | INTERNALmkInt2bv (long a0, int a1, long a2) |
static native long | INTERNALmkBv2int (long a0, long a1, boolean a2) |
static native long | INTERNALmkBvaddNoOverflow (long a0, long a1, long a2, boolean a3) |
static native long | INTERNALmkBvaddNoUnderflow (long a0, long a1, long a2) |
static native long | INTERNALmkBvsubNoOverflow (long a0, long a1, long a2) |
static native long | INTERNALmkBvsubNoUnderflow (long a0, long a1, long a2, boolean a3) |
static native long | INTERNALmkBvsdivNoOverflow (long a0, long a1, long a2) |
static native long | INTERNALmkBvnegNoOverflow (long a0, long a1) |
static native long | INTERNALmkBvmulNoOverflow (long a0, long a1, long a2, boolean a3) |
static native long | INTERNALmkBvmulNoUnderflow (long a0, long a1, long a2) |
static native long | INTERNALmkSelect (long a0, long a1, long a2) |
static native long | INTERNALmkSelectN (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALmkStore (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkStoreN (long a0, long a1, int a2, long[] a3, long a4) |
static native long | INTERNALmkConstArray (long a0, long a1, long a2) |
static native long | INTERNALmkMap (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALmkArrayDefault (long a0, long a1) |
static native long | INTERNALmkAsArray (long a0, long a1) |
static native long | INTERNALmkSetHasSize (long a0, long a1, long a2) |
static native long | INTERNALmkSetSort (long a0, long a1) |
static native long | INTERNALmkEmptySet (long a0, long a1) |
static native long | INTERNALmkFullSet (long a0, long a1) |
static native long | INTERNALmkSetAdd (long a0, long a1, long a2) |
static native long | INTERNALmkSetDel (long a0, long a1, long a2) |
static native long | INTERNALmkSetUnion (long a0, int a1, long[] a2) |
static native long | INTERNALmkSetIntersect (long a0, int a1, long[] a2) |
static native long | INTERNALmkSetDifference (long a0, long a1, long a2) |
static native long | INTERNALmkSetComplement (long a0, long a1) |
static native long | INTERNALmkSetMember (long a0, long a1, long a2) |
static native long | INTERNALmkSetSubset (long a0, long a1, long a2) |
static native long | INTERNALmkArrayExt (long a0, long a1, long a2) |
static native long | INTERNALmkNumeral (long a0, String a1, long a2) |
static native long | INTERNALmkReal (long a0, int a1, int a2) |
static native long | INTERNALmkInt (long a0, int a1, long a2) |
static native long | INTERNALmkUnsignedInt (long a0, int a1, long a2) |
static native long | INTERNALmkInt64 (long a0, long a1, long a2) |
static native long | INTERNALmkUnsignedInt64 (long a0, long a1, long a2) |
static native long | INTERNALmkBvNumeral (long a0, int a1, boolean[] a2) |
static native long | INTERNALmkSeqSort (long a0, long a1) |
static native boolean | INTERNALisSeqSort (long a0, long a1) |
static native long | INTERNALgetSeqSortBasis (long a0, long a1) |
static native long | INTERNALmkReSort (long a0, long a1) |
static native boolean | INTERNALisReSort (long a0, long a1) |
static native long | INTERNALgetReSortBasis (long a0, long a1) |
static native long | INTERNALmkStringSort (long a0) |
static native boolean | INTERNALisStringSort (long a0, long a1) |
static native long | INTERNALmkString (long a0, String a1) |
static native long | INTERNALmkLstring (long a0, int a1, String a2) |
static native boolean | INTERNALisString (long a0, long a1) |
static native String | INTERNALgetString (long a0, long a1) |
static native long | INTERNALgetLstring (long a0, long a1, IntPtr a2) |
static native long | INTERNALmkSeqEmpty (long a0, long a1) |
static native long | INTERNALmkSeqUnit (long a0, long a1) |
static native long | INTERNALmkSeqConcat (long a0, int a1, long[] a2) |
static native long | INTERNALmkSeqPrefix (long a0, long a1, long a2) |
static native long | INTERNALmkSeqSuffix (long a0, long a1, long a2) |
static native long | INTERNALmkSeqContains (long a0, long a1, long a2) |
static native long | INTERNALmkStrLt (long a0, long a1, long a2) |
static native long | INTERNALmkStrLe (long a0, long a1, long a2) |
static native long | INTERNALmkSeqExtract (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkSeqReplace (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkSeqAt (long a0, long a1, long a2) |
static native long | INTERNALmkSeqNth (long a0, long a1, long a2) |
static native long | INTERNALmkSeqLength (long a0, long a1) |
static native long | INTERNALmkSeqIndex (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkSeqLastIndex (long a0, long a1, long a2) |
static native long | INTERNALmkStrToInt (long a0, long a1) |
static native long | INTERNALmkIntToStr (long a0, long a1) |
static native long | INTERNALmkSeqToRe (long a0, long a1) |
static native long | INTERNALmkSeqInRe (long a0, long a1, long a2) |
static native long | INTERNALmkRePlus (long a0, long a1) |
static native long | INTERNALmkReStar (long a0, long a1) |
static native long | INTERNALmkReOption (long a0, long a1) |
static native long | INTERNALmkReUnion (long a0, int a1, long[] a2) |
static native long | INTERNALmkReConcat (long a0, int a1, long[] a2) |
static native long | INTERNALmkReRange (long a0, long a1, long a2) |
static native long | INTERNALmkReLoop (long a0, long a1, int a2, int a3) |
static native long | INTERNALmkReIntersect (long a0, int a1, long[] a2) |
static native long | INTERNALmkReComplement (long a0, long a1) |
static native long | INTERNALmkReEmpty (long a0, long a1) |
static native long | INTERNALmkReFull (long a0, long a1) |
static native long | INTERNALmkLinearOrder (long a0, long a1, int a2) |
static native long | INTERNALmkPartialOrder (long a0, long a1, int a2) |
static native long | INTERNALmkPiecewiseLinearOrder (long a0, long a1, int a2) |
static native long | INTERNALmkTreeOrder (long a0, long a1, int a2) |
static native long | INTERNALmkTransitiveClosure (long a0, long a1) |
static native long | INTERNALmkPattern (long a0, int a1, long[] a2) |
static native long | INTERNALmkBound (long a0, int a1, long a2) |
static native long | INTERNALmkForall (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7) |
static native long | INTERNALmkExists (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long[] a6, long a7) |
static native long | INTERNALmkQuantifier (long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long[] a7, long a8) |
static native long | INTERNALmkQuantifierEx (long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long[] a11, long a12) |
static native long | INTERNALmkForallConst (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6) |
static native long | INTERNALmkExistsConst (long a0, int a1, int a2, long[] a3, int a4, long[] a5, long a6) |
static native long | INTERNALmkQuantifierConst (long a0, boolean a1, int a2, int a3, long[] a4, int a5, long[] a6, long a7) |
static native long | INTERNALmkQuantifierConstEx (long a0, boolean a1, int a2, long a3, long a4, int a5, long[] a6, int a7, long[] a8, int a9, long[] a10, long a11) |
static native long | INTERNALmkLambda (long a0, int a1, long[] a2, long[] a3, long a4) |
static native long | INTERNALmkLambdaConst (long a0, int a1, long[] a2, long a3) |
static native int | INTERNALgetSymbolKind (long a0, long a1) |
static native int | INTERNALgetSymbolInt (long a0, long a1) |
static native String | INTERNALgetSymbolString (long a0, long a1) |
static native long | INTERNALgetSortName (long a0, long a1) |
static native int | INTERNALgetSortId (long a0, long a1) |
static native long | INTERNALsortToAst (long a0, long a1) |
static native boolean | INTERNALisEqSort (long a0, long a1, long a2) |
static native int | INTERNALgetSortKind (long a0, long a1) |
static native int | INTERNALgetBvSortSize (long a0, long a1) |
static native boolean | INTERNALgetFiniteDomainSortSize (long a0, long a1, LongPtr a2) |
static native long | INTERNALgetArraySortDomain (long a0, long a1) |
static native long | INTERNALgetArraySortRange (long a0, long a1) |
static native long | INTERNALgetTupleSortMkDecl (long a0, long a1) |
static native int | INTERNALgetTupleSortNumFields (long a0, long a1) |
static native long | INTERNALgetTupleSortFieldDecl (long a0, long a1, int a2) |
static native int | INTERNALgetDatatypeSortNumConstructors (long a0, long a1) |
static native long | INTERNALgetDatatypeSortConstructor (long a0, long a1, int a2) |
static native long | INTERNALgetDatatypeSortRecognizer (long a0, long a1, int a2) |
static native long | INTERNALgetDatatypeSortConstructorAccessor (long a0, long a1, int a2, int a3) |
static native long | INTERNALdatatypeUpdateField (long a0, long a1, long a2, long a3) |
static native int | INTERNALgetRelationArity (long a0, long a1) |
static native long | INTERNALgetRelationColumn (long a0, long a1, int a2) |
static native long | INTERNALmkAtmost (long a0, int a1, long[] a2, int a3) |
static native long | INTERNALmkAtleast (long a0, int a1, long[] a2, int a3) |
static native long | INTERNALmkPble (long a0, int a1, long[] a2, int[] a3, int a4) |
static native long | INTERNALmkPbge (long a0, int a1, long[] a2, int[] a3, int a4) |
static native long | INTERNALmkPbeq (long a0, int a1, long[] a2, int[] a3, int a4) |
static native long | INTERNALfuncDeclToAst (long a0, long a1) |
static native boolean | INTERNALisEqFuncDecl (long a0, long a1, long a2) |
static native int | INTERNALgetFuncDeclId (long a0, long a1) |
static native long | INTERNALgetDeclName (long a0, long a1) |
static native int | INTERNALgetDeclKind (long a0, long a1) |
static native int | INTERNALgetDomainSize (long a0, long a1) |
static native int | INTERNALgetArity (long a0, long a1) |
static native long | INTERNALgetDomain (long a0, long a1, int a2) |
static native long | INTERNALgetRange (long a0, long a1) |
static native int | INTERNALgetDeclNumParameters (long a0, long a1) |
static native int | INTERNALgetDeclParameterKind (long a0, long a1, int a2) |
static native int | INTERNALgetDeclIntParameter (long a0, long a1, int a2) |
static native double | INTERNALgetDeclDoubleParameter (long a0, long a1, int a2) |
static native long | INTERNALgetDeclSymbolParameter (long a0, long a1, int a2) |
static native long | INTERNALgetDeclSortParameter (long a0, long a1, int a2) |
static native long | INTERNALgetDeclAstParameter (long a0, long a1, int a2) |
static native long | INTERNALgetDeclFuncDeclParameter (long a0, long a1, int a2) |
static native String | INTERNALgetDeclRationalParameter (long a0, long a1, int a2) |
static native long | INTERNALappToAst (long a0, long a1) |
static native long | INTERNALgetAppDecl (long a0, long a1) |
static native int | INTERNALgetAppNumArgs (long a0, long a1) |
static native long | INTERNALgetAppArg (long a0, long a1, int a2) |
static native boolean | INTERNALisEqAst (long a0, long a1, long a2) |
static native int | INTERNALgetAstId (long a0, long a1) |
static native int | INTERNALgetAstHash (long a0, long a1) |
static native long | INTERNALgetSort (long a0, long a1) |
static native boolean | INTERNALisWellSorted (long a0, long a1) |
static native int | INTERNALgetBoolValue (long a0, long a1) |
static native int | INTERNALgetAstKind (long a0, long a1) |
static native boolean | INTERNALisApp (long a0, long a1) |
static native boolean | INTERNALisNumeralAst (long a0, long a1) |
static native boolean | INTERNALisAlgebraicNumber (long a0, long a1) |
static native long | INTERNALtoApp (long a0, long a1) |
static native long | INTERNALtoFuncDecl (long a0, long a1) |
static native String | INTERNALgetNumeralString (long a0, long a1) |
static native String | INTERNALgetNumeralDecimalString (long a0, long a1, int a2) |
static native double | INTERNALgetNumeralDouble (long a0, long a1) |
static native long | INTERNALgetNumerator (long a0, long a1) |
static native long | INTERNALgetDenominator (long a0, long a1) |
static native boolean | INTERNALgetNumeralSmall (long a0, long a1, LongPtr a2, LongPtr a3) |
static native boolean | INTERNALgetNumeralInt (long a0, long a1, IntPtr a2) |
static native boolean | INTERNALgetNumeralUint (long a0, long a1, IntPtr a2) |
static native boolean | INTERNALgetNumeralUint64 (long a0, long a1, LongPtr a2) |
static native boolean | INTERNALgetNumeralInt64 (long a0, long a1, LongPtr a2) |
static native boolean | INTERNALgetNumeralRationalInt64 (long a0, long a1, LongPtr a2, LongPtr a3) |
static native long | INTERNALgetAlgebraicNumberLower (long a0, long a1, int a2) |
static native long | INTERNALgetAlgebraicNumberUpper (long a0, long a1, int a2) |
static native long | INTERNALpatternToAst (long a0, long a1) |
static native int | INTERNALgetPatternNumTerms (long a0, long a1) |
static native long | INTERNALgetPattern (long a0, long a1, int a2) |
static native int | INTERNALgetIndexValue (long a0, long a1) |
static native boolean | INTERNALisQuantifierForall (long a0, long a1) |
static native boolean | INTERNALisQuantifierExists (long a0, long a1) |
static native boolean | INTERNALisLambda (long a0, long a1) |
static native int | INTERNALgetQuantifierWeight (long a0, long a1) |
static native int | INTERNALgetQuantifierNumPatterns (long a0, long a1) |
static native long | INTERNALgetQuantifierPatternAst (long a0, long a1, int a2) |
static native int | INTERNALgetQuantifierNumNoPatterns (long a0, long a1) |
static native long | INTERNALgetQuantifierNoPatternAst (long a0, long a1, int a2) |
static native int | INTERNALgetQuantifierNumBound (long a0, long a1) |
static native long | INTERNALgetQuantifierBoundName (long a0, long a1, int a2) |
static native long | INTERNALgetQuantifierBoundSort (long a0, long a1, int a2) |
static native long | INTERNALgetQuantifierBody (long a0, long a1) |
static native long | INTERNALsimplify (long a0, long a1) |
static native long | INTERNALsimplifyEx (long a0, long a1, long a2) |
static native String | INTERNALsimplifyGetHelp (long a0) |
static native long | INTERNALsimplifyGetParamDescrs (long a0) |
static native long | INTERNALupdateTerm (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALsubstitute (long a0, long a1, int a2, long[] a3, long[] a4) |
static native long | INTERNALsubstituteVars (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALtranslate (long a0, long a1, long a2) |
static native long | INTERNALmkModel (long a0) |
static native void | INTERNALmodelIncRef (long a0, long a1) |
static native void | INTERNALmodelDecRef (long a0, long a1) |
static native boolean | INTERNALmodelEval (long a0, long a1, long a2, boolean a3, LongPtr a4) |
static native long | INTERNALmodelGetConstInterp (long a0, long a1, long a2) |
static native boolean | INTERNALmodelHasInterp (long a0, long a1, long a2) |
static native long | INTERNALmodelGetFuncInterp (long a0, long a1, long a2) |
static native int | INTERNALmodelGetNumConsts (long a0, long a1) |
static native long | INTERNALmodelGetConstDecl (long a0, long a1, int a2) |
static native int | INTERNALmodelGetNumFuncs (long a0, long a1) |
static native long | INTERNALmodelGetFuncDecl (long a0, long a1, int a2) |
static native int | INTERNALmodelGetNumSorts (long a0, long a1) |
static native long | INTERNALmodelGetSort (long a0, long a1, int a2) |
static native long | INTERNALmodelGetSortUniverse (long a0, long a1, long a2) |
static native long | INTERNALmodelTranslate (long a0, long a1, long a2) |
static native boolean | INTERNALisAsArray (long a0, long a1) |
static native long | INTERNALgetAsArrayFuncDecl (long a0, long a1) |
static native long | INTERNALaddFuncInterp (long a0, long a1, long a2, long a3) |
static native void | INTERNALaddConstInterp (long a0, long a1, long a2, long a3) |
static native void | INTERNALfuncInterpIncRef (long a0, long a1) |
static native void | INTERNALfuncInterpDecRef (long a0, long a1) |
static native int | INTERNALfuncInterpGetNumEntries (long a0, long a1) |
static native long | INTERNALfuncInterpGetEntry (long a0, long a1, int a2) |
static native long | INTERNALfuncInterpGetElse (long a0, long a1) |
static native void | INTERNALfuncInterpSetElse (long a0, long a1, long a2) |
static native int | INTERNALfuncInterpGetArity (long a0, long a1) |
static native void | INTERNALfuncInterpAddEntry (long a0, long a1, long a2, long a3) |
static native void | INTERNALfuncEntryIncRef (long a0, long a1) |
static native void | INTERNALfuncEntryDecRef (long a0, long a1) |
static native long | INTERNALfuncEntryGetValue (long a0, long a1) |
static native int | INTERNALfuncEntryGetNumArgs (long a0, long a1) |
static native long | INTERNALfuncEntryGetArg (long a0, long a1, int a2) |
static native int | INTERNALopenLog (String a0) |
static native void | INTERNALappendLog (String a0) |
static native void | INTERNALcloseLog () |
static native void | INTERNALtoggleWarningMessages (boolean a0) |
static native void | INTERNALsetAstPrintMode (long a0, int a1) |
static native String | INTERNALastToString (long a0, long a1) |
static native String | INTERNALpatternToString (long a0, long a1) |
static native String | INTERNALsortToString (long a0, long a1) |
static native String | INTERNALfuncDeclToString (long a0, long a1) |
static native String | INTERNALmodelToString (long a0, long a1) |
static native String | INTERNALbenchmarkToSmtlibString (long a0, String a1, String a2, String a3, String a4, int a5, long[] a6, long a7) |
static native long | INTERNALparseSmtlib2String (long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7) |
static native long | INTERNALparseSmtlib2File (long a0, String a1, int a2, long[] a3, long[] a4, int a5, long[] a6, long[] a7) |
static native String | INTERNALevalSmtlib2String (long a0, String a1) |
static native int | INTERNALgetErrorCode (long a0) |
static native void | INTERNALsetError (long a0, int a1) |
static native String | INTERNALgetErrorMsg (long a0, int a1) |
static native void | INTERNALgetVersion (IntPtr a0, IntPtr a1, IntPtr a2, IntPtr a3) |
static native String | INTERNALgetFullVersion () |
static native void | INTERNALenableTrace (String a0) |
static native void | INTERNALdisableTrace (String a0) |
static native void | INTERNALresetMemory () |
static native void | INTERNALfinalizeMemory () |
static native long | INTERNALmkGoal (long a0, boolean a1, boolean a2, boolean a3) |
static native void | INTERNALgoalIncRef (long a0, long a1) |
static native void | INTERNALgoalDecRef (long a0, long a1) |
static native int | INTERNALgoalPrecision (long a0, long a1) |
static native void | INTERNALgoalAssert (long a0, long a1, long a2) |
static native boolean | INTERNALgoalInconsistent (long a0, long a1) |
static native int | INTERNALgoalDepth (long a0, long a1) |
static native void | INTERNALgoalReset (long a0, long a1) |
static native int | INTERNALgoalSize (long a0, long a1) |
static native long | INTERNALgoalFormula (long a0, long a1, int a2) |
static native int | INTERNALgoalNumExprs (long a0, long a1) |
static native boolean | INTERNALgoalIsDecidedSat (long a0, long a1) |
static native boolean | INTERNALgoalIsDecidedUnsat (long a0, long a1) |
static native long | INTERNALgoalTranslate (long a0, long a1, long a2) |
static native long | INTERNALgoalConvertModel (long a0, long a1, long a2) |
static native String | INTERNALgoalToString (long a0, long a1) |
static native String | INTERNALgoalToDimacsString (long a0, long a1) |
static native long | INTERNALmkTactic (long a0, String a1) |
static native void | INTERNALtacticIncRef (long a0, long a1) |
static native void | INTERNALtacticDecRef (long a0, long a1) |
static native long | INTERNALmkProbe (long a0, String a1) |
static native void | INTERNALprobeIncRef (long a0, long a1) |
static native void | INTERNALprobeDecRef (long a0, long a1) |
static native long | INTERNALtacticAndThen (long a0, long a1, long a2) |
static native long | INTERNALtacticOrElse (long a0, long a1, long a2) |
static native long | INTERNALtacticParOr (long a0, int a1, long[] a2) |
static native long | INTERNALtacticParAndThen (long a0, long a1, long a2) |
static native long | INTERNALtacticTryFor (long a0, long a1, int a2) |
static native long | INTERNALtacticWhen (long a0, long a1, long a2) |
static native long | INTERNALtacticCond (long a0, long a1, long a2, long a3) |
static native long | INTERNALtacticRepeat (long a0, long a1, int a2) |
static native long | INTERNALtacticSkip (long a0) |
static native long | INTERNALtacticFail (long a0) |
static native long | INTERNALtacticFailIf (long a0, long a1) |
static native long | INTERNALtacticFailIfNotDecided (long a0) |
static native long | INTERNALtacticUsingParams (long a0, long a1, long a2) |
static native long | INTERNALprobeConst (long a0, double a1) |
static native long | INTERNALprobeLt (long a0, long a1, long a2) |
static native long | INTERNALprobeGt (long a0, long a1, long a2) |
static native long | INTERNALprobeLe (long a0, long a1, long a2) |
static native long | INTERNALprobeGe (long a0, long a1, long a2) |
static native long | INTERNALprobeEq (long a0, long a1, long a2) |
static native long | INTERNALprobeAnd (long a0, long a1, long a2) |
static native long | INTERNALprobeOr (long a0, long a1, long a2) |
static native long | INTERNALprobeNot (long a0, long a1) |
static native int | INTERNALgetNumTactics (long a0) |
static native String | INTERNALgetTacticName (long a0, int a1) |
static native int | INTERNALgetNumProbes (long a0) |
static native String | INTERNALgetProbeName (long a0, int a1) |
static native String | INTERNALtacticGetHelp (long a0, long a1) |
static native long | INTERNALtacticGetParamDescrs (long a0, long a1) |
static native String | INTERNALtacticGetDescr (long a0, String a1) |
static native String | INTERNALprobeGetDescr (long a0, String a1) |
static native double | INTERNALprobeApply (long a0, long a1, long a2) |
static native long | INTERNALtacticApply (long a0, long a1, long a2) |
static native long | INTERNALtacticApplyEx (long a0, long a1, long a2, long a3) |
static native void | INTERNALapplyResultIncRef (long a0, long a1) |
static native void | INTERNALapplyResultDecRef (long a0, long a1) |
static native String | INTERNALapplyResultToString (long a0, long a1) |
static native int | INTERNALapplyResultGetNumSubgoals (long a0, long a1) |
static native long | INTERNALapplyResultGetSubgoal (long a0, long a1, int a2) |
static native long | INTERNALmkSolver (long a0) |
static native long | INTERNALmkSimpleSolver (long a0) |
static native long | INTERNALmkSolverForLogic (long a0, long a1) |
static native long | INTERNALmkSolverFromTactic (long a0, long a1) |
static native long | INTERNALsolverTranslate (long a0, long a1, long a2) |
static native void | INTERNALsolverImportModelConverter (long a0, long a1, long a2) |
static native String | INTERNALsolverGetHelp (long a0, long a1) |
static native long | INTERNALsolverGetParamDescrs (long a0, long a1) |
static native void | INTERNALsolverSetParams (long a0, long a1, long a2) |
static native void | INTERNALsolverIncRef (long a0, long a1) |
static native void | INTERNALsolverDecRef (long a0, long a1) |
static native void | INTERNALsolverInterrupt (long a0, long a1) |
static native void | INTERNALsolverPush (long a0, long a1) |
static native void | INTERNALsolverPop (long a0, long a1, int a2) |
static native void | INTERNALsolverReset (long a0, long a1) |
static native int | INTERNALsolverGetNumScopes (long a0, long a1) |
static native void | INTERNALsolverAssert (long a0, long a1, long a2) |
static native void | INTERNALsolverAssertAndTrack (long a0, long a1, long a2, long a3) |
static native void | INTERNALsolverFromFile (long a0, long a1, String a2) |
static native void | INTERNALsolverFromString (long a0, long a1, String a2) |
static native long | INTERNALsolverGetAssertions (long a0, long a1) |
static native long | INTERNALsolverGetUnits (long a0, long a1) |
static native long | INTERNALsolverGetTrail (long a0, long a1) |
static native long | INTERNALsolverGetNonUnits (long a0, long a1) |
static native void | INTERNALsolverGetLevels (long a0, long a1, long a2, int a3, int[] a4) |
static native int | INTERNALsolverCheck (long a0, long a1) |
static native int | INTERNALsolverCheckAssumptions (long a0, long a1, int a2, long[] a3) |
static native int | INTERNALgetImpliedEqualities (long a0, long a1, int a2, long[] a3, int[] a4) |
static native int | INTERNALsolverGetConsequences (long a0, long a1, long a2, long a3, long a4) |
static native long | INTERNALsolverCube (long a0, long a1, long a2, int a3) |
static native long | INTERNALsolverGetModel (long a0, long a1) |
static native long | INTERNALsolverGetProof (long a0, long a1) |
static native long | INTERNALsolverGetUnsatCore (long a0, long a1) |
static native String | INTERNALsolverGetReasonUnknown (long a0, long a1) |
static native long | INTERNALsolverGetStatistics (long a0, long a1) |
static native String | INTERNALsolverToString (long a0, long a1) |
static native String | INTERNALsolverToDimacsString (long a0, long a1, boolean a2) |
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 | INTERNALalgebraicGetPoly (long a0, long a1) |
static native int | INTERNALalgebraicGetI (long a0, long a1) |
static native long | INTERNALpolynomialSubresultants (long a0, long a1, long a2, long a3) |
static native void | INTERNALrcfDel (long a0, long a1) |
static native long | INTERNALrcfMkRational (long a0, String a1) |
static native long | INTERNALrcfMkSmallInt (long a0, int a1) |
static native long | INTERNALrcfMkPi (long a0) |
static native long | INTERNALrcfMkE (long a0) |
static native long | INTERNALrcfMkInfinitesimal (long a0) |
static native int | INTERNALrcfMkRoots (long a0, int a1, long[] a2, long[] a3) |
static native long | INTERNALrcfAdd (long a0, long a1, long a2) |
static native long | INTERNALrcfSub (long a0, long a1, long a2) |
static native long | INTERNALrcfMul (long a0, long a1, long a2) |
static native long | INTERNALrcfDiv (long a0, long a1, long a2) |
static native long | INTERNALrcfNeg (long a0, long a1) |
static native long | INTERNALrcfInv (long a0, long a1) |
static native long | INTERNALrcfPower (long a0, long a1, int a2) |
static native boolean | INTERNALrcfLt (long a0, long a1, long a2) |
static native boolean | INTERNALrcfGt (long a0, long a1, long a2) |
static native boolean | INTERNALrcfLe (long a0, long a1, long a2) |
static native boolean | INTERNALrcfGe (long a0, long a1, long a2) |
static native boolean | INTERNALrcfEq (long a0, long a1, long a2) |
static native boolean | INTERNALrcfNeq (long a0, long a1, long a2) |
static native String | INTERNALrcfNumToString (long a0, long a1, boolean a2, boolean a3) |
static native String | INTERNALrcfNumToDecimalString (long a0, long a1, int a2) |
static native void | INTERNALrcfGetNumeratorDenominator (long a0, long a1, LongPtr a2, LongPtr a3) |
static native long | INTERNALmkFixedpoint (long a0) |
static native void | INTERNALfixedpointIncRef (long a0, long a1) |
static native void | INTERNALfixedpointDecRef (long a0, long a1) |
static native void | INTERNALfixedpointAddRule (long a0, long a1, long a2, long a3) |
static native void | INTERNALfixedpointAddFact (long a0, long a1, long a2, int a3, int[] a4) |
static native void | INTERNALfixedpointAssert (long a0, long a1, long a2) |
static native int | INTERNALfixedpointQuery (long a0, long a1, long a2) |
static native int | INTERNALfixedpointQueryRelations (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALfixedpointGetAnswer (long a0, long a1) |
static native String | INTERNALfixedpointGetReasonUnknown (long a0, long a1) |
static native void | INTERNALfixedpointUpdateRule (long a0, long a1, long a2, long a3) |
static native int | INTERNALfixedpointGetNumLevels (long a0, long a1, long a2) |
static native long | INTERNALfixedpointGetCoverDelta (long a0, long a1, int a2, long a3) |
static native void | INTERNALfixedpointAddCover (long a0, long a1, int a2, long a3, long a4) |
static native long | INTERNALfixedpointGetStatistics (long a0, long a1) |
static native void | INTERNALfixedpointRegisterRelation (long a0, long a1, long a2) |
static native void | INTERNALfixedpointSetPredicateRepresentation (long a0, long a1, long a2, int a3, long[] a4) |
static native long | INTERNALfixedpointGetRules (long a0, long a1) |
static native long | INTERNALfixedpointGetAssertions (long a0, long a1) |
static native void | INTERNALfixedpointSetParams (long a0, long a1, long a2) |
static native String | INTERNALfixedpointGetHelp (long a0, long a1) |
static native long | INTERNALfixedpointGetParamDescrs (long a0, long a1) |
static native String | INTERNALfixedpointToString (long a0, long a1, int a2, long[] a3) |
static native long | INTERNALfixedpointFromString (long a0, long a1, String a2) |
static native long | INTERNALfixedpointFromFile (long a0, long a1, String a2) |
static native long | INTERNALmkOptimize (long a0) |
static native void | INTERNALoptimizeIncRef (long a0, long a1) |
static native void | INTERNALoptimizeDecRef (long a0, long a1) |
static native void | INTERNALoptimizeAssert (long a0, long a1, long a2) |
static native void | INTERNALoptimizeAssertAndTrack (long a0, long a1, long a2, long a3) |
static native int | INTERNALoptimizeAssertSoft (long a0, long a1, long a2, String a3, long a4) |
static native int | INTERNALoptimizeMaximize (long a0, long a1, long a2) |
static native int | INTERNALoptimizeMinimize (long a0, long a1, long a2) |
static native void | INTERNALoptimizePush (long a0, long a1) |
static native void | INTERNALoptimizePop (long a0, long a1) |
static native int | INTERNALoptimizeCheck (long a0, long a1, int a2, long[] a3) |
static native String | INTERNALoptimizeGetReasonUnknown (long a0, long a1) |
static native long | INTERNALoptimizeGetModel (long a0, long a1) |
static native long | INTERNALoptimizeGetUnsatCore (long a0, long a1) |
static native void | INTERNALoptimizeSetParams (long a0, long a1, long a2) |
static native long | INTERNALoptimizeGetParamDescrs (long a0, long a1) |
static native long | INTERNALoptimizeGetLower (long a0, long a1, int a2) |
static native long | INTERNALoptimizeGetUpper (long a0, long a1, int a2) |
static native long | INTERNALoptimizeGetLowerAsVector (long a0, long a1, int a2) |
static native long | INTERNALoptimizeGetUpperAsVector (long a0, long a1, int a2) |
static native String | INTERNALoptimizeToString (long a0, long a1) |
static native void | INTERNALoptimizeFromString (long a0, long a1, String a2) |
static native void | INTERNALoptimizeFromFile (long a0, long a1, String a2) |
static native String | INTERNALoptimizeGetHelp (long a0, long a1) |
static native long | INTERNALoptimizeGetStatistics (long a0, long a1) |
static native long | INTERNALoptimizeGetAssertions (long a0, long a1) |
static native long | INTERNALoptimizeGetObjectives (long a0, long a1) |
static native long | INTERNALmkFpaRoundingModeSort (long a0) |
static native long | INTERNALmkFpaRoundNearestTiesToEven (long a0) |
static native long | INTERNALmkFpaRne (long a0) |
static native long | INTERNALmkFpaRoundNearestTiesToAway (long a0) |
static native long | INTERNALmkFpaRna (long a0) |
static native long | INTERNALmkFpaRoundTowardPositive (long a0) |
static native long | INTERNALmkFpaRtp (long a0) |
static native long | INTERNALmkFpaRoundTowardNegative (long a0) |
static native long | INTERNALmkFpaRtn (long a0) |
static native long | INTERNALmkFpaRoundTowardZero (long a0) |
static native long | INTERNALmkFpaRtz (long a0) |
static native long | INTERNALmkFpaSort (long a0, int a1, int a2) |
static native long | INTERNALmkFpaSortHalf (long a0) |
static native long | INTERNALmkFpaSort16 (long a0) |
static native long | INTERNALmkFpaSortSingle (long a0) |
static native long | INTERNALmkFpaSort32 (long a0) |
static native long | INTERNALmkFpaSortDouble (long a0) |
static native long | INTERNALmkFpaSort64 (long a0) |
static native long | INTERNALmkFpaSortQuadruple (long a0) |
static native long | INTERNALmkFpaSort128 (long a0) |
static native long | INTERNALmkFpaNan (long a0, long a1) |
static native long | INTERNALmkFpaInf (long a0, long a1, boolean a2) |
static native long | INTERNALmkFpaZero (long a0, long a1, boolean a2) |
static native long | INTERNALmkFpaFp (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaNumeralFloat (long a0, float a1, long a2) |
static native long | INTERNALmkFpaNumeralDouble (long a0, double a1, long a2) |
static native long | INTERNALmkFpaNumeralInt (long a0, int a1, long a2) |
static native long | INTERNALmkFpaNumeralIntUint (long a0, boolean a1, int a2, int a3, long a4) |
static native long | INTERNALmkFpaNumeralInt64Uint64 (long a0, boolean a1, long a2, long a3, long a4) |
static native long | INTERNALmkFpaAbs (long a0, long a1) |
static native long | INTERNALmkFpaNeg (long a0, long a1) |
static native long | INTERNALmkFpaAdd (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaSub (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaMul (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaDiv (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaFma (long a0, long a1, long a2, long a3, long a4) |
static native long | INTERNALmkFpaSqrt (long a0, long a1, long a2) |
static native long | INTERNALmkFpaRem (long a0, long a1, long a2) |
static native long | INTERNALmkFpaRoundToIntegral (long a0, long a1, long a2) |
static native long | INTERNALmkFpaMin (long a0, long a1, long a2) |
static native long | INTERNALmkFpaMax (long a0, long a1, long a2) |
static native long | INTERNALmkFpaLeq (long a0, long a1, long a2) |
static native long | INTERNALmkFpaLt (long a0, long a1, long a2) |
static native long | INTERNALmkFpaGeq (long a0, long a1, long a2) |
static native long | INTERNALmkFpaGt (long a0, long a1, long a2) |
static native long | INTERNALmkFpaEq (long a0, long a1, long a2) |
static native long | INTERNALmkFpaIsNormal (long a0, long a1) |
static native long | INTERNALmkFpaIsSubnormal (long a0, long a1) |
static native long | INTERNALmkFpaIsZero (long a0, long a1) |
static native long | INTERNALmkFpaIsInfinite (long a0, long a1) |
static native long | INTERNALmkFpaIsNan (long a0, long a1) |
static native long | INTERNALmkFpaIsNegative (long a0, long a1) |
static native long | INTERNALmkFpaIsPositive (long a0, long a1) |
static native long | INTERNALmkFpaToFpBv (long a0, long a1, long a2) |
static native long | INTERNALmkFpaToFpFloat (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaToFpReal (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaToFpSigned (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaToFpUnsigned (long a0, long a1, long a2, long a3) |
static native long | INTERNALmkFpaToUbv (long a0, long a1, long a2, int a3) |
static native long | INTERNALmkFpaToSbv (long a0, long a1, long a2, int a3) |
static native long | INTERNALmkFpaToReal (long a0, long a1) |
static native int | INTERNALfpaGetEbits (long a0, long a1) |
static native int | INTERNALfpaGetSbits (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralNan (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralInf (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralZero (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralNormal (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralSubnormal (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralPositive (long a0, long a1) |
static native boolean | INTERNALfpaIsNumeralNegative (long a0, long a1) |
static native long | INTERNALfpaGetNumeralSignBv (long a0, long a1) |
static native long | INTERNALfpaGetNumeralSignificandBv (long a0, long a1) |
static native boolean | INTERNALfpaGetNumeralSign (long a0, long a1, IntPtr a2) |
static native String | INTERNALfpaGetNumeralSignificandString (long a0, long a1) |
static native boolean | INTERNALfpaGetNumeralSignificandUint64 (long a0, long a1, LongPtr a2) |
static native String | INTERNALfpaGetNumeralExponentString (long a0, long a1, boolean a2) |
static native boolean | INTERNALfpaGetNumeralExponentInt64 (long a0, long a1, LongPtr a2, boolean a3) |
static native long | INTERNALfpaGetNumeralExponentBv (long a0, long a1, boolean a2) |
static native long | INTERNALmkFpaToIeeeBv (long a0, long a1) |
static native long | INTERNALmkFpaToFpIntReal (long a0, long a1, long a2, long a3, long a4) |
static native int | INTERNALfixedpointQueryFromLvl (long a0, long a1, long a2, int a3) |
static native long | INTERNALfixedpointGetGroundSatAnswer (long a0, long a1) |
static native long | INTERNALfixedpointGetRulesAlongTrace (long a0, long a1) |
static native long | INTERNALfixedpointGetRuleNamesAlongTrace (long a0, long a1) |
static native void | INTERNALfixedpointAddInvariant (long a0, long a1, long a2, long a3) |
static native long | INTERNALfixedpointGetReachable (long a0, long a1, long a2) |
static native long | INTERNALqeModelProject (long a0, long a1, int a2, long[] a3, long a4) |
static native long | INTERNALqeModelProjectSkolem (long a0, long a1, int a2, long[] a3, long a4, long a5) |
static native long | INTERNALmodelExtrapolate (long a0, long a1, long a2) |
static native long | INTERNALqeLite (long a0, long a1, long a2) |
Definition at line 4 of file Native.java.
|
inlinestatic |
Definition at line 3674 of file Native.java.
|
inlinestatic |
Definition at line 3665 of file Native.java.
|
inlinestatic |
Definition at line 1157 of file Native.java.
|
inlinestatic |
Definition at line 5125 of file Native.java.
|
inlinestatic |
Definition at line 5152 of file Native.java.
|
inlinestatic |
Definition at line 5215 of file Native.java.
|
inlinestatic |
Definition at line 5242 of file Native.java.
|
inlinestatic |
Definition at line 5206 of file Native.java.
|
inlinestatic |
Definition at line 5260 of file Native.java.
|
inlinestatic |
Definition at line 5251 of file Native.java.
|
inlinestatic |
Definition at line 5188 of file Native.java.
|
inlinestatic |
Definition at line 5098 of file Native.java.
|
inlinestatic |
Definition at line 5089 of file Native.java.
|
inlinestatic |
Definition at line 5080 of file Native.java.
|
inlinestatic |
Definition at line 5107 of file Native.java.
|
inlinestatic |
Definition at line 5197 of file Native.java.
|
inlinestatic |
Definition at line 5179 of file Native.java.
|
inlinestatic |
Definition at line 5143 of file Native.java.
|
inlinestatic |
Definition at line 5224 of file Native.java.
|
inlinestatic |
Definition at line 5170 of file Native.java.
|
inlinestatic |
Definition at line 5161 of file Native.java.
|
inlinestatic |
Definition at line 5233 of file Native.java.
|
inlinestatic |
Definition at line 5116 of file Native.java.
|
inlinestatic |
Definition at line 5134 of file Native.java.
|
inlinestatic |
Definition at line 3799 of file Native.java.
Referenced by Log.append().
|
inlinestatic |
Definition at line 4461 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4453 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 3037 of file Native.java.
|
inlinestatic |
Definition at line 5011 of file Native.java.
|
inlinestatic |
Definition at line 5003 of file Native.java.
|
inlinestatic |
Definition at line 5037 of file Native.java.
|
inlinestatic |
Definition at line 5020 of file Native.java.
|
inlinestatic |
Definition at line 4995 of file Native.java.
|
inlinestatic |
Definition at line 5029 of file Native.java.
|
inlinestatic |
Definition at line 5062 of file Native.java.
|
inlinestatic |
Definition at line 5045 of file Native.java.
|
inlinestatic |
Definition at line 5053 of file Native.java.
|
inlinestatic |
Definition at line 5071 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4918 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4910 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3804 of file Native.java.
Referenced by Log.close().
|
inlinestatic |
|
inlinestatic |
Definition at line 768 of file Native.java.
|
inlinestatic |
Definition at line 729 of file Native.java.
Referenced by Context.Context().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 755 of file Native.java.
Referenced by Context.close().
|
inlinestatic |
Definition at line 3942 of file Native.java.
Referenced by Global.disableTrace().
|
inlinestatic |
Definition at line 3937 of file Native.java.
Referenced by Global.enableTrace().
|
inlinestatic |
Definition at line 3894 of file Native.java.
|
inlinestatic |
Definition at line 3952 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 6688 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 5500 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 6661 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 6696 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 6679 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 6670 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 5492 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 6652 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2875 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 3758 of file Native.java.
|
inlinestatic |
Definition at line 3784 of file Native.java.
|
inlinestatic |
Definition at line 3775 of file Native.java.
|
inlinestatic |
Definition at line 3766 of file Native.java.
|
inlinestatic |
Definition at line 3750 of file Native.java.
|
inlinestatic |
Definition at line 3742 of file Native.java.
|
inlinestatic |
Definition at line 3690 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3682 of file Native.java.
|
inlinestatic |
Definition at line 3725 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2776 of file Native.java.
Referenced by DatatypeSort.getAccessors(), ListSort.getConsDecl(), EnumSort.getConstDecl(), EnumSort.getConstDecls(), DatatypeSort.getConstructors(), and ListSort.getNilDecl().
|
inlinestatic |
Definition at line 2794 of file Native.java.
Referenced by DatatypeSort.getAccessors(), ListSort.getHeadDecl(), and ListSort.getTailDecl().
|
inlinestatic |
Definition at line 2767 of file Native.java.
Referenced by EnumSort.getConstDecls(), DatatypeSort.getNumConstructors(), and EnumSort.getTesterDecls().
|
inlinestatic |
Definition at line 2785 of file Native.java.
Referenced by ListSort.getIsConsDecl(), ListSort.getIsNilDecl(), DatatypeSort.getRecognizers(), EnumSort.getTesterDecl(), and EnumSort.getTesterDecls().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2965 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 3001 of file Native.java.
|
inlinestatic |
Definition at line 2992 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3903 of file Native.java.
|
inlinestatic |
Definition at line 3917 of file Native.java.
|
inlinestatic |
Definition at line 4895 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 3931 of file Native.java.
Referenced by Version.getFullVersion().
|
inlinestatic |
|
inlinestatic |
Definition at line 4726 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 2200 of file Native.java.
|
inlinestatic |
Definition at line 3190 of file Native.java.
Referenced by AlgebraicNum.toDecimal(), and RatNum.toDecimalString().
|
inlinestatic |
Definition at line 3199 of file Native.java.
|
inlinestatic |
Definition at line 3235 of file Native.java.
Referenced by BitVecNum.getInt(), IntNum.getInt(), and FiniteDomainNum.getInt().
|
inlinestatic |
Definition at line 3262 of file Native.java.
Referenced by IntNum.getInt64(), FiniteDomainNum.getInt64(), and BitVecNum.getLong().
|
inlinestatic |
Definition at line 3271 of file Native.java.
|
inlinestatic |
Definition at line 3226 of file Native.java.
|
inlinestatic |
Definition at line 3181 of file Native.java.
Referenced by IntNum.toString(), BitVecNum.toString(), FiniteDomainNum.toString(), RatNum.toString(), and FPNum.toString().
|
inlinestatic |
Definition at line 3244 of file Native.java.
|
inlinestatic |
Definition at line 3253 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3433 of file Native.java.
Referenced by Lambda.getBody(), and Quantifier.getBody().
|
inlinestatic |
Definition at line 3415 of file Native.java.
Referenced by Lambda.getBoundVariableNames(), and Quantifier.getBoundVariableNames().
|
inlinestatic |
Definition at line 3424 of file Native.java.
Referenced by Lambda.getBoundVariableSorts(), and Quantifier.getBoundVariableSorts().
|
inlinestatic |
|
inlinestatic |
Definition at line 3406 of file Native.java.
Referenced by Lambda.getNumBound(), and Quantifier.getNumBound().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2947 of file Native.java.
Referenced by Model.getFuncInterp(), and FuncDecl.getRange().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2137 of file Native.java.
|
inlinestatic |
Definition at line 2110 of file Native.java.
|
inlinestatic |
Definition at line 3100 of file Native.java.
Referenced by Expr.getSort(), Expr.isArray(), Expr.isBool(), Expr.isBV(), Expr.isFiniteDomain(), Expr.isInt(), Expr.isReal(), and Expr.isRelation().
|
inlinestatic |
|
inlinestatic |
Definition at line 2695 of file Native.java.
Referenced by Model.getFuncInterp(), Sort.getSortKind(), Expr.isArray(), Expr.isBV(), Expr.isInt(), and Expr.isReal().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3926 of file Native.java.
Referenced by Version.getBuild(), Version.getMajor(), Version.getMinor(), Version.getRevision(), and Version.getString().
|
inlinestatic |
Definition at line 717 of file Native.java.
Referenced by Global.getParameter().
|
inlinestatic |
Definition at line 712 of file Native.java.
Referenced by Global.resetParameters().
|
inlinestatic |
Definition at line 707 of file Native.java.
Referenced by Global.setParameter().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3974 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3966 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4097 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 760 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.algebraicGetI().
|
staticprotected |
Referenced by Native.algebraicGetPoly().
|
staticprotected |
Referenced by Native.algebraicGt().
|
staticprotected |
Referenced by Native.algebraicIsNeg().
|
staticprotected |
Referenced by Native.algebraicIsPos().
|
staticprotected |
Referenced by Native.algebraicIsValue().
|
staticprotected |
Referenced by Native.algebraicIsZero().
|
staticprotected |
Referenced by Native.algebraicLe().
|
staticprotected |
Referenced by Native.algebraicLt().
|
staticprotected |
Referenced by Native.algebraicMul().
|
staticprotected |
Referenced by Native.algebraicNeq().
|
staticprotected |
Referenced by Native.algebraicPower().
|
staticprotected |
Referenced by Native.algebraicRoot().
|
staticprotected |
Referenced by Native.algebraicRoots().
|
staticprotected |
Referenced by Native.algebraicSign().
|
staticprotected |
Referenced by Native.algebraicSub().
|
staticprotected |
Referenced by Native.appendLog().
|
staticprotected |
Referenced by Native.applyResultDecRef().
|
staticprotected |
Referenced by Native.applyResultGetNumSubgoals().
|
staticprotected |
Referenced by Native.applyResultGetSubgoal().
|
staticprotected |
Referenced by Native.applyResultIncRef().
|
staticprotected |
Referenced by Native.applyResultToString().
|
staticprotected |
Referenced by Native.appToAst().
|
staticprotected |
Referenced by Native.astMapContains().
|
staticprotected |
Referenced by Native.astMapDecRef().
|
staticprotected |
Referenced by Native.astMapErase().
|
staticprotected |
Referenced by Native.astMapFind().
|
staticprotected |
Referenced by Native.astMapIncRef().
|
staticprotected |
Referenced by Native.astMapInsert().
|
staticprotected |
Referenced by Native.astMapKeys().
|
staticprotected |
Referenced by Native.astMapReset().
|
staticprotected |
Referenced by Native.astMapSize().
|
staticprotected |
Referenced by Native.astMapToString().
|
staticprotected |
Referenced by Native.astToString().
|
staticprotected |
Referenced by Native.astVectorDecRef().
|
staticprotected |
Referenced by Native.astVectorGet().
|
staticprotected |
Referenced by Native.astVectorIncRef().
|
staticprotected |
Referenced by Native.astVectorPush().
|
staticprotected |
Referenced by Native.astVectorResize().
|
staticprotected |
Referenced by Native.astVectorSet().
|
staticprotected |
Referenced by Native.astVectorSize().
|
staticprotected |
Referenced by Native.astVectorToString().
|
staticprotected |
Referenced by Native.astVectorTranslate().
|
staticprotected |
Referenced by Native.benchmarkToSmtlibString().
|
staticprotected |
Referenced by Native.closeLog().
|
staticprotected |
Referenced by Native.datatypeUpdateField().
|
staticprotected |
Referenced by Native.decRef().
|
staticprotected |
Referenced by Native.delConfig().
|
staticprotected |
Referenced by Native.delConstructor().
|
staticprotected |
Referenced by Native.delConstructorList().
|
staticprotected |
Referenced by Native.delContext().
|
staticprotected |
Referenced by Native.disableTrace().
|
staticprotected |
Referenced by Native.enableTrace().
|
staticprotected |
Referenced by Native.evalSmtlib2String().
|
staticprotected |
Referenced by Native.finalizeMemory().
|
staticprotected |
Referenced by Native.fixedpointAddCover().
|
staticprotected |
Referenced by Native.fixedpointAddFact().
|
staticprotected |
Referenced by Native.fixedpointAddInvariant().
|
staticprotected |
Referenced by Native.fixedpointAddRule().
|
staticprotected |
Referenced by Native.fixedpointAssert().
|
staticprotected |
Referenced by Native.fixedpointDecRef().
|
staticprotected |
Referenced by Native.fixedpointFromFile().
|
staticprotected |
Referenced by Native.fixedpointFromString().
|
staticprotected |
Referenced by Native.fixedpointGetAnswer().
|
staticprotected |
Referenced by Native.fixedpointGetAssertions().
|
staticprotected |
Referenced by Native.fixedpointGetCoverDelta().
|
staticprotected |
Referenced by Native.fixedpointGetGroundSatAnswer().
|
staticprotected |
Referenced by Native.fixedpointGetHelp().
|
staticprotected |
Referenced by Native.fixedpointGetNumLevels().
|
staticprotected |
Referenced by Native.fixedpointGetParamDescrs().
|
staticprotected |
Referenced by Native.fixedpointGetReachable().
|
staticprotected |
Referenced by Native.fixedpointGetReasonUnknown().
|
staticprotected |
Referenced by Native.fixedpointGetRuleNamesAlongTrace().
|
staticprotected |
Referenced by Native.fixedpointGetRules().
|
staticprotected |
Referenced by Native.fixedpointGetRulesAlongTrace().
|
staticprotected |
Referenced by Native.fixedpointGetStatistics().
|
staticprotected |
Referenced by Native.fixedpointIncRef().
|
staticprotected |
Referenced by Native.fixedpointQuery().
|
staticprotected |
Referenced by Native.fixedpointQueryFromLvl().
|
staticprotected |
Referenced by Native.fixedpointQueryRelations().
|
staticprotected |
Referenced by Native.fixedpointRegisterRelation().
|
staticprotected |
Referenced by Native.fixedpointSetParams().
|
staticprotected |
Referenced by Native.fixedpointSetPredicateRepresentation().
|
staticprotected |
Referenced by Native.fixedpointToString().
|
staticprotected |
Referenced by Native.fixedpointUpdateRule().
|
staticprotected |
Referenced by Native.fpaGetEbits().
|
staticprotected |
Referenced by Native.fpaGetNumeralExponentBv().
|
staticprotected |
Referenced by Native.fpaGetNumeralExponentInt64().
|
staticprotected |
Referenced by Native.fpaGetNumeralExponentString().
|
staticprotected |
Referenced by Native.fpaGetNumeralSign().
|
staticprotected |
Referenced by Native.fpaGetNumeralSignBv().
|
staticprotected |
Referenced by Native.fpaGetNumeralSignificandBv().
|
staticprotected |
Referenced by Native.fpaGetNumeralSignificandString().
|
staticprotected |
Referenced by Native.fpaGetNumeralSignificandUint64().
|
staticprotected |
Referenced by Native.fpaGetSbits().
|
staticprotected |
Referenced by Native.fpaIsNumeralInf().
|
staticprotected |
Referenced by Native.fpaIsNumeralNan().
|
staticprotected |
Referenced by Native.fpaIsNumeralNegative().
|
staticprotected |
Referenced by Native.fpaIsNumeralNormal().
|
staticprotected |
Referenced by Native.fpaIsNumeralPositive().
|
staticprotected |
Referenced by Native.fpaIsNumeralSubnormal().
|
staticprotected |
Referenced by Native.fpaIsNumeralZero().
|
staticprotected |
Referenced by Native.funcDeclToAst().
|
staticprotected |
Referenced by Native.funcDeclToString().
|
staticprotected |
Referenced by Native.funcEntryDecRef().
|
staticprotected |
Referenced by Native.funcEntryGetArg().
|
staticprotected |
Referenced by Native.funcEntryGetNumArgs().
|
staticprotected |
Referenced by Native.funcEntryGetValue().
|
staticprotected |
Referenced by Native.funcEntryIncRef().
|
staticprotected |
Referenced by Native.funcInterpAddEntry().
|
staticprotected |
Referenced by Native.funcInterpDecRef().
|
staticprotected |
Referenced by Native.funcInterpGetArity().
|
staticprotected |
Referenced by Native.funcInterpGetElse().
|
staticprotected |
Referenced by Native.funcInterpGetEntry().
|
staticprotected |
Referenced by Native.funcInterpGetNumEntries().
|
staticprotected |
Referenced by Native.funcInterpIncRef().
|
staticprotected |
Referenced by Native.funcInterpSetElse().
|
staticprotected |
Referenced by Native.getAlgebraicNumberLower().
|
staticprotected |
Referenced by Native.getAlgebraicNumberUpper().
|
staticprotected |
Referenced by Native.getAppArg().
|
staticprotected |
Referenced by Native.getAppDecl().
|
staticprotected |
Referenced by Native.getAppNumArgs().
|
staticprotected |
Referenced by Native.getArity().
|
staticprotected |
Referenced by Native.getArraySortDomain().
|
staticprotected |
Referenced by Native.getArraySortRange().
|
staticprotected |
Referenced by Native.getAsArrayFuncDecl().
|
staticprotected |
Referenced by Native.getAstHash().
|
staticprotected |
Referenced by Native.getAstId().
|
staticprotected |
Referenced by Native.getAstKind().
|
staticprotected |
Referenced by Native.getBoolValue().
|
staticprotected |
Referenced by Native.getBvSortSize().
|
staticprotected |
Referenced by Native.getDatatypeSortConstructor().
|
staticprotected |
Referenced by Native.getDatatypeSortConstructorAccessor().
|
staticprotected |
Referenced by Native.getDatatypeSortNumConstructors().
|
staticprotected |
Referenced by Native.getDatatypeSortRecognizer().
|
staticprotected |
Referenced by Native.getDeclAstParameter().
|
staticprotected |
Referenced by Native.getDeclDoubleParameter().
|
staticprotected |
Referenced by Native.getDeclFuncDeclParameter().
|
staticprotected |
Referenced by Native.getDeclIntParameter().
|
staticprotected |
Referenced by Native.getDeclKind().
|
staticprotected |
Referenced by Native.getDeclName().
|
staticprotected |
Referenced by Native.getDeclNumParameters().
|
staticprotected |
Referenced by Native.getDeclParameterKind().
|
staticprotected |
Referenced by Native.getDeclRationalParameter().
|
staticprotected |
Referenced by Native.getDeclSortParameter().
|
staticprotected |
Referenced by Native.getDeclSymbolParameter().
|
staticprotected |
Referenced by Native.getDenominator().
|
staticprotected |
Referenced by Native.getDomain().
|
staticprotected |
Referenced by Native.getDomainSize().
|
staticprotected |
Referenced by Native.addConstInterp(), Native.addFuncInterp(), Native.addRecDef(), Native.algebraicAdd(), Native.algebraicDiv(), Native.algebraicEq(), Native.algebraicEval(), Native.algebraicGe(), Native.algebraicGetI(), Native.algebraicGetPoly(), Native.algebraicGt(), Native.algebraicIsNeg(), Native.algebraicIsPos(), Native.algebraicIsValue(), Native.algebraicIsZero(), Native.algebraicLe(), Native.algebraicLt(), Native.algebraicMul(), Native.algebraicNeq(), Native.algebraicPower(), Native.algebraicRoot(), Native.algebraicRoots(), Native.algebraicSign(), Native.algebraicSub(), Native.applyResultDecRef(), Native.applyResultGetNumSubgoals(), Native.applyResultGetSubgoal(), Native.applyResultIncRef(), Native.applyResultToString(), Native.appToAst(), Native.astMapContains(), Native.astMapDecRef(), Native.astMapErase(), Native.astMapFind(), Native.astMapIncRef(), Native.astMapInsert(), Native.astMapKeys(), Native.astMapReset(), Native.astMapSize(), Native.astMapToString(), Native.astToString(), Native.astVectorDecRef(), Native.astVectorGet(), Native.astVectorIncRef(), Native.astVectorPush(), Native.astVectorResize(), Native.astVectorSet(), Native.astVectorSize(), Native.astVectorToString(), Native.astVectorTranslate(), Native.benchmarkToSmtlibString(), Native.datatypeUpdateField(), Native.decRef(), Native.delConstructor(), Native.delConstructorList(), Native.evalSmtlib2String(), Native.fixedpointAddCover(), Native.fixedpointAddFact(), Native.fixedpointAddInvariant(), Native.fixedpointAddRule(), Native.fixedpointAssert(), Native.fixedpointDecRef(), Native.fixedpointFromFile(), Native.fixedpointFromString(), Native.fixedpointGetAnswer(), Native.fixedpointGetAssertions(), Native.fixedpointGetCoverDelta(), Native.fixedpointGetGroundSatAnswer(), Native.fixedpointGetHelp(), Native.fixedpointGetNumLevels(), Native.fixedpointGetParamDescrs(), Native.fixedpointGetReachable(), Native.fixedpointGetReasonUnknown(), Native.fixedpointGetRuleNamesAlongTrace(), Native.fixedpointGetRules(), Native.fixedpointGetRulesAlongTrace(), Native.fixedpointGetStatistics(), Native.fixedpointIncRef(), Native.fixedpointQuery(), Native.fixedpointQueryFromLvl(), Native.fixedpointQueryRelations(), Native.fixedpointRegisterRelation(), Native.fixedpointSetParams(), Native.fixedpointSetPredicateRepresentation(), Native.fixedpointToString(), Native.fixedpointUpdateRule(), Native.fpaGetEbits(), Native.fpaGetNumeralExponentBv(), Native.fpaGetNumeralExponentInt64(), Native.fpaGetNumeralExponentString(), Native.fpaGetNumeralSign(), Native.fpaGetNumeralSignBv(), Native.fpaGetNumeralSignificandBv(), Native.fpaGetNumeralSignificandString(), Native.fpaGetNumeralSignificandUint64(), Native.fpaGetSbits(), Native.fpaIsNumeralInf(), Native.fpaIsNumeralNan(), Native.fpaIsNumeralNegative(), Native.fpaIsNumeralNormal(), Native.fpaIsNumeralPositive(), Native.fpaIsNumeralSubnormal(), Native.fpaIsNumeralZero(), Native.funcDeclToAst(), Native.funcDeclToString(), Native.funcEntryDecRef(), Native.funcEntryGetArg(), Native.funcEntryGetNumArgs(), Native.funcEntryGetValue(), Native.funcEntryIncRef(), Native.funcInterpAddEntry(), Native.funcInterpDecRef(), Native.funcInterpGetArity(), Native.funcInterpGetElse(), Native.funcInterpGetEntry(), Native.funcInterpGetNumEntries(), Native.funcInterpIncRef(), Native.funcInterpSetElse(), Native.getAlgebraicNumberLower(), Native.getAlgebraicNumberUpper(), Native.getAppArg(), Native.getAppDecl(), Native.getAppNumArgs(), Native.getArity(), Native.getArraySortDomain(), Native.getArraySortRange(), Native.getAsArrayFuncDecl(), Native.getAstHash(), Native.getAstId(), Native.getAstKind(), Native.getBoolValue(), Native.getBvSortSize(), Native.getDatatypeSortConstructor(), Native.getDatatypeSortConstructorAccessor(), Native.getDatatypeSortNumConstructors(), Native.getDatatypeSortRecognizer(), Native.getDeclAstParameter(), Native.getDeclDoubleParameter(), Native.getDeclFuncDeclParameter(), Native.getDeclIntParameter(), Native.getDeclKind(), Native.getDeclName(), Native.getDeclNumParameters(), Native.getDeclParameterKind(), Native.getDeclRationalParameter(), Native.getDeclSortParameter(), Native.getDeclSymbolParameter(), Native.getDenominator(), Native.getDomain(), Native.getDomainSize(), Native.getErrorCode(), Native.getErrorMsg(), Native.getFiniteDomainSortSize(), Native.getFuncDeclId(), Native.getImpliedEqualities(), Native.getIndexValue(), Native.getLstring(), Native.getNumeralDecimalString(), Native.getNumeralDouble(), Native.getNumeralInt(), Native.getNumeralInt64(), Native.getNumeralRationalInt64(), Native.getNumeralSmall(), Native.getNumeralString(), Native.getNumeralUint(), Native.getNumeralUint64(), Native.getNumerator(), Native.getNumProbes(), Native.getNumTactics(), Native.getPattern(), Native.getPatternNumTerms(), Native.getProbeName(), Native.getQuantifierBody(), Native.getQuantifierBoundName(), Native.getQuantifierBoundSort(), Native.getQuantifierNoPatternAst(), Native.getQuantifierNumBound(), Native.getQuantifierNumNoPatterns(), Native.getQuantifierNumPatterns(), Native.getQuantifierPatternAst(), Native.getQuantifierWeight(), Native.getRange(), Native.getRelationArity(), Native.getRelationColumn(), Native.getReSortBasis(), Native.getSeqSortBasis(), Native.getSort(), Native.getSortId(), Native.getSortKind(), Native.getSortName(), Native.getString(), Native.getSymbolInt(), Native.getSymbolKind(), Native.getSymbolString(), Native.getTacticName(), Native.getTupleSortFieldDecl(), Native.getTupleSortMkDecl(), Native.getTupleSortNumFields(), Native.goalAssert(), Native.goalConvertModel(), Native.goalDecRef(), Native.goalDepth(), Native.goalFormula(), Native.goalInconsistent(), Native.goalIncRef(), Native.goalIsDecidedSat(), Native.goalIsDecidedUnsat(), Native.goalNumExprs(), Native.goalPrecision(), Native.goalReset(), Native.goalSize(), Native.goalToDimacsString(), Native.goalToString(), Native.goalTranslate(), Native.incRef(), Native.interrupt(), Native.isAlgebraicNumber(), Native.isApp(), Native.isAsArray(), Native.isEqAst(), Native.isEqFuncDecl(), Native.isEqSort(), Native.isLambda(), Native.isNumeralAst(), Native.isQuantifierExists(), Native.isQuantifierForall(), Native.isReSort(), Native.isSeqSort(), Native.isString(), Native.isStringSort(), Native.isWellSorted(), Native.mkAdd(), Native.mkAnd(), Native.mkApp(), Native.mkArrayDefault(), Native.mkArrayExt(), Native.mkArraySort(), Native.mkArraySortN(), Native.mkAsArray(), Native.mkAstMap(), Native.mkAstVector(), Native.mkAtleast(), Native.mkAtmost(), Native.mkBoolSort(), Native.mkBound(), Native.mkBv2int(), Native.mkBvadd(), Native.mkBvaddNoOverflow(), Native.mkBvaddNoUnderflow(), Native.mkBvand(), Native.mkBvashr(), Native.mkBvlshr(), Native.mkBvmul(), Native.mkBvmulNoOverflow(), Native.mkBvmulNoUnderflow(), Native.mkBvnand(), Native.mkBvneg(), Native.mkBvnegNoOverflow(), Native.mkBvnor(), Native.mkBvnot(), Native.mkBvNumeral(), Native.mkBvor(), Native.mkBvredand(), Native.mkBvredor(), Native.mkBvsdiv(), Native.mkBvsdivNoOverflow(), Native.mkBvsge(), Native.mkBvsgt(), Native.mkBvshl(), Native.mkBvsle(), Native.mkBvslt(), Native.mkBvsmod(), Native.mkBvSort(), Native.mkBvsrem(), Native.mkBvsub(), Native.mkBvsubNoOverflow(), Native.mkBvsubNoUnderflow(), Native.mkBvudiv(), Native.mkBvuge(), Native.mkBvugt(), Native.mkBvule(), Native.mkBvult(), Native.mkBvurem(), Native.mkBvxnor(), Native.mkBvxor(), Native.mkConcat(), Native.mkConst(), Native.mkConstArray(), Native.mkConstructor(), Native.mkConstructorList(), Native.mkDatatype(), Native.mkDatatypes(), Native.mkDistinct(), Native.mkDiv(), Native.mkDivides(), Native.mkEmptySet(), Native.mkEnumerationSort(), Native.mkEq(), Native.mkExists(), Native.mkExistsConst(), Native.mkExtract(), Native.mkExtRotateLeft(), Native.mkExtRotateRight(), Native.mkFalse(), Native.mkFiniteDomainSort(), Native.mkFixedpoint(), Native.mkForall(), Native.mkForallConst(), Native.mkFpaAbs(), Native.mkFpaAdd(), Native.mkFpaDiv(), Native.mkFpaEq(), Native.mkFpaFma(), Native.mkFpaFp(), Native.mkFpaGeq(), Native.mkFpaGt(), Native.mkFpaInf(), Native.mkFpaIsInfinite(), Native.mkFpaIsNan(), Native.mkFpaIsNegative(), Native.mkFpaIsNormal(), Native.mkFpaIsPositive(), Native.mkFpaIsSubnormal(), Native.mkFpaIsZero(), Native.mkFpaLeq(), Native.mkFpaLt(), Native.mkFpaMax(), Native.mkFpaMin(), Native.mkFpaMul(), Native.mkFpaNan(), Native.mkFpaNeg(), Native.mkFpaNumeralDouble(), Native.mkFpaNumeralFloat(), Native.mkFpaNumeralInt(), Native.mkFpaNumeralInt64Uint64(), Native.mkFpaNumeralIntUint(), Native.mkFpaRem(), Native.mkFpaRna(), Native.mkFpaRne(), Native.mkFpaRoundingModeSort(), Native.mkFpaRoundNearestTiesToAway(), Native.mkFpaRoundNearestTiesToEven(), Native.mkFpaRoundToIntegral(), Native.mkFpaRoundTowardNegative(), Native.mkFpaRoundTowardPositive(), Native.mkFpaRoundTowardZero(), Native.mkFpaRtn(), Native.mkFpaRtp(), Native.mkFpaRtz(), Native.mkFpaSort(), Native.mkFpaSort128(), Native.mkFpaSort16(), Native.mkFpaSort32(), Native.mkFpaSort64(), Native.mkFpaSortDouble(), Native.mkFpaSortHalf(), Native.mkFpaSortQuadruple(), Native.mkFpaSortSingle(), Native.mkFpaSqrt(), Native.mkFpaSub(), Native.mkFpaToFpBv(), Native.mkFpaToFpFloat(), Native.mkFpaToFpIntReal(), Native.mkFpaToFpReal(), Native.mkFpaToFpSigned(), Native.mkFpaToFpUnsigned(), Native.mkFpaToIeeeBv(), Native.mkFpaToReal(), Native.mkFpaToSbv(), Native.mkFpaToUbv(), Native.mkFpaZero(), Native.mkFreshConst(), Native.mkFreshFuncDecl(), Native.mkFullSet(), Native.mkFuncDecl(), Native.mkGe(), Native.mkGoal(), Native.mkGt(), Native.mkIff(), Native.mkImplies(), Native.mkInt(), Native.mkInt2bv(), Native.mkInt2real(), Native.mkInt64(), Native.mkIntSort(), Native.mkIntSymbol(), Native.mkIntToStr(), Native.mkIsInt(), Native.mkIte(), Native.mkLambda(), Native.mkLambdaConst(), Native.mkLe(), Native.mkLinearOrder(), Native.mkListSort(), Native.mkLstring(), Native.mkLt(), Native.mkMap(), Native.mkMod(), Native.mkModel(), Native.mkMul(), Native.mkNot(), Native.mkNumeral(), Native.mkOptimize(), Native.mkOr(), Native.mkParams(), Native.mkPartialOrder(), Native.mkPattern(), Native.mkPbeq(), Native.mkPbge(), Native.mkPble(), Native.mkPiecewiseLinearOrder(), Native.mkPower(), Native.mkProbe(), Native.mkQuantifier(), Native.mkQuantifierConst(), Native.mkQuantifierConstEx(), Native.mkQuantifierEx(), Native.mkReal(), Native.mkReal2int(), Native.mkRealSort(), Native.mkRecFuncDecl(), Native.mkReComplement(), Native.mkReConcat(), Native.mkReEmpty(), Native.mkReFull(), Native.mkReIntersect(), Native.mkReLoop(), Native.mkRem(), Native.mkReOption(), Native.mkRepeat(), Native.mkRePlus(), Native.mkReRange(), Native.mkReSort(), Native.mkReStar(), Native.mkReUnion(), Native.mkRotateLeft(), Native.mkRotateRight(), Native.mkSelect(), Native.mkSelectN(), Native.mkSeqAt(), Native.mkSeqConcat(), Native.mkSeqContains(), Native.mkSeqEmpty(), Native.mkSeqExtract(), Native.mkSeqIndex(), Native.mkSeqInRe(), Native.mkSeqLastIndex(), Native.mkSeqLength(), Native.mkSeqNth(), Native.mkSeqPrefix(), Native.mkSeqReplace(), Native.mkSeqSort(), Native.mkSeqSuffix(), Native.mkSeqToRe(), Native.mkSeqUnit(), Native.mkSetAdd(), Native.mkSetComplement(), Native.mkSetDel(), Native.mkSetDifference(), Native.mkSetHasSize(), Native.mkSetIntersect(), Native.mkSetMember(), Native.mkSetSort(), Native.mkSetSubset(), Native.mkSetUnion(), Native.mkSignExt(), Native.mkSimpleSolver(), Native.mkSolver(), Native.mkSolverForLogic(), Native.mkSolverFromTactic(), Native.mkStore(), Native.mkStoreN(), Native.mkString(), Native.mkStringSort(), Native.mkStringSymbol(), Native.mkStrLe(), Native.mkStrLt(), Native.mkStrToInt(), Native.mkSub(), Native.mkTactic(), Native.mkTransitiveClosure(), Native.mkTreeOrder(), Native.mkTrue(), Native.mkTupleSort(), Native.mkUnaryMinus(), Native.mkUninterpretedSort(), Native.mkUnsignedInt(), Native.mkUnsignedInt64(), Native.mkXor(), Native.mkZeroExt(), Native.modelDecRef(), Native.modelEval(), Native.modelExtrapolate(), Native.modelGetConstDecl(), Native.modelGetConstInterp(), Native.modelGetFuncDecl(), Native.modelGetFuncInterp(), Native.modelGetNumConsts(), Native.modelGetNumFuncs(), Native.modelGetNumSorts(), Native.modelGetSort(), Native.modelGetSortUniverse(), Native.modelHasInterp(), Native.modelIncRef(), Native.modelToString(), Native.modelTranslate(), Native.optimizeAssert(), Native.optimizeAssertAndTrack(), Native.optimizeAssertSoft(), Native.optimizeCheck(), Native.optimizeDecRef(), Native.optimizeFromFile(), Native.optimizeFromString(), Native.optimizeGetAssertions(), Native.optimizeGetHelp(), Native.optimizeGetLower(), Native.optimizeGetLowerAsVector(), Native.optimizeGetModel(), Native.optimizeGetObjectives(), Native.optimizeGetParamDescrs(), Native.optimizeGetReasonUnknown(), Native.optimizeGetStatistics(), Native.optimizeGetUnsatCore(), Native.optimizeGetUpper(), Native.optimizeGetUpperAsVector(), Native.optimizeIncRef(), Native.optimizeMaximize(), Native.optimizeMinimize(), Native.optimizePop(), Native.optimizePush(), Native.optimizeSetParams(), Native.optimizeToString(), Native.paramDescrsDecRef(), Native.paramDescrsGetDocumentation(), Native.paramDescrsGetKind(), Native.paramDescrsGetName(), Native.paramDescrsIncRef(), Native.paramDescrsSize(), Native.paramDescrsToString(), Native.paramsDecRef(), Native.paramsIncRef(), Native.paramsSetBool(), Native.paramsSetDouble(), Native.paramsSetSymbol(), Native.paramsSetUint(), Native.paramsToString(), Native.paramsValidate(), Native.parseSmtlib2File(), Native.parseSmtlib2String(), Native.patternToAst(), Native.patternToString(), Native.polynomialSubresultants(), Native.probeAnd(), Native.probeApply(), Native.probeConst(), Native.probeDecRef(), Native.probeEq(), Native.probeGe(), Native.probeGetDescr(), Native.probeGt(), Native.probeIncRef(), Native.probeLe(), Native.probeLt(), Native.probeNot(), Native.probeOr(), Native.qeLite(), Native.qeModelProject(), Native.qeModelProjectSkolem(), Native.queryConstructor(), Native.rcfAdd(), Native.rcfDel(), Native.rcfDiv(), Native.rcfEq(), Native.rcfGe(), Native.rcfGetNumeratorDenominator(), Native.rcfGt(), Native.rcfInv(), Native.rcfLe(), Native.rcfLt(), Native.rcfMkE(), Native.rcfMkInfinitesimal(), Native.rcfMkPi(), Native.rcfMkRational(), Native.rcfMkRoots(), Native.rcfMkSmallInt(), Native.rcfMul(), Native.rcfNeg(), Native.rcfNeq(), Native.rcfNumToDecimalString(), Native.rcfNumToString(), Native.rcfPower(), Native.rcfSub(), Native.setAstPrintMode(), Native.setError(), Native.simplify(), Native.simplifyEx(), Native.simplifyGetHelp(), Native.simplifyGetParamDescrs(), Native.solverAssert(), Native.solverAssertAndTrack(), Native.solverCheck(), Native.solverCheckAssumptions(), Native.solverCube(), Native.solverDecRef(), Native.solverFromFile(), Native.solverFromString(), Native.solverGetAssertions(), Native.solverGetConsequences(), Native.solverGetHelp(), Native.solverGetLevels(), Native.solverGetModel(), Native.solverGetNonUnits(), Native.solverGetNumScopes(), Native.solverGetParamDescrs(), Native.solverGetProof(), Native.solverGetReasonUnknown(), Native.solverGetStatistics(), Native.solverGetTrail(), Native.solverGetUnits(), Native.solverGetUnsatCore(), Native.solverImportModelConverter(), Native.solverIncRef(), Native.solverInterrupt(), Native.solverPop(), Native.solverPush(), Native.solverReset(), Native.solverSetParams(), Native.solverToDimacsString(), Native.solverToString(), Native.solverTranslate(), Native.sortToAst(), Native.sortToString(), Native.statsDecRef(), Native.statsGetDoubleValue(), Native.statsGetKey(), Native.statsGetUintValue(), Native.statsIncRef(), Native.statsIsDouble(), Native.statsIsUint(), Native.statsSize(), Native.statsToString(), Native.substitute(), Native.substituteVars(), Native.tacticAndThen(), Native.tacticApply(), Native.tacticApplyEx(), Native.tacticCond(), Native.tacticDecRef(), Native.tacticFail(), Native.tacticFailIf(), Native.tacticFailIfNotDecided(), Native.tacticGetDescr(), Native.tacticGetHelp(), Native.tacticGetParamDescrs(), Native.tacticIncRef(), Native.tacticOrElse(), Native.tacticParAndThen(), Native.tacticParOr(), Native.tacticRepeat(), Native.tacticSkip(), Native.tacticTryFor(), Native.tacticUsingParams(), Native.tacticWhen(), Native.toApp(), Native.toFuncDecl(), Native.translate(), Native.updateParamValue(), and Native.updateTerm().
|
staticprotected |
Referenced by Native.addConstInterp(), Native.addFuncInterp(), Native.addRecDef(), Native.algebraicAdd(), Native.algebraicDiv(), Native.algebraicEq(), Native.algebraicEval(), Native.algebraicGe(), Native.algebraicGetI(), Native.algebraicGetPoly(), Native.algebraicGt(), Native.algebraicIsNeg(), Native.algebraicIsPos(), Native.algebraicIsValue(), Native.algebraicIsZero(), Native.algebraicLe(), Native.algebraicLt(), Native.algebraicMul(), Native.algebraicNeq(), Native.algebraicPower(), Native.algebraicRoot(), Native.algebraicRoots(), Native.algebraicSign(), Native.algebraicSub(), Native.applyResultDecRef(), Native.applyResultGetNumSubgoals(), Native.applyResultGetSubgoal(), Native.applyResultIncRef(), Native.applyResultToString(), Native.appToAst(), Native.astMapContains(), Native.astMapDecRef(), Native.astMapErase(), Native.astMapFind(), Native.astMapIncRef(), Native.astMapInsert(), Native.astMapKeys(), Native.astMapReset(), Native.astMapSize(), Native.astMapToString(), Native.astToString(), Native.astVectorDecRef(), Native.astVectorGet(), Native.astVectorIncRef(), Native.astVectorPush(), Native.astVectorResize(), Native.astVectorSet(), Native.astVectorSize(), Native.astVectorToString(), Native.astVectorTranslate(), Native.benchmarkToSmtlibString(), Native.datatypeUpdateField(), Native.decRef(), Native.delConstructor(), Native.delConstructorList(), Native.evalSmtlib2String(), Native.fixedpointAddCover(), Native.fixedpointAddFact(), Native.fixedpointAddInvariant(), Native.fixedpointAddRule(), Native.fixedpointAssert(), Native.fixedpointDecRef(), Native.fixedpointFromFile(), Native.fixedpointFromString(), Native.fixedpointGetAnswer(), Native.fixedpointGetAssertions(), Native.fixedpointGetCoverDelta(), Native.fixedpointGetGroundSatAnswer(), Native.fixedpointGetHelp(), Native.fixedpointGetNumLevels(), Native.fixedpointGetParamDescrs(), Native.fixedpointGetReachable(), Native.fixedpointGetReasonUnknown(), Native.fixedpointGetRuleNamesAlongTrace(), Native.fixedpointGetRules(), Native.fixedpointGetRulesAlongTrace(), Native.fixedpointGetStatistics(), Native.fixedpointIncRef(), Native.fixedpointQuery(), Native.fixedpointQueryFromLvl(), Native.fixedpointQueryRelations(), Native.fixedpointRegisterRelation(), Native.fixedpointSetParams(), Native.fixedpointSetPredicateRepresentation(), Native.fixedpointToString(), Native.fixedpointUpdateRule(), Native.fpaGetEbits(), Native.fpaGetNumeralExponentBv(), Native.fpaGetNumeralExponentInt64(), Native.fpaGetNumeralExponentString(), Native.fpaGetNumeralSign(), Native.fpaGetNumeralSignBv(), Native.fpaGetNumeralSignificandBv(), Native.fpaGetNumeralSignificandString(), Native.fpaGetNumeralSignificandUint64(), Native.fpaGetSbits(), Native.fpaIsNumeralInf(), Native.fpaIsNumeralNan(), Native.fpaIsNumeralNegative(), Native.fpaIsNumeralNormal(), Native.fpaIsNumeralPositive(), Native.fpaIsNumeralSubnormal(), Native.fpaIsNumeralZero(), Native.funcDeclToAst(), Native.funcDeclToString(), Native.funcEntryDecRef(), Native.funcEntryGetArg(), Native.funcEntryGetNumArgs(), Native.funcEntryGetValue(), Native.funcEntryIncRef(), Native.funcInterpAddEntry(), Native.funcInterpDecRef(), Native.funcInterpGetArity(), Native.funcInterpGetElse(), Native.funcInterpGetEntry(), Native.funcInterpGetNumEntries(), Native.funcInterpIncRef(), Native.funcInterpSetElse(), Native.getAlgebraicNumberLower(), Native.getAlgebraicNumberUpper(), Native.getAppArg(), Native.getAppDecl(), Native.getAppNumArgs(), Native.getArity(), Native.getArraySortDomain(), Native.getArraySortRange(), Native.getAsArrayFuncDecl(), Native.getAstHash(), Native.getAstId(), Native.getAstKind(), Native.getBoolValue(), Native.getBvSortSize(), Native.getDatatypeSortConstructor(), Native.getDatatypeSortConstructorAccessor(), Native.getDatatypeSortNumConstructors(), Native.getDatatypeSortRecognizer(), Native.getDeclAstParameter(), Native.getDeclDoubleParameter(), Native.getDeclFuncDeclParameter(), Native.getDeclIntParameter(), Native.getDeclKind(), Native.getDeclName(), Native.getDeclNumParameters(), Native.getDeclParameterKind(), Native.getDeclRationalParameter(), Native.getDeclSortParameter(), Native.getDeclSymbolParameter(), Native.getDenominator(), Native.getDomain(), Native.getDomainSize(), Native.getErrorMsg(), Native.getFiniteDomainSortSize(), Native.getFuncDeclId(), Native.getImpliedEqualities(), Native.getIndexValue(), Native.getLstring(), Native.getNumeralDecimalString(), Native.getNumeralDouble(), Native.getNumeralInt(), Native.getNumeralInt64(), Native.getNumeralRationalInt64(), Native.getNumeralSmall(), Native.getNumeralString(), Native.getNumeralUint(), Native.getNumeralUint64(), Native.getNumerator(), Native.getNumProbes(), Native.getNumTactics(), Native.getPattern(), Native.getPatternNumTerms(), Native.getProbeName(), Native.getQuantifierBody(), Native.getQuantifierBoundName(), Native.getQuantifierBoundSort(), Native.getQuantifierNoPatternAst(), Native.getQuantifierNumBound(), Native.getQuantifierNumNoPatterns(), Native.getQuantifierNumPatterns(), Native.getQuantifierPatternAst(), Native.getQuantifierWeight(), Native.getRange(), Native.getRelationArity(), Native.getRelationColumn(), Native.getReSortBasis(), Native.getSeqSortBasis(), Native.getSort(), Native.getSortId(), Native.getSortKind(), Native.getSortName(), Native.getString(), Native.getSymbolInt(), Native.getSymbolKind(), Native.getSymbolString(), Native.getTacticName(), Native.getTupleSortFieldDecl(), Native.getTupleSortMkDecl(), Native.getTupleSortNumFields(), Native.goalAssert(), Native.goalConvertModel(), Native.goalDecRef(), Native.goalDepth(), Native.goalFormula(), Native.goalInconsistent(), Native.goalIncRef(), Native.goalIsDecidedSat(), Native.goalIsDecidedUnsat(), Native.goalNumExprs(), Native.goalPrecision(), Native.goalReset(), Native.goalSize(), Native.goalToDimacsString(), Native.goalToString(), Native.goalTranslate(), Native.incRef(), Native.interrupt(), Native.isAlgebraicNumber(), Native.isApp(), Native.isAsArray(), Native.isEqAst(), Native.isEqFuncDecl(), Native.isEqSort(), Native.isLambda(), Native.isNumeralAst(), Native.isQuantifierExists(), Native.isQuantifierForall(), Native.isReSort(), Native.isSeqSort(), Native.isString(), Native.isStringSort(), Native.isWellSorted(), Native.mkAdd(), Native.mkAnd(), Native.mkApp(), Native.mkArrayDefault(), Native.mkArrayExt(), Native.mkArraySort(), Native.mkArraySortN(), Native.mkAsArray(), Native.mkAstMap(), Native.mkAstVector(), Native.mkAtleast(), Native.mkAtmost(), Native.mkBoolSort(), Native.mkBound(), Native.mkBv2int(), Native.mkBvadd(), Native.mkBvaddNoOverflow(), Native.mkBvaddNoUnderflow(), Native.mkBvand(), Native.mkBvashr(), Native.mkBvlshr(), Native.mkBvmul(), Native.mkBvmulNoOverflow(), Native.mkBvmulNoUnderflow(), Native.mkBvnand(), Native.mkBvneg(), Native.mkBvnegNoOverflow(), Native.mkBvnor(), Native.mkBvnot(), Native.mkBvNumeral(), Native.mkBvor(), Native.mkBvredand(), Native.mkBvredor(), Native.mkBvsdiv(), Native.mkBvsdivNoOverflow(), Native.mkBvsge(), Native.mkBvsgt(), Native.mkBvshl(), Native.mkBvsle(), Native.mkBvslt(), Native.mkBvsmod(), Native.mkBvSort(), Native.mkBvsrem(), Native.mkBvsub(), Native.mkBvsubNoOverflow(), Native.mkBvsubNoUnderflow(), Native.mkBvudiv(), Native.mkBvuge(), Native.mkBvugt(), Native.mkBvule(), Native.mkBvult(), Native.mkBvurem(), Native.mkBvxnor(), Native.mkBvxor(), Native.mkConcat(), Native.mkConst(), Native.mkConstArray(), Native.mkConstructor(), Native.mkConstructorList(), Native.mkDatatype(), Native.mkDatatypes(), Native.mkDistinct(), Native.mkDiv(), Native.mkDivides(), Native.mkEmptySet(), Native.mkEnumerationSort(), Native.mkEq(), Native.mkExists(), Native.mkExistsConst(), Native.mkExtract(), Native.mkExtRotateLeft(), Native.mkExtRotateRight(), Native.mkFalse(), Native.mkFiniteDomainSort(), Native.mkFixedpoint(), Native.mkForall(), Native.mkForallConst(), Native.mkFpaAbs(), Native.mkFpaAdd(), Native.mkFpaDiv(), Native.mkFpaEq(), Native.mkFpaFma(), Native.mkFpaFp(), Native.mkFpaGeq(), Native.mkFpaGt(), Native.mkFpaInf(), Native.mkFpaIsInfinite(), Native.mkFpaIsNan(), Native.mkFpaIsNegative(), Native.mkFpaIsNormal(), Native.mkFpaIsPositive(), Native.mkFpaIsSubnormal(), Native.mkFpaIsZero(), Native.mkFpaLeq(), Native.mkFpaLt(), Native.mkFpaMax(), Native.mkFpaMin(), Native.mkFpaMul(), Native.mkFpaNan(), Native.mkFpaNeg(), Native.mkFpaNumeralDouble(), Native.mkFpaNumeralFloat(), Native.mkFpaNumeralInt(), Native.mkFpaNumeralInt64Uint64(), Native.mkFpaNumeralIntUint(), Native.mkFpaRem(), Native.mkFpaRna(), Native.mkFpaRne(), Native.mkFpaRoundingModeSort(), Native.mkFpaRoundNearestTiesToAway(), Native.mkFpaRoundNearestTiesToEven(), Native.mkFpaRoundToIntegral(), Native.mkFpaRoundTowardNegative(), Native.mkFpaRoundTowardPositive(), Native.mkFpaRoundTowardZero(), Native.mkFpaRtn(), Native.mkFpaRtp(), Native.mkFpaRtz(), Native.mkFpaSort(), Native.mkFpaSort128(), Native.mkFpaSort16(), Native.mkFpaSort32(), Native.mkFpaSort64(), Native.mkFpaSortDouble(), Native.mkFpaSortHalf(), Native.mkFpaSortQuadruple(), Native.mkFpaSortSingle(), Native.mkFpaSqrt(), Native.mkFpaSub(), Native.mkFpaToFpBv(), Native.mkFpaToFpFloat(), Native.mkFpaToFpIntReal(), Native.mkFpaToFpReal(), Native.mkFpaToFpSigned(), Native.mkFpaToFpUnsigned(), Native.mkFpaToIeeeBv(), Native.mkFpaToReal(), Native.mkFpaToSbv(), Native.mkFpaToUbv(), Native.mkFpaZero(), Native.mkFreshConst(), Native.mkFreshFuncDecl(), Native.mkFullSet(), Native.mkFuncDecl(), Native.mkGe(), Native.mkGoal(), Native.mkGt(), Native.mkIff(), Native.mkImplies(), Native.mkInt(), Native.mkInt2bv(), Native.mkInt2real(), Native.mkInt64(), Native.mkIntSort(), Native.mkIntSymbol(), Native.mkIntToStr(), Native.mkIsInt(), Native.mkIte(), Native.mkLambda(), Native.mkLambdaConst(), Native.mkLe(), Native.mkLinearOrder(), Native.mkListSort(), Native.mkLstring(), Native.mkLt(), Native.mkMap(), Native.mkMod(), Native.mkModel(), Native.mkMul(), Native.mkNot(), Native.mkNumeral(), Native.mkOptimize(), Native.mkOr(), Native.mkParams(), Native.mkPartialOrder(), Native.mkPattern(), Native.mkPbeq(), Native.mkPbge(), Native.mkPble(), Native.mkPiecewiseLinearOrder(), Native.mkPower(), Native.mkProbe(), Native.mkQuantifier(), Native.mkQuantifierConst(), Native.mkQuantifierConstEx(), Native.mkQuantifierEx(), Native.mkReal(), Native.mkReal2int(), Native.mkRealSort(), Native.mkRecFuncDecl(), Native.mkReComplement(), Native.mkReConcat(), Native.mkReEmpty(), Native.mkReFull(), Native.mkReIntersect(), Native.mkReLoop(), Native.mkRem(), Native.mkReOption(), Native.mkRepeat(), Native.mkRePlus(), Native.mkReRange(), Native.mkReSort(), Native.mkReStar(), Native.mkReUnion(), Native.mkRotateLeft(), Native.mkRotateRight(), Native.mkSelect(), Native.mkSelectN(), Native.mkSeqAt(), Native.mkSeqConcat(), Native.mkSeqContains(), Native.mkSeqEmpty(), Native.mkSeqExtract(), Native.mkSeqIndex(), Native.mkSeqInRe(), Native.mkSeqLastIndex(), Native.mkSeqLength(), Native.mkSeqNth(), Native.mkSeqPrefix(), Native.mkSeqReplace(), Native.mkSeqSort(), Native.mkSeqSuffix(), Native.mkSeqToRe(), Native.mkSeqUnit(), Native.mkSetAdd(), Native.mkSetComplement(), Native.mkSetDel(), Native.mkSetDifference(), Native.mkSetHasSize(), Native.mkSetIntersect(), Native.mkSetMember(), Native.mkSetSort(), Native.mkSetSubset(), Native.mkSetUnion(), Native.mkSignExt(), Native.mkSimpleSolver(), Native.mkSolver(), Native.mkSolverForLogic(), Native.mkSolverFromTactic(), Native.mkStore(), Native.mkStoreN(), Native.mkString(), Native.mkStringSort(), Native.mkStringSymbol(), Native.mkStrLe(), Native.mkStrLt(), Native.mkStrToInt(), Native.mkSub(), Native.mkTactic(), Native.mkTransitiveClosure(), Native.mkTreeOrder(), Native.mkTrue(), Native.mkTupleSort(), Native.mkUnaryMinus(), Native.mkUninterpretedSort(), Native.mkUnsignedInt(), Native.mkUnsignedInt64(), Native.mkXor(), Native.mkZeroExt(), Native.modelDecRef(), Native.modelEval(), Native.modelExtrapolate(), Native.modelGetConstDecl(), Native.modelGetConstInterp(), Native.modelGetFuncDecl(), Native.modelGetFuncInterp(), Native.modelGetNumConsts(), Native.modelGetNumFuncs(), Native.modelGetNumSorts(), Native.modelGetSort(), Native.modelGetSortUniverse(), Native.modelHasInterp(), Native.modelIncRef(), Native.modelToString(), Native.modelTranslate(), Native.optimizeAssert(), Native.optimizeAssertAndTrack(), Native.optimizeAssertSoft(), Native.optimizeCheck(), Native.optimizeDecRef(), Native.optimizeFromFile(), Native.optimizeFromString(), Native.optimizeGetAssertions(), Native.optimizeGetHelp(), Native.optimizeGetLower(), Native.optimizeGetLowerAsVector(), Native.optimizeGetModel(), Native.optimizeGetObjectives(), Native.optimizeGetParamDescrs(), Native.optimizeGetReasonUnknown(), Native.optimizeGetStatistics(), Native.optimizeGetUnsatCore(), Native.optimizeGetUpper(), Native.optimizeGetUpperAsVector(), Native.optimizeIncRef(), Native.optimizeMaximize(), Native.optimizeMinimize(), Native.optimizePop(), Native.optimizePush(), Native.optimizeSetParams(), Native.optimizeToString(), Native.paramDescrsDecRef(), Native.paramDescrsGetDocumentation(), Native.paramDescrsGetKind(), Native.paramDescrsGetName(), Native.paramDescrsIncRef(), Native.paramDescrsSize(), Native.paramDescrsToString(), Native.paramsDecRef(), Native.paramsIncRef(), Native.paramsSetBool(), Native.paramsSetDouble(), Native.paramsSetSymbol(), Native.paramsSetUint(), Native.paramsToString(), Native.paramsValidate(), Native.parseSmtlib2File(), Native.parseSmtlib2String(), Native.patternToAst(), Native.patternToString(), Native.polynomialSubresultants(), Native.probeAnd(), Native.probeApply(), Native.probeConst(), Native.probeDecRef(), Native.probeEq(), Native.probeGe(), Native.probeGetDescr(), Native.probeGt(), Native.probeIncRef(), Native.probeLe(), Native.probeLt(), Native.probeNot(), Native.probeOr(), Native.qeLite(), Native.qeModelProject(), Native.qeModelProjectSkolem(), Native.queryConstructor(), Native.rcfAdd(), Native.rcfDel(), Native.rcfDiv(), Native.rcfEq(), Native.rcfGe(), Native.rcfGetNumeratorDenominator(), Native.rcfGt(), Native.rcfInv(), Native.rcfLe(), Native.rcfLt(), Native.rcfMkE(), Native.rcfMkInfinitesimal(), Native.rcfMkPi(), Native.rcfMkRational(), Native.rcfMkRoots(), Native.rcfMkSmallInt(), Native.rcfMul(), Native.rcfNeg(), Native.rcfNeq(), Native.rcfNumToDecimalString(), Native.rcfNumToString(), Native.rcfPower(), Native.rcfSub(), Native.setAstPrintMode(), Native.setError(), Native.simplify(), Native.simplifyEx(), Native.simplifyGetHelp(), Native.simplifyGetParamDescrs(), Native.solverAssert(), Native.solverAssertAndTrack(), Native.solverCheck(), Native.solverCheckAssumptions(), Native.solverCube(), Native.solverDecRef(), Native.solverFromFile(), Native.solverFromString(), Native.solverGetAssertions(), Native.solverGetConsequences(), Native.solverGetHelp(), Native.solverGetLevels(), Native.solverGetModel(), Native.solverGetNonUnits(), Native.solverGetNumScopes(), Native.solverGetParamDescrs(), Native.solverGetProof(), Native.solverGetReasonUnknown(), Native.solverGetStatistics(), Native.solverGetTrail(), Native.solverGetUnits(), Native.solverGetUnsatCore(), Native.solverImportModelConverter(), Native.solverIncRef(), Native.solverInterrupt(), Native.solverPop(), Native.solverPush(), Native.solverReset(), Native.solverSetParams(), Native.solverToDimacsString(), Native.solverToString(), Native.solverTranslate(), Native.sortToAst(), Native.sortToString(), Native.statsDecRef(), Native.statsGetDoubleValue(), Native.statsGetKey(), Native.statsGetUintValue(), Native.statsIncRef(), Native.statsIsDouble(), Native.statsIsUint(), Native.statsSize(), Native.statsToString(), Native.substitute(), Native.substituteVars(), Native.tacticAndThen(), Native.tacticApply(), Native.tacticApplyEx(), Native.tacticCond(), Native.tacticDecRef(), Native.tacticFail(), Native.tacticFailIf(), Native.tacticFailIfNotDecided(), Native.tacticGetDescr(), Native.tacticGetHelp(), Native.tacticGetParamDescrs(), Native.tacticIncRef(), Native.tacticOrElse(), Native.tacticParAndThen(), Native.tacticParOr(), Native.tacticRepeat(), Native.tacticSkip(), Native.tacticTryFor(), Native.tacticUsingParams(), Native.tacticWhen(), Native.toApp(), Native.toFuncDecl(), Native.translate(), Native.updateParamValue(), and Native.updateTerm().
|
staticprotected |
Referenced by Native.getEstimatedAllocSize().
|
staticprotected |
Referenced by Native.getFiniteDomainSortSize().
|
staticprotected |
Referenced by Native.getFullVersion().
|
staticprotected |
Referenced by Native.getFuncDeclId().
|
staticprotected |
Referenced by Native.getImpliedEqualities().
|
staticprotected |
Referenced by Native.getIndexValue().
|
staticprotected |
Referenced by Native.getLstring().
|
staticprotected |
Referenced by Native.getNumeralDecimalString().
|
staticprotected |
Referenced by Native.getNumeralDouble().
|
staticprotected |
Referenced by Native.getNumeralInt().
|
staticprotected |
Referenced by Native.getNumeralInt64().
|
staticprotected |
Referenced by Native.getNumeralRationalInt64().
|
staticprotected |
Referenced by Native.getNumeralSmall().
|
staticprotected |
Referenced by Native.getNumeralString().
|
staticprotected |
Referenced by Native.getNumeralUint().
|
staticprotected |
Referenced by Native.getNumeralUint64().
|
staticprotected |
Referenced by Native.getNumerator().
|
staticprotected |
Referenced by Native.getNumProbes().
|
staticprotected |
Referenced by Native.getNumTactics().
|
staticprotected |
Referenced by Native.getPattern().
|
staticprotected |
Referenced by Native.getPatternNumTerms().
|
staticprotected |
Referenced by Native.getProbeName().
|
staticprotected |
Referenced by Native.getQuantifierBody().
|
staticprotected |
Referenced by Native.getQuantifierBoundName().
|
staticprotected |
Referenced by Native.getQuantifierBoundSort().
|
staticprotected |
Referenced by Native.getQuantifierNoPatternAst().
|
staticprotected |
Referenced by Native.getQuantifierNumBound().
|
staticprotected |
Referenced by Native.getQuantifierNumNoPatterns().
|
staticprotected |
Referenced by Native.getQuantifierNumPatterns().
|
staticprotected |
Referenced by Native.getQuantifierPatternAst().
|
staticprotected |
Referenced by Native.getQuantifierWeight().
|
staticprotected |
Referenced by Native.getRange().
|
staticprotected |
Referenced by Native.getRelationArity().
|
staticprotected |
Referenced by Native.getRelationColumn().
|
staticprotected |
Referenced by Native.getReSortBasis().
|
staticprotected |
Referenced by Native.getSeqSortBasis().
|
staticprotected |
Referenced by Native.getSort().
|
staticprotected |
Referenced by Native.getSortId().
|
staticprotected |
Referenced by Native.getSortKind().
|
staticprotected |
Referenced by Native.getSortName().
|
staticprotected |
Referenced by Native.getString().
|
staticprotected |
Referenced by Native.getSymbolInt().
|
staticprotected |
Referenced by Native.getSymbolKind().
|
staticprotected |
Referenced by Native.getSymbolString().
|
staticprotected |
Referenced by Native.getTacticName().
|
staticprotected |
Referenced by Native.getTupleSortFieldDecl().
|
staticprotected |
Referenced by Native.getTupleSortMkDecl().
|
staticprotected |
Referenced by Native.getTupleSortNumFields().
|
staticprotected |
Referenced by Native.getVersion().
|
staticprotected |
Referenced by Native.globalParamGet().
|
staticprotected |
Referenced by Native.globalParamResetAll().
|
staticprotected |
Referenced by Native.globalParamSet().
|
staticprotected |
Referenced by Native.goalAssert().
|
staticprotected |
Referenced by Native.goalConvertModel().
|
staticprotected |
Referenced by Native.goalDecRef().
|
staticprotected |
Referenced by Native.goalDepth().
|
staticprotected |
Referenced by Native.goalFormula().
|
staticprotected |
Referenced by Native.goalInconsistent().
|
staticprotected |
Referenced by Native.goalIncRef().
|
staticprotected |
Referenced by Native.goalIsDecidedSat().
|
staticprotected |
Referenced by Native.goalIsDecidedUnsat().
|
staticprotected |
Referenced by Native.goalNumExprs().
|
staticprotected |
Referenced by Native.goalPrecision().
|
staticprotected |
Referenced by Native.goalReset().
|
staticprotected |
Referenced by Native.goalSize().
|
staticprotected |
Referenced by Native.goalToDimacsString().
|
staticprotected |
Referenced by Native.goalToString().
|
staticprotected |
Referenced by Native.goalTranslate().
|
staticprotected |
Referenced by Native.incRef().
|
staticprotected |
Referenced by Native.interrupt().
|
staticprotected |
Referenced by Native.isAlgebraicNumber().
|
staticprotected |
Referenced by Native.isApp().
|
staticprotected |
Referenced by Native.isAsArray().
|
staticprotected |
Referenced by Native.isEqAst().
|
staticprotected |
Referenced by Native.isEqFuncDecl().
|
staticprotected |
Referenced by Native.isEqSort().
|
staticprotected |
Referenced by Native.isLambda().
|
staticprotected |
Referenced by Native.isNumeralAst().
|
staticprotected |
Referenced by Native.isQuantifierExists().
|
staticprotected |
Referenced by Native.isQuantifierForall().
|
staticprotected |
Referenced by Native.isReSort().
|
staticprotected |
Referenced by Native.isSeqSort().
|
staticprotected |
Referenced by Native.isString().
|
staticprotected |
Referenced by Native.isStringSort().
|
staticprotected |
Referenced by Native.isWellSorted().
|
staticprotected |
Referenced by Native.mkAdd().
|
staticprotected |
Referenced by Native.mkAnd().
|
staticprotected |
Referenced by Native.mkApp().
|
staticprotected |
Referenced by Native.mkArrayDefault().
|
staticprotected |
Referenced by Native.mkArrayExt().
|
staticprotected |
Referenced by Native.mkArraySort().
|
staticprotected |
Referenced by Native.mkArraySortN().
|
staticprotected |
Referenced by Native.mkAsArray().
|
staticprotected |
Referenced by Native.mkAstMap().
|
staticprotected |
Referenced by Native.mkAstVector().
|
staticprotected |
Referenced by Native.mkAtleast().
|
staticprotected |
Referenced by Native.mkAtmost().
|
staticprotected |
Referenced by Native.mkBoolSort().
|
staticprotected |
Referenced by Native.mkBound().
|
staticprotected |
Referenced by Native.mkBv2int().
|
staticprotected |
Referenced by Native.mkBvadd().
|
staticprotected |
Referenced by Native.mkBvaddNoOverflow().
|
staticprotected |
Referenced by Native.mkBvaddNoUnderflow().
|
staticprotected |
Referenced by Native.mkBvand().
|
staticprotected |
Referenced by Native.mkBvashr().
|
staticprotected |
Referenced by Native.mkBvlshr().
|
staticprotected |
Referenced by Native.mkBvmul().
|
staticprotected |
Referenced by Native.mkBvmulNoOverflow().
|
staticprotected |
Referenced by Native.mkBvmulNoUnderflow().
|
staticprotected |
Referenced by Native.mkBvnand().
|
staticprotected |
Referenced by Native.mkBvneg().
|
staticprotected |
Referenced by Native.mkBvnegNoOverflow().
|
staticprotected |
Referenced by Native.mkBvnor().
|
staticprotected |
Referenced by Native.mkBvnot().
|
staticprotected |
Referenced by Native.mkBvNumeral().
|
staticprotected |
Referenced by Native.mkBvor().
|
staticprotected |
Referenced by Native.mkBvredand().
|
staticprotected |
Referenced by Native.mkBvredor().
|
staticprotected |
Referenced by Native.mkBvsdiv().
|
staticprotected |
Referenced by Native.mkBvsdivNoOverflow().
|
staticprotected |
Referenced by Native.mkBvsge().
|
staticprotected |
Referenced by Native.mkBvsgt().
|
staticprotected |
Referenced by Native.mkBvshl().
|
staticprotected |
Referenced by Native.mkBvsle().
|
staticprotected |
Referenced by Native.mkBvslt().
|
staticprotected |
Referenced by Native.mkBvsmod().
|
staticprotected |
Referenced by Native.mkBvSort().
|
staticprotected |
Referenced by Native.mkBvsrem().
|
staticprotected |
Referenced by Native.mkBvsub().
|
staticprotected |
Referenced by Native.mkBvsubNoOverflow().
|
staticprotected |
Referenced by Native.mkBvsubNoUnderflow().
|
staticprotected |
Referenced by Native.mkBvudiv().
|
staticprotected |
Referenced by Native.mkBvuge().
|
staticprotected |
Referenced by Native.mkBvugt().
|
staticprotected |
Referenced by Native.mkBvule().
|
staticprotected |
Referenced by Native.mkBvult().
|
staticprotected |
Referenced by Native.mkBvurem().
|
staticprotected |
Referenced by Native.mkBvxnor().
|
staticprotected |
Referenced by Native.mkBvxor().
|
staticprotected |
Referenced by Native.mkConcat().
|
staticprotected |
Referenced by Native.mkConfig().
|
staticprotected |
Referenced by Native.mkConst().
|
staticprotected |
Referenced by Native.mkConstArray().
|
staticprotected |
Referenced by Native.mkConstructor().
|
staticprotected |
Referenced by Native.mkConstructorList().
|
staticprotected |
Referenced by Native.mkContext().
|
staticprotected |
Referenced by Native.mkContextRc().
|
staticprotected |
Referenced by Native.mkDatatype().
|
staticprotected |
Referenced by Native.mkDatatypes().
|
staticprotected |
Referenced by Native.mkDistinct().
|
staticprotected |
Referenced by Native.mkDiv().
|
staticprotected |
Referenced by Native.mkDivides().
|
staticprotected |
Referenced by Native.mkEmptySet().
|
staticprotected |
Referenced by Native.mkEnumerationSort().
|
staticprotected |
Referenced by Native.mkEq().
|
staticprotected |
Referenced by Native.mkExists().
|
staticprotected |
Referenced by Native.mkExistsConst().
|
staticprotected |
Referenced by Native.mkExtract().
|
staticprotected |
Referenced by Native.mkExtRotateLeft().
|
staticprotected |
Referenced by Native.mkExtRotateRight().
|
staticprotected |
Referenced by Native.mkFalse().
|
staticprotected |
Referenced by Native.mkFiniteDomainSort().
|
staticprotected |
Referenced by Native.mkFixedpoint().
|
staticprotected |
Referenced by Native.mkForall().
|
staticprotected |
Referenced by Native.mkForallConst().
|
staticprotected |
Referenced by Native.mkFpaAbs().
|
staticprotected |
Referenced by Native.mkFpaAdd().
|
staticprotected |
Referenced by Native.mkFpaDiv().
|
staticprotected |
Referenced by Native.mkFpaEq().
|
staticprotected |
Referenced by Native.mkFpaFma().
|
staticprotected |
Referenced by Native.mkFpaFp().
|
staticprotected |
Referenced by Native.mkFpaGeq().
|
staticprotected |
Referenced by Native.mkFpaGt().
|
staticprotected |
Referenced by Native.mkFpaInf().
|
staticprotected |
Referenced by Native.mkFpaIsInfinite().
|
staticprotected |
Referenced by Native.mkFpaIsNan().
|
staticprotected |
Referenced by Native.mkFpaIsNegative().
|
staticprotected |
Referenced by Native.mkFpaIsNormal().
|
staticprotected |
Referenced by Native.mkFpaIsPositive().
|
staticprotected |
Referenced by Native.mkFpaIsSubnormal().
|
staticprotected |
Referenced by Native.mkFpaIsZero().
|
staticprotected |
Referenced by Native.mkFpaLeq().
|
staticprotected |
Referenced by Native.mkFpaLt().
|
staticprotected |
Referenced by Native.mkFpaMax().
|
staticprotected |
Referenced by Native.mkFpaMin().
|
staticprotected |
Referenced by Native.mkFpaMul().
|
staticprotected |
Referenced by Native.mkFpaNan().
|
staticprotected |
Referenced by Native.mkFpaNeg().
|
staticprotected |
Referenced by Native.mkFpaNumeralDouble().
|
staticprotected |
Referenced by Native.mkFpaNumeralFloat().
|
staticprotected |
Referenced by Native.mkFpaNumeralInt().
|
staticprotected |
Referenced by Native.mkFpaNumeralInt64Uint64().
|
staticprotected |
Referenced by Native.mkFpaNumeralIntUint().
|
staticprotected |
Referenced by Native.mkFpaRem().
|
staticprotected |
Referenced by Native.mkFpaRna().
|
staticprotected |
Referenced by Native.mkFpaRne().
|
staticprotected |
Referenced by Native.mkFpaRoundingModeSort().
|
staticprotected |
Referenced by Native.mkFpaRoundNearestTiesToAway().
|
staticprotected |
Referenced by Native.mkFpaRoundNearestTiesToEven().
|
staticprotected |
Referenced by Native.mkFpaRoundToIntegral().
|
staticprotected |
Referenced by Native.mkFpaRoundTowardNegative().
|
staticprotected |
Referenced by Native.mkFpaRoundTowardPositive().
|
staticprotected |
Referenced by Native.mkFpaRoundTowardZero().
|
staticprotected |
Referenced by Native.mkFpaRtn().
|
staticprotected |
Referenced by Native.mkFpaRtp().
|
staticprotected |
Referenced by Native.mkFpaRtz().
|
staticprotected |
Referenced by Native.mkFpaSort().
|
staticprotected |
Referenced by Native.mkFpaSort128().
|
staticprotected |
Referenced by Native.mkFpaSort16().
|
staticprotected |
Referenced by Native.mkFpaSort32().
|
staticprotected |
Referenced by Native.mkFpaSort64().
|
staticprotected |
Referenced by Native.mkFpaSortDouble().
|
staticprotected |
Referenced by Native.mkFpaSortHalf().
|
staticprotected |
Referenced by Native.mkFpaSortQuadruple().
|
staticprotected |
Referenced by Native.mkFpaSortSingle().
|
staticprotected |
Referenced by Native.mkFpaSqrt().
|
staticprotected |
Referenced by Native.mkFpaSub().
|
staticprotected |
Referenced by Native.mkFpaToFpBv().
|
staticprotected |
Referenced by Native.mkFpaToFpFloat().
|
staticprotected |
Referenced by Native.mkFpaToFpIntReal().
|
staticprotected |
Referenced by Native.mkFpaToFpReal().
|
staticprotected |
Referenced by Native.mkFpaToFpSigned().
|
staticprotected |
Referenced by Native.mkFpaToFpUnsigned().
|
staticprotected |
Referenced by Native.mkFpaToIeeeBv().
|
staticprotected |
Referenced by Native.mkFpaToReal().
|
staticprotected |
Referenced by Native.mkFpaToSbv().
|
staticprotected |
Referenced by Native.mkFpaToUbv().
|
staticprotected |
Referenced by Native.mkFpaZero().
|
staticprotected |
Referenced by Native.mkFreshConst().
|
staticprotected |
Referenced by Native.mkFreshFuncDecl().
|
staticprotected |
Referenced by Native.mkFullSet().
|
staticprotected |
Referenced by Native.mkFuncDecl().
|
staticprotected |
Referenced by Native.mkGe().
|
staticprotected |
Referenced by Native.mkGoal().
|
staticprotected |
Referenced by Native.mkGt().
|
staticprotected |
Referenced by Native.mkIff().
|
staticprotected |
Referenced by Native.mkImplies().
|
staticprotected |
Referenced by Native.mkInt().
|
staticprotected |
Referenced by Native.mkInt2bv().
|
staticprotected |
Referenced by Native.mkInt2real().
|
staticprotected |
Referenced by Native.mkInt64().
|
staticprotected |
Referenced by Native.mkIntSort().
|
staticprotected |
Referenced by Native.mkIntSymbol().
|
staticprotected |
Referenced by Native.mkIntToStr().
|
staticprotected |
Referenced by Native.mkIsInt().
|
staticprotected |
Referenced by Native.mkIte().
|
staticprotected |
Referenced by Native.mkLambda().
|
staticprotected |
Referenced by Native.mkLambdaConst().
|
staticprotected |
Referenced by Native.mkLe().
|
staticprotected |
Referenced by Native.mkLinearOrder().
|
staticprotected |
Referenced by Native.mkListSort().
|
staticprotected |
Referenced by Native.mkLstring().
|
staticprotected |
Referenced by Native.mkLt().
|
staticprotected |
Referenced by Native.mkMap().
|
staticprotected |
Referenced by Native.mkMod().
|
staticprotected |
Referenced by Native.mkModel().
|
staticprotected |
Referenced by Native.mkMul().
|
staticprotected |
Referenced by Native.mkNot().
|
staticprotected |
Referenced by Native.mkNumeral().
|
staticprotected |
Referenced by Native.mkOptimize().
|
staticprotected |
Referenced by Native.mkOr().
|
staticprotected |
Referenced by Native.mkParams().
|
staticprotected |
Referenced by Native.mkPartialOrder().
|
staticprotected |
Referenced by Native.mkPattern().
|
staticprotected |
Referenced by Native.mkPbeq().
|
staticprotected |
Referenced by Native.mkPbge().
|
staticprotected |
Referenced by Native.mkPble().
|
staticprotected |
Referenced by Native.mkPiecewiseLinearOrder().
|
staticprotected |
Referenced by Native.mkPower().
|
staticprotected |
Referenced by Native.mkProbe().
|
staticprotected |
Referenced by Native.mkQuantifier().
|
staticprotected |
Referenced by Native.mkQuantifierConst().
|
staticprotected |
Referenced by Native.mkQuantifierConstEx().
|
staticprotected |
Referenced by Native.mkQuantifierEx().
|
staticprotected |
Referenced by Native.mkReal().
|
staticprotected |
Referenced by Native.mkReal2int().
|
staticprotected |
Referenced by Native.mkRealSort().
|
staticprotected |
Referenced by Native.mkRecFuncDecl().
|
staticprotected |
Referenced by Native.mkReComplement().
|
staticprotected |
Referenced by Native.mkReConcat().
|
staticprotected |
Referenced by Native.mkReEmpty().
|
staticprotected |
Referenced by Native.mkReFull().
|
staticprotected |
Referenced by Native.mkReIntersect().
|
staticprotected |
Referenced by Native.mkReLoop().
|
staticprotected |
Referenced by Native.mkRem().
|
staticprotected |
Referenced by Native.mkReOption().
|
staticprotected |
Referenced by Native.mkRepeat().
|
staticprotected |
Referenced by Native.mkRePlus().
|
staticprotected |
Referenced by Native.mkReRange().
|
staticprotected |
Referenced by Native.mkReSort().
|
staticprotected |
Referenced by Native.mkReStar().
|
staticprotected |
Referenced by Native.mkReUnion().
|
staticprotected |
Referenced by Native.mkRotateLeft().
|
staticprotected |
Referenced by Native.mkRotateRight().
|
staticprotected |
Referenced by Native.mkSelect().
|
staticprotected |
Referenced by Native.mkSelectN().
|
staticprotected |
Referenced by Native.mkSeqAt().
|
staticprotected |
Referenced by Native.mkSeqConcat().
|
staticprotected |
Referenced by Native.mkSeqContains().
|
staticprotected |
Referenced by Native.mkSeqEmpty().
|
staticprotected |
Referenced by Native.mkSeqExtract().
|
staticprotected |
Referenced by Native.mkSeqIndex().
|
staticprotected |
Referenced by Native.mkSeqInRe().
|
staticprotected |
Referenced by Native.mkSeqLastIndex().
|
staticprotected |
Referenced by Native.mkSeqLength().
|
staticprotected |
Referenced by Native.mkSeqNth().
|
staticprotected |
Referenced by Native.mkSeqPrefix().
|
staticprotected |
Referenced by Native.mkSeqReplace().
|
staticprotected |
Referenced by Native.mkSeqSort().
|
staticprotected |
Referenced by Native.mkSeqSuffix().
|
staticprotected |
Referenced by Native.mkSeqToRe().
|
staticprotected |
Referenced by Native.mkSeqUnit().
|
staticprotected |
Referenced by Native.mkSetAdd().
|
staticprotected |
Referenced by Native.mkSetComplement().
|
staticprotected |
Referenced by Native.mkSetDel().
|
staticprotected |
Referenced by Native.mkSetDifference().
|
staticprotected |
Referenced by Native.mkSetHasSize().
|
staticprotected |
Referenced by Native.mkSetIntersect().
|
staticprotected |
Referenced by Native.mkSetMember().
|
staticprotected |
Referenced by Native.mkSetSort().
|
staticprotected |
Referenced by Native.mkSetSubset().
|
staticprotected |
Referenced by Native.mkSetUnion().
|
staticprotected |
Referenced by Native.mkSignExt().
|
staticprotected |
Referenced by Native.mkSimpleSolver().
|
staticprotected |
Referenced by Native.mkSolver().
|
staticprotected |
Referenced by Native.mkSolverForLogic().
|
staticprotected |
Referenced by Native.mkSolverFromTactic().
|
staticprotected |
Referenced by Native.mkStore().
|
staticprotected |
Referenced by Native.mkStoreN().
|
staticprotected |
Referenced by Native.mkString().
|
staticprotected |
Referenced by Native.mkStringSort().
|
staticprotected |
Referenced by Native.mkStringSymbol().
|
staticprotected |
Referenced by Native.mkStrLe().
|
staticprotected |
Referenced by Native.mkStrLt().
|
staticprotected |
Referenced by Native.mkStrToInt().
|
staticprotected |
Referenced by Native.mkSub().
|
staticprotected |
Referenced by Native.mkTactic().
|
staticprotected |
Referenced by Native.mkTransitiveClosure().
|
staticprotected |
Referenced by Native.mkTreeOrder().
|
staticprotected |
Referenced by Native.mkTrue().
|
staticprotected |
Referenced by Native.mkTupleSort().
|
staticprotected |
Referenced by Native.mkUnaryMinus().
|
staticprotected |
Referenced by Native.mkUninterpretedSort().
|
staticprotected |
Referenced by Native.mkUnsignedInt().
|
staticprotected |
Referenced by Native.mkUnsignedInt64().
|
staticprotected |
Referenced by Native.mkXor().
|
staticprotected |
Referenced by Native.mkZeroExt().
|
staticprotected |
Referenced by Native.modelDecRef().
|
staticprotected |
Referenced by Native.modelEval().
|
staticprotected |
Referenced by Native.modelExtrapolate().
|
staticprotected |
Referenced by Native.modelGetConstDecl().
|
staticprotected |
Referenced by Native.modelGetConstInterp().
|
staticprotected |
Referenced by Native.modelGetFuncDecl().
|
staticprotected |
Referenced by Native.modelGetFuncInterp().
|
staticprotected |
Referenced by Native.modelGetNumConsts().
|
staticprotected |
Referenced by Native.modelGetNumFuncs().
|
staticprotected |
Referenced by Native.modelGetNumSorts().
|
staticprotected |
Referenced by Native.modelGetSort().
|
staticprotected |
Referenced by Native.modelGetSortUniverse().
|
staticprotected |
Referenced by Native.modelHasInterp().
|
staticprotected |
Referenced by Native.modelIncRef().
|
staticprotected |
Referenced by Native.modelToString().
|
staticprotected |
Referenced by Native.modelTranslate().
|
staticprotected |
Referenced by Native.openLog().
|
staticprotected |
Referenced by Native.optimizeAssert().
|
staticprotected |
Referenced by Native.optimizeAssertAndTrack().
|
staticprotected |
Referenced by Native.optimizeAssertSoft().
|
staticprotected |
Referenced by Native.optimizeCheck().
|
staticprotected |
Referenced by Native.optimizeDecRef().
|
staticprotected |
Referenced by Native.optimizeFromFile().
|
staticprotected |
Referenced by Native.optimizeFromString().
|
staticprotected |
Referenced by Native.optimizeGetAssertions().
|
staticprotected |
Referenced by Native.optimizeGetHelp().
|
staticprotected |
Referenced by Native.optimizeGetLower().
|
staticprotected |
Referenced by Native.optimizeGetLowerAsVector().
|
staticprotected |
Referenced by Native.optimizeGetModel().
|
staticprotected |
Referenced by Native.optimizeGetObjectives().
|
staticprotected |
Referenced by Native.optimizeGetParamDescrs().
|
staticprotected |
Referenced by Native.optimizeGetReasonUnknown().
|
staticprotected |
Referenced by Native.optimizeGetStatistics().
|
staticprotected |
Referenced by Native.optimizeGetUnsatCore().
|
staticprotected |
Referenced by Native.optimizeGetUpper().
|
staticprotected |
Referenced by Native.optimizeGetUpperAsVector().
|
staticprotected |
Referenced by Native.optimizeIncRef().
|
staticprotected |
Referenced by Native.optimizeMaximize().
|
staticprotected |
Referenced by Native.optimizeMinimize().
|
staticprotected |
Referenced by Native.optimizePop().
|
staticprotected |
Referenced by Native.optimizePush().
|
staticprotected |
Referenced by Native.optimizeSetParams().
|
staticprotected |
Referenced by Native.optimizeToString().
|
staticprotected |
Referenced by Native.paramDescrsDecRef().
|
staticprotected |
Referenced by Native.paramDescrsGetDocumentation().
|
staticprotected |
Referenced by Native.paramDescrsGetKind().
|
staticprotected |
Referenced by Native.paramDescrsGetName().
|
staticprotected |
Referenced by Native.paramDescrsIncRef().
|
staticprotected |
Referenced by Native.paramDescrsSize().
|
staticprotected |
Referenced by Native.paramDescrsToString().
|
staticprotected |
Referenced by Native.paramsDecRef().
|
staticprotected |
Referenced by Native.paramsIncRef().
|
staticprotected |
Referenced by Native.paramsSetBool().
|
staticprotected |
Referenced by Native.paramsSetDouble().
|
staticprotected |
Referenced by Native.paramsSetSymbol().
|
staticprotected |
Referenced by Native.paramsSetUint().
|
staticprotected |
Referenced by Native.paramsToString().
|
staticprotected |
Referenced by Native.paramsValidate().
|
staticprotected |
Referenced by Native.parseSmtlib2File().
|
staticprotected |
Referenced by Native.parseSmtlib2String().
|
staticprotected |
Referenced by Native.patternToAst().
|
staticprotected |
Referenced by Native.patternToString().
|
staticprotected |
Referenced by Native.polynomialSubresultants().
|
staticprotected |
Referenced by Native.probeAnd().
|
staticprotected |
Referenced by Native.probeApply().
|
staticprotected |
Referenced by Native.probeConst().
|
staticprotected |
Referenced by Native.probeDecRef().
|
staticprotected |
Referenced by Native.probeEq().
|
staticprotected |
Referenced by Native.probeGe().
|
staticprotected |
Referenced by Native.probeGetDescr().
|
staticprotected |
Referenced by Native.probeGt().
|
staticprotected |
Referenced by Native.probeIncRef().
|
staticprotected |
Referenced by Native.probeLe().
|
staticprotected |
Referenced by Native.probeLt().
|
staticprotected |
Referenced by Native.probeNot().
|
staticprotected |
Referenced by Native.probeOr().
|
staticprotected |
Referenced by Native.qeLite().
|
staticprotected |
Referenced by Native.qeModelProject().
|
staticprotected |
Referenced by Native.qeModelProjectSkolem().
|
staticprotected |
Referenced by Native.queryConstructor().
|
staticprotected |
Referenced by Native.rcfAdd().
|
staticprotected |
Referenced by Native.rcfDel().
|
staticprotected |
Referenced by Native.rcfDiv().
|
staticprotected |
Referenced by Native.rcfEq().
|
staticprotected |
Referenced by Native.rcfGe().
|
staticprotected |
Referenced by Native.rcfGetNumeratorDenominator().
|
staticprotected |
Referenced by Native.rcfGt().
|
staticprotected |
Referenced by Native.rcfInv().
|
staticprotected |
Referenced by Native.rcfLe().
|
staticprotected |
Referenced by Native.rcfLt().
|
staticprotected |
Referenced by Native.rcfMkE().
|
staticprotected |
Referenced by Native.rcfMkInfinitesimal().
|
staticprotected |
Referenced by Native.rcfMkPi().
|
staticprotected |
Referenced by Native.rcfMkRational().
|
staticprotected |
Referenced by Native.rcfMkRoots().
|
staticprotected |
Referenced by Native.rcfMkSmallInt().
|
staticprotected |
Referenced by Native.rcfMul().
|
staticprotected |
Referenced by Native.rcfNeg().
|
staticprotected |
Referenced by Native.rcfNeq().
|
staticprotected |
Referenced by Native.rcfNumToDecimalString().
|
staticprotected |
Referenced by Native.rcfNumToString().
|
staticprotected |
Referenced by Native.rcfPower().
|
staticprotected |
Referenced by Native.rcfSub().
|
staticprotected |
Referenced by Native.resetMemory().
|
staticprotected |
Referenced by Native.setAstPrintMode().
|
staticprotected |
Referenced by Native.setError().
|
staticprotected |
Referenced by Native.setParamValue().
|
staticprotected |
Referenced by Native.simplify().
|
staticprotected |
Referenced by Native.simplifyEx().
|
staticprotected |
Referenced by Native.simplifyGetHelp().
|
staticprotected |
Referenced by Native.simplifyGetParamDescrs().
|
staticprotected |
Referenced by Native.solverAssert().
|
staticprotected |
Referenced by Native.solverAssertAndTrack().
|
staticprotected |
Referenced by Native.solverCheck().
|
staticprotected |
Referenced by Native.solverCheckAssumptions().
|
staticprotected |
Referenced by Native.solverCube().
|
staticprotected |
Referenced by Native.solverDecRef().
|
staticprotected |
Referenced by Native.solverFromFile().
|
staticprotected |
Referenced by Native.solverFromString().
|
staticprotected |
Referenced by Native.solverGetAssertions().
|
staticprotected |
Referenced by Native.solverGetConsequences().
|
staticprotected |
Referenced by Native.solverGetHelp().
|
staticprotected |
Referenced by Native.solverGetLevels().
|
staticprotected |
Referenced by Native.solverGetModel().
|
staticprotected |
Referenced by Native.solverGetNonUnits().
|
staticprotected |
Referenced by Native.solverGetNumScopes().
|
staticprotected |
Referenced by Native.solverGetParamDescrs().
|
staticprotected |
Referenced by Native.solverGetProof().
|
staticprotected |
Referenced by Native.solverGetReasonUnknown().
|
staticprotected |
Referenced by Native.solverGetStatistics().
|
staticprotected |
Referenced by Native.solverGetTrail().
|
staticprotected |
Referenced by Native.solverGetUnits().
|
staticprotected |
Referenced by Native.solverGetUnsatCore().
|
staticprotected |
Referenced by Native.solverImportModelConverter().
|
staticprotected |
Referenced by Native.solverIncRef().
|
staticprotected |
Referenced by Native.solverInterrupt().
|
staticprotected |
Referenced by Native.solverPop().
|
staticprotected |
Referenced by Native.solverPush().
|
staticprotected |
Referenced by Native.solverReset().
|
staticprotected |
Referenced by Native.solverSetParams().
|
staticprotected |
Referenced by Native.solverToDimacsString().
|
staticprotected |
Referenced by Native.solverToString().
|
staticprotected |
Referenced by Native.solverTranslate().
|
staticprotected |
Referenced by Native.sortToAst().
|
staticprotected |
Referenced by Native.sortToString().
|
staticprotected |
Referenced by Native.statsDecRef().
|
staticprotected |
Referenced by Native.statsGetDoubleValue().
|
staticprotected |
Referenced by Native.statsGetKey().
|
staticprotected |
Referenced by Native.statsGetUintValue().
|
staticprotected |
Referenced by Native.statsIncRef().
|
staticprotected |
Referenced by Native.statsIsDouble().
|
staticprotected |
Referenced by Native.statsIsUint().
|
staticprotected |
Referenced by Native.statsSize().
|
staticprotected |
Referenced by Native.statsToString().
|
staticprotected |
Referenced by Native.substitute().
|
staticprotected |
Referenced by Native.substituteVars().
|
staticprotected |
Referenced by Native.tacticAndThen().
|
staticprotected |
Referenced by Native.tacticApply().
|
staticprotected |
Referenced by Native.tacticApplyEx().
|
staticprotected |
Referenced by Native.tacticCond().
|
staticprotected |
Referenced by Native.tacticDecRef().
|
staticprotected |
Referenced by Native.tacticFail().
|
staticprotected |
Referenced by Native.tacticFailIf().
|
staticprotected |
Referenced by Native.tacticFailIfNotDecided().
|
staticprotected |
Referenced by Native.tacticGetDescr().
|
staticprotected |
Referenced by Native.tacticGetHelp().
|
staticprotected |
Referenced by Native.tacticGetParamDescrs().
|
staticprotected |
Referenced by Native.tacticIncRef().
|
staticprotected |
Referenced by Native.tacticOrElse().
|
staticprotected |
Referenced by Native.tacticParAndThen().
|
staticprotected |
Referenced by Native.tacticParOr().
|
staticprotected |
Referenced by Native.tacticRepeat().
|
staticprotected |
Referenced by Native.tacticSkip().
|
staticprotected |
Referenced by Native.tacticTryFor().
|
staticprotected |
Referenced by Native.tacticUsingParams().
|
staticprotected |
Referenced by Native.tacticWhen().
|
staticprotected |
Referenced by Native.toApp().
|
staticprotected |
Referenced by Native.toFuncDecl().
|
staticprotected |
Referenced by Native.toggleWarningMessages().
|
staticprotected |
Referenced by Native.translate().
|
staticprotected |
Referenced by Native.updateParamValue().
|
staticprotected |
Referenced by Native.updateTerm().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3136 of file Native.java.
Referenced by Expr.isArray(), Expr.isFiniteDomain(), and Expr.isRelation().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3352 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2128 of file Native.java.
|
inlinestatic |
Definition at line 2101 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 2155 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 1112 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 999 of file Native.java.
|
inlinestatic |
Definition at line 1008 of file Native.java.
|
inlinestatic |
Definition at line 1903 of file Native.java.
|
inlinestatic |
Definition at line 4986 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2083 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 723 of file Native.java.
Referenced by Context.Context().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 1044 of file Native.java.
|
inlinestatic |
Definition at line 1070 of file Native.java.
|
inlinestatic |
Definition at line 739 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 1061 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 1372 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 1026 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 2551 of file Native.java.
|
inlinestatic |
Definition at line 2587 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 990 of file Native.java.
|
inlinestatic |
Definition at line 5483 of file Native.java.
|
inlinestatic |
Definition at line 2542 of file Native.java.
|
inlinestatic |
Definition at line 2578 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 1130 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 1103 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 3957 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2047 of file Native.java.
Referenced by Context.mkInt(), Context.mkNumeral(), and Context.mkReal().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2065 of file Native.java.
Referenced by Context.mkInt(), Context.mkNumeral(), and Context.mkReal().
|
inlinestatic |
Definition at line 963 of file Native.java.
|
inlinestatic |
Definition at line 927 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2479 of file Native.java.
|
inlinestatic |
Definition at line 1035 of file Native.java.
|
inlinestatic |
Definition at line 2173 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3514 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2029 of file Native.java.
Referenced by Context.mkInt(), Context.mkNumeral(), and Context.mkReal().
|
inlinestatic |
Definition at line 5698 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 792 of file Native.java.
|
inlinestatic |
Definition at line 2488 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2497 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4131 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 972 of file Native.java.
|
inlinestatic |
Definition at line 1148 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2335 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 2308 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 1912 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 1921 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 936 of file Native.java.
|
inlinestatic |
Definition at line 2272 of file Native.java.
|
inlinestatic |
Definition at line 2263 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4106 of file Native.java.
|
inlinestatic |
Definition at line 2515 of file Native.java.
|
inlinestatic |
Definition at line 2506 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 1017 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 945 of file Native.java.
|
inlinestatic |
Definition at line 2056 of file Native.java.
|
inlinestatic |
Definition at line 2074 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3531 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 6723 of file Native.java.
|
inlinestatic |
Definition at line 3584 of file Native.java.
Referenced by Model.getConstDecls(), and Model.getDecls().
|
inlinestatic |
Definition at line 3548 of file Native.java.
Referenced by Model.getConstInterp(), and Model.getFuncInterp().
|
inlinestatic |
Definition at line 3602 of file Native.java.
Referenced by Model.getDecls(), and Model.getFuncDecls().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3557 of file Native.java.
|
inlinestatic |
Definition at line 3523 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 3638 of file Native.java.
|
inlinestatic |
Definition at line 3793 of file Native.java.
Referenced by Log.open().
|
inlinestatic |
|
inlinestatic |
Definition at line 5731 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 5715 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 5835 of file Native.java.
|
inlinestatic |
Definition at line 5853 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 5844 of file Native.java.
|
inlinestatic |
Definition at line 5862 of file Native.java.
|
inlinestatic |
Definition at line 5707 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 874 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 866 of file Native.java.
|
inlinestatic |
Definition at line 891 of file Native.java.
Referenced by ParamDescrs.getNames(), and ParamDescrs.size().
|
inlinestatic |
|
inlinestatic |
Definition at line 809 of file Native.java.
|
inlinestatic |
Definition at line 801 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3298 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 5269 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4148 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4140 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 6732 of file Native.java.
|
inlinestatic |
Definition at line 6705 of file Native.java.
|
inlinestatic |
Definition at line 6714 of file Native.java.
|
inlinestatic |
Definition at line 1095 of file Native.java.
Referenced by Constructor.ConstructorDecl(), Constructor.getAccessorDecls(), and Constructor.getTesterDecl().
|
inlinestatic |
Definition at line 5340 of file Native.java.
|
inlinestatic |
Definition at line 5278 of file Native.java.
|
inlinestatic |
Definition at line 5367 of file Native.java.
|
inlinestatic |
Definition at line 5439 of file Native.java.
|
inlinestatic |
Definition at line 5430 of file Native.java.
|
inlinestatic |
Definition at line 5475 of file Native.java.
|
inlinestatic |
Definition at line 5412 of file Native.java.
|
inlinestatic |
Definition at line 5385 of file Native.java.
|
inlinestatic |
Definition at line 5421 of file Native.java.
|
inlinestatic |
Definition at line 5403 of file Native.java.
|
inlinestatic |
Definition at line 5313 of file Native.java.
|
inlinestatic |
Definition at line 5322 of file Native.java.
|
inlinestatic |
Definition at line 5304 of file Native.java.
|
inlinestatic |
Definition at line 5286 of file Native.java.
|
inlinestatic |
Definition at line 5331 of file Native.java.
|
inlinestatic |
Definition at line 5295 of file Native.java.
|
inlinestatic |
Definition at line 5358 of file Native.java.
|
inlinestatic |
Definition at line 5376 of file Native.java.
|
inlinestatic |
Definition at line 5448 of file Native.java.
|
inlinestatic |
Definition at line 5466 of file Native.java.
|
inlinestatic |
Definition at line 5457 of file Native.java.
|
inlinestatic |
Definition at line 5394 of file Native.java.
|
inlinestatic |
Definition at line 5349 of file Native.java.
|
inlinestatic |
Definition at line 3947 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 3909 of file Native.java.
|
static |
|
inlinestatic |
Definition at line 734 of file Native.java.
Referenced by Context.Context().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3469 of file Native.java.
Referenced by Context.getSimplifyParameterDescriptions().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4744 of file Native.java.
|
inlinestatic |
Definition at line 4583 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4664 of file Native.java.
Referenced by Solver.getAssertions(), and Solver.getNumAssertions().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4700 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4691 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4682 of file Native.java.
|
inlinestatic |
Definition at line 4673 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4541 of file Native.java.
|
inlinestatic |
Definition at line 4575 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4807 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 2677 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4833 of file Native.java.
|
inlinestatic |
|
inlinestatic |
Definition at line 4850 of file Native.java.
Referenced by Statistics.getEntries(), and Statistics.getKeys().
|
inlinestatic |
|
inlinestatic |
Definition at line 4825 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4123 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 4115 of file Native.java.
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Definition at line 3163 of file Native.java.
|
inlinestatic |
Definition at line 3172 of file Native.java.
|
inlinestatic |
Definition at line 3809 of file Native.java.
Referenced by Global.ToggleWarningMessages().
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |