Z3
Public Member Functions
FPRMNum Class Reference
+ Inheritance diagram for FPRMNum:

Public Member Functions

boolean isRoundNearestTiesToEven ()
 
boolean isRNE ()
 
boolean isRoundNearestTiesToAway ()
 
boolean isRNA ()
 
boolean isRoundTowardPositive ()
 
boolean isRTP ()
 
boolean isRoundTowardNegative ()
 
boolean isRTN ()
 
boolean isRoundTowardZero ()
 
boolean isRTZ ()
 
 FPRMNum (Context ctx, long obj)
 
- Public Member Functions inherited from FPRMExpr
 FPRMExpr (Context ctx, long obj)
 
- Public Member Functions inherited from Expr< FPRMSort >
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 ()
 
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 ()
 

Additional Inherited Members

- Protected Member Functions inherited from Expr< FPRMSort >
 Expr (Context ctx, long obj)
 

Detailed Description

FloatingPoint RoundingMode Numerals

Definition at line 24 of file FPRMNum.java.

Constructor & Destructor Documentation

◆ FPRMNum()

FPRMNum ( Context  ctx,
long  obj 
)
inline

Definition at line 86 of file FPRMNum.java.

86  {
87  super(ctx, obj);
88  }

Member Function Documentation

◆ isRNA()

boolean isRNA ( )
inline

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway

Exceptions
Z3Exception

Definition at line 48 of file FPRMNum.java.

48 { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }

◆ isRNE()

boolean isRNE ( )
inline

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven

Exceptions
Z3Exception

Definition at line 36 of file FPRMNum.java.

36 { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }

◆ isRoundNearestTiesToAway()

boolean isRoundNearestTiesToAway ( )
inline

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway

Exceptions
Z3Exception

Definition at line 42 of file FPRMNum.java.

42 { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; }

◆ isRoundNearestTiesToEven()

boolean isRoundNearestTiesToEven ( )
inline

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven

Exceptions
Z3Exception

Definition at line 30 of file FPRMNum.java.

30 { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; }

◆ isRoundTowardNegative()

boolean isRoundTowardNegative ( )
inline

Indicates whether the term is the floating-point rounding numeral roundTowardNegative

Exceptions
Z3Exception

Definition at line 66 of file FPRMNum.java.

66 { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }

◆ isRoundTowardPositive()

boolean isRoundTowardPositive ( )
inline

Indicates whether the term is the floating-point rounding numeral roundTowardPositive

Exceptions
Z3Exception

Definition at line 54 of file FPRMNum.java.

54 { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }

◆ isRoundTowardZero()

boolean isRoundTowardZero ( )
inline

Indicates whether the term is the floating-point rounding numeral roundTowardZero

Exceptions
Z3Exception

Definition at line 78 of file FPRMNum.java.

78 { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }

◆ isRTN()

boolean isRTN ( )
inline

Indicates whether the term is the floating-point rounding numeral roundTowardNegative

Exceptions
Z3Exception

Definition at line 72 of file FPRMNum.java.

72 { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; }

◆ isRTP()

boolean isRTP ( )
inline

Indicates whether the term is the floating-point rounding numeral roundTowardPositive

Exceptions
Z3Exception

Definition at line 60 of file FPRMNum.java.

60 { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; }

◆ isRTZ()

boolean isRTZ ( )
inline

Indicates whether the term is the floating-point rounding numeral roundTowardZero

Exceptions
Z3Exception

Definition at line 84 of file FPRMNum.java.

84 { return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; }
com.microsoft.z3.Expr< FPRMSort >::getFuncDecl
FuncDecl< R > getFuncDecl()
Definition: Expr.java:73
Z3_decl_kind
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1000