Public Member Functions | |
int | getInt () |
long | getInt64 () |
BigInteger | getBigInteger () |
String | toString () |
![]() | |
Expr | simplify () |
Expr | simplify (Params p) |
FuncDecl | getFuncDecl () |
Z3_lbool | getBoolValue () |
int | getNumArgs () |
Expr[] | getArgs () |
void | update (Expr[] args) |
Expr | substitute (Expr[] from, Expr[] to) |
Expr | substitute (Expr from, Expr to) |
Expr | substituteVars (Expr[] to) |
Expr | translate (Context ctx) |
String | toString () |
boolean | isNumeral () |
boolean | isWellSorted () |
Sort | 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 | 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 | isProofPullQuantStar () |
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 | isProofNNFStar () |
boolean | isProofCNFStar () |
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 () |
![]() | |
boolean | equals (Object o) |
int | compareTo (Object other) |
int | hashCode () |
int | getId () |
AST | translate (Context ctx) |
Z3_ast_kind | getASTKind () |
boolean | isExpr () |
boolean | isApp () |
boolean | isVar () |
boolean | isQuantifier () |
boolean | isSort () |
boolean | isFuncDecl () |
String | toString () |
String | getSExpr () |
![]() | |
void | dispose () |
![]() | |
void | dispose () |
Additional Inherited Members | |
![]() | |
Expr (Context ctx) | |
Expr (Context ctx, long obj) | |
![]() | |
void | finalize () |
Integer Numerals
Definition at line 25 of file IntNum.java.
|
inline |
|
inline |
Retrieve the int value.
Definition at line 36 of file IntNum.java.
|
inline |
Retrieve the 64-bit int value.
Definition at line 47 of file IntNum.java.
|
inline |
Returns a string representation of the numeral.
Definition at line 66 of file IntNum.java.
Referenced by RatNum.getBigIntDenominator(), IntNum.getBigInteger(), and RatNum.getBigIntNumerator().