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 ()
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 ()

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.

                                          {
        super(ctx, obj);
    }

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.

{ 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.

{ 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.

{ 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.

{ 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.

{ 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.

{ 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.

{ 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.

{ 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.

{ 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.

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