Package com.microsoft.z3

Class FPRMNum

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.AST

com.microsoft.z3.Expr<FPRMSort>

com.microsoft.z3.FPRMExpr

com.microsoft.z3.FPRMNum

All Implemented Interfaces:

Comparable<AST>

public class FPRMNum
extends FPRMExpr

FloatingPoint RoundingMode Numerals

Constructor Summary

Constructors

Constructor	Description
FPRMNum(Context ctx, long obj)

Method Summary

Modifier and Type	Method	Description
boolean	isRNA()	Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
boolean	isRNE()	Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
boolean	isRoundNearestTiesToAway()	Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
boolean	isRoundNearestTiesToEven()	Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
boolean	isRoundTowardNegative()	Indicates whether the term is the floating-point rounding numeral roundTowardNegative
boolean	isRoundTowardPositive()	Indicates whether the term is the floating-point rounding numeral roundTowardPositive
boolean	isRoundTowardZero()	Indicates whether the term is the floating-point rounding numeral roundTowardZero
boolean	isRTN()	Indicates whether the term is the floating-point rounding numeral roundTowardNegative
boolean	isRTP()	Indicates whether the term is the floating-point rounding numeral roundTowardPositive
boolean	isRTZ()	Indicates whether the term is the floating-point rounding numeral roundTowardZero

Methods inherited from class com.microsoft.z3.Expr

distillSort, getArgs, getBoolValue, getFuncDecl, getIndex, getNumArgs, getSort, getString, isAdd, isAlgebraicNumber, isAnd, isArithmeticNumeral, isArray, isArrayMap, isAsArray, isBool, isBV, isBVAdd, isBVAND, isBVBitOne, isBVBitZero, isBVCarry, isBVComp, isBVConcat, isBVExtract, isBVMul, isBVNAND, isBVNOR, isBVNOT, isBVNumeral, isBVOR, isBVReduceAND, isBVReduceOR, isBVRepeat, isBVRotateLeft, isBVRotateLeftExtended, isBVRotateRight, isBVRotateRightExtended, isBVSDiv, isBVSGE, isBVSGT, isBVShiftLeft, isBVShiftRightArithmetic, isBVShiftRightLogical, isBVSignExtension, isBVSLE, isBVSLT, isBVSMod, isBVSRem, isBVSub, isBVToInt, isBVUDiv, isBVUGE, isBVUGT, isBVULE, isBVULT, isBVUMinus, isBVURem, isBVXNOR, isBVXOR, isBVXOR3, isBVZeroExtension, isConcat, isConst, isConstantArray, isDefaultArray, isDistinct, isDiv, isEmptyRelation, isEq, isFalse, isFiniteDomain, isFiniteDomainLT, isGE, isGT, isIDiv, isIff, isImplies, isInt, isIntNum, isIntToBV, isIntToReal, isIsEmptyRelation, isITE, isLabel, isLabelLit, isLE, isLT, isModulus, isMul, isNot, isNumeral, isOEQ, isOr, isProofAndElimination, isProofApplyDef, isProofAsserted, isProofCommutativity, isProofDefAxiom, isProofDefIntro, isProofDER, isProofDistributivity, isProofElimUnusedVars, isProofGoal, isProofHypothesis, isProofIFFFalse, isProofIFFOEQ, isProofIFFTrue, isProofLemma, isProofModusPonens, isProofModusPonensOEQ, isProofMonotonicity, isProofNNFNeg, isProofNNFPos, isProofOrElimination, isProofPullQuant, isProofPushQuant, isProofQuantInst, isProofQuantIntro, isProofReflexivity, isProofRewrite, isProofRewriteStar, isProofSkolemize, isProofSymmetry, isProofTheoryLemma, isProofTransitivity, isProofTransitivityStar, isProofTrue, isProofUnitResolution, isRatNum, isReal, isRealIsInt, isRealToInt, isRelation, isRelationalJoin, isRelationClone, isRelationComplement, isRelationFilter, isRelationNegationFilter, isRelationProject, isRelationRename, isRelationSelect, isRelationStore, isRelationUnion, isRelationWiden, isRemainder, isSelect, isSetComplement, isSetDifference, isSetIntersect, isSetSubset, isSetUnion, isStore, isString, isSub, isTrue, isUMinus, isWellSorted, isXor, simplify, simplify, substitute, substitute, substituteVars, toString, translate, update

Methods inherited from class com.microsoft.z3.AST

compareTo, equals, getASTKind, getId, getSExpr, hashCode, isApp, isExpr, isFuncDecl, isQuantifier, isSort, isVar

Methods inherited from class com.microsoft.z3.Z3Object

arrayLength, arrayToNative

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Details

FPRMNum

public FPRMNum(Context ctx,
 long obj)

Method Details

isRoundNearestTiesToEven

public boolean isRoundNearestTiesToEven()

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

Throws:

Z3Exception

isRNE

public boolean isRNE()

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

Throws:

Z3Exception

isRoundNearestTiesToAway

public boolean isRoundNearestTiesToAway()

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

Throws:

Z3Exception

isRNA

public boolean isRNA()

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

Throws:

Z3Exception

isRoundTowardPositive

public boolean isRoundTowardPositive()

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

Throws:

Z3Exception

isRTP

public boolean isRTP()

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

Throws:

Z3Exception

isRoundTowardNegative

public boolean isRoundTowardNegative()

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

Throws:

Z3Exception

isRTN

public boolean isRTN()

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

Throws:

Z3Exception

isRoundTowardZero

public boolean isRoundTowardZero()

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

Throws:

Z3Exception

isRTZ

public boolean isRTZ()

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

Throws:

Z3Exception