|
Z3
|
|
|
Z3
|
|
Inheritance diagram for ArithExpr< R extends ArithSort >:Additional Inherited Members | |
| Public Member Functions inherited from Expr< R > | |
| Expr< R > | simplify () |
| Expr< R > | simplify (Params p) |
| FuncDecl< R > | getFuncDecl () |
| Z3_lbool | getBoolValue () |
| int | getNumArgs () |
| Expr<?>[] | getArgs () |
| Expr< R > | update (Expr<?>[] args) |
| Expr< R > | substitute (Expr<?>[] from, Expr<?>[] to) |
| Expr< R > | substitute (Expr<?> from, Expr<?> to) |
| Expr< R > | substituteVars (Expr<?>[] to) |
| Expr< R > | translate (Context ctx) |
| String | toString () |
| boolean | isNumeral () |
| boolean | isWellSorted () |
| R | getSort () |
| boolean | isConst () |
| boolean | isIntNum () |
| boolean | isRatNum () |
| boolean | isAlgebraicNumber () |
| boolean | isBool () |
| boolean | isTrue () |
| boolean | isFalse () |
| boolean | isEq () |
| boolean | isDistinct () |
| boolean | isITE () |
| boolean | isAnd () |
| boolean | isOr () |
| boolean | isIff () |
| boolean | isXor () |
| boolean | isNot () |
| boolean | isImplies () |
| boolean | isInt () |
| boolean | isReal () |
| boolean | isArithmeticNumeral () |
| boolean | isLE () |
| boolean | isGE () |
| boolean | isLT () |
| boolean | isGT () |
| boolean | isAdd () |
| boolean | isSub () |
| boolean | isUMinus () |
| boolean | isMul () |
| boolean | isDiv () |
| boolean | isIDiv () |
| boolean | isRemainder () |
| boolean | isModulus () |
| boolean | isIntToReal () |
| boolean | isRealToInt () |
| boolean | isRealIsInt () |
| boolean | isArray () |
| boolean | isStore () |
| boolean | isSelect () |
| boolean | isConstantArray () |
| boolean | isDefaultArray () |
| boolean | isArrayMap () |
| boolean | isAsArray () |
| boolean | isSetUnion () |
| boolean | isSetIntersect () |
| boolean | isSetDifference () |
| boolean | isSetComplement () |
| boolean | isSetSubset () |
| boolean | isBV () |
| boolean | isBVNumeral () |
| boolean | isBVBitOne () |
| boolean | isBVBitZero () |
| boolean | isBVUMinus () |
| boolean | isBVAdd () |
| boolean | isBVSub () |
| boolean | isBVMul () |
| boolean | isBVSDiv () |
| boolean | isBVUDiv () |
| boolean | isBVSRem () |
| boolean | isBVURem () |
| boolean | isBVSMod () |
| boolean | isBVULE () |
| boolean | isBVSLE () |
| boolean | isBVUGE () |
| boolean | isBVSGE () |
| boolean | isBVULT () |
| boolean | isBVSLT () |
| boolean | isBVUGT () |
| boolean | isBVSGT () |
| boolean | isBVAND () |
| boolean | isBVOR () |
| boolean | isBVNOT () |
| boolean | isBVXOR () |
| boolean | isBVNAND () |
| boolean | isBVNOR () |
| boolean | isBVXNOR () |
| boolean | isBVConcat () |
| boolean | isBVSignExtension () |
| boolean | isBVZeroExtension () |
| boolean | isBVExtract () |
| boolean | isBVRepeat () |
| boolean | isBVReduceOR () |
| boolean | isBVReduceAND () |
| boolean | isBVComp () |
| boolean | isBVShiftLeft () |
| boolean | isBVShiftRightLogical () |
| boolean | isBVShiftRightArithmetic () |
| boolean | isBVRotateLeft () |
| boolean | isBVRotateRight () |
| boolean | isBVRotateLeftExtended () |
| boolean | isBVRotateRightExtended () |
| boolean | isIntToBV () |
| boolean | isBVToInt () |
| boolean | isBVCarry () |
| boolean | isBVXOR3 () |
| boolean | isLabel () |
| boolean | isLabelLit () |
| boolean | isString () |
| String | getString () |
| boolean | isConcat () |
| boolean | isOEQ () |
| boolean | isProofTrue () |
| boolean | isProofAsserted () |
| boolean | isProofGoal () |
| boolean | isProofModusPonens () |
| boolean | isProofReflexivity () |
| boolean | isProofSymmetry () |
| boolean | isProofTransitivity () |
| boolean | isProofTransitivityStar () |
| boolean | isProofMonotonicity () |
| boolean | isProofQuantIntro () |
| boolean | isProofDistributivity () |
| boolean | isProofAndElimination () |
| boolean | isProofOrElimination () |
| boolean | isProofRewrite () |
| boolean | isProofRewriteStar () |
| boolean | isProofPullQuant () |
| boolean | isProofPushQuant () |
| boolean | isProofElimUnusedVars () |
| boolean | isProofDER () |
| boolean | isProofQuantInst () |
| boolean | isProofHypothesis () |
| boolean | isProofLemma () |
| boolean | isProofUnitResolution () |
| boolean | isProofIFFTrue () |
| boolean | isProofIFFFalse () |
| boolean | isProofCommutativity () |
| boolean | isProofDefAxiom () |
| boolean | isProofDefIntro () |
| boolean | isProofApplyDef () |
| boolean | isProofIFFOEQ () |
| boolean | isProofNNFPos () |
| boolean | isProofNNFNeg () |
| boolean | isProofSkolemize () |
| boolean | isProofModusPonensOEQ () |
| boolean | isProofTheoryLemma () |
| boolean | isRelation () |
| boolean | isRelationStore () |
| boolean | isEmptyRelation () |
| boolean | isIsEmptyRelation () |
| boolean | isRelationalJoin () |
| boolean | isRelationUnion () |
| boolean | isRelationWiden () |
| boolean | isRelationProject () |
| boolean | isRelationFilter () |
| boolean | isRelationNegationFilter () |
| boolean | isRelationRename () |
| boolean | isRelationComplement () |
| boolean | isRelationSelect () |
| boolean | isRelationClone () |
| boolean | isFiniteDomain () |
| boolean | isFiniteDomainLT () |
| int | getIndex () |
| Protected Member Functions inherited from Expr< R > | |
| Expr (Context ctx, long obj) | |
Arithmetic expressions (int/real)
Definition at line 23 of file ArithExpr.java.
1.9.1
