Z3 |

Public Member Functions
FPNum Class Reference
Inheritance diagram for FPNum:

## Public Member Functions
boolean | getSign ()
BitVecExpr | getSignBV ()
String | getSignificand ()
long | getSignificandUInt64 ()
BitVecExpr | getSignificandBV ()
String | getExponent (boolean biased)
long | getExponentInt64 (boolean biased)
BitVecExpr | getExponentBV (boolean biased)
boolean | isNaN ()
boolean | isInf ()
boolean | isZero ()
boolean | isNormal ()
boolean | isSubnormal ()
boolean | isPositive ()
boolean | isNegative ()
| FPNum (Context ctx, long obj)
String | toString ()
Public Member Functions inherited from FPExpr
int | getEBits ()
int | getSBits ()
| FPExpr (Context ctx, long obj)
Public Member Functions inherited from Expr< FPSort >
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< FPSort >
| Expr (Context ctx, long obj)

## Detailed Description

FloatingPoint Numerals

Definition at line 22 of file FPNum.java.

## Constructor & Destructor Documentation

## ◆ FPNum()

FPNum | ( | Context | ctx,
|  | long | obj
| ) |  |
| inline

Definition at line 181 of file FPNum.java.

182 {
183 super(ctx, obj);
184 }

## Member Function Documentation

## ◆ getExponent()

String getExponent | ( | boolean | biased | ) |
| inline

Return the exponent value of a floating-point numeral as a string Remarks: NaN is an invalid argument.

Exceptions

  Z3Exception |

Definition at line 84 of file FPNum.java.

84 {
85 return Native.fpaGetNumeralExponentString(getContext().nCtx(), getNativeObject(), biased);
86 }

## ◆ getExponentBV()

BitVecExpr getExponentBV | ( | boolean | biased | ) |
| inline

The exponent of a floating-point numeral as a bit-vector expression Remarks: NaN is an invalid argument.

Exceptions

  Z3Exception |

Definition at line 105 of file FPNum.java.

105 {
106 return new BitVecExpr(getContext(), Native.fpaGetNumeralExponentBv(getContext().nCtx(), getNativeObject(), biased));
107 }

## ◆ getExponentInt64()

long getExponentInt64 | ( | boolean | biased | ) |
| inline

Return the exponent value of a floating-point numeral as a signed 64-bit integer Remarks: NaN is an invalid argument.

Exceptions

  Z3Exception |

Definition at line 93 of file FPNum.java.

93 {
94 Native.LongPtr res = new Native.LongPtr();
95 if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res, biased))
96 throw new Z3Exception("Exponent is not a 64 bit integer");
97 return res.value;
98 }

## ◆ getSign()

boolean getSign | ( |  | ) |
| inline

Retrieves the sign of a floating-point literal
Remarks: returns true if the numeral is negative

Exceptions

  Z3Exception |

Definition at line 29 of file FPNum.java.

29 {
30 Native.IntPtr res = new Native.IntPtr();
31 if (!Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res))
32 throw new Z3Exception("Sign is not a Boolean value");
33 return res.value != 0;
34 }

## ◆ getSignBV()

BitVecExpr getSignBV | ( |  | ) |
| inline

The sign of a floating-point numeral as a bit-vector expression Remarks: NaN's do not have a bit-vector sign, so they are invalid arguments.

Exceptions

  Z3Exception |

Definition at line 41 of file FPNum.java.

41 {
42 return new BitVecExpr(getContext(), Native.fpaGetNumeralSignBv(getContext().nCtx(), getNativeObject()));
43 }

## ◆ getSignificand()

String getSignificand | ( |  | ) |
| inline

The significand value of a floating-point numeral as a string Remarks: The significand s is always 0 < s < 2.0; the resulting string is long enough to represent the real significand precisely.

Exceptions

  Z3Exception |

Definition at line 51 of file FPNum.java.

51 {
52 return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
53 }

## ◆ getSignificandBV()

BitVecExpr getSignificandBV | ( |  | ) |
| inline

The significand of a floating-point numeral as a bit-vector expression Remarks: NaN is an invalid argument.

Exceptions

  Z3Exception |

Definition at line 75 of file FPNum.java.

75 {
76 return new BitVecExpr(getContext(), Native.fpaGetNumeralSignificandBv(getContext().nCtx(), getNativeObject()));
77 }

## ◆ getSignificandUInt64()

long getSignificandUInt64 | ( |  | ) |
| inline

The significand value of a floating-point numeral as a UInt64 Remarks: This function extracts the significand bits, without the hidden bit or normalization. Throws an exception if the significand does not fit into a UInt64.

Exceptions

  Z3Exception |

Definition at line 62 of file FPNum.java.

63 {
64 Native.LongPtr res = new Native.LongPtr();
65 if (!Native.fpaGetNumeralSignificandUint64(getContext().nCtx(), getNativeObject(), res))
66 throw new Z3Exception("Significand is not a 64 bit unsigned integer");
67 return res.value;
68 }

## ◆ isInf()

boolean isInf | ( |  | ) |
| inline

Indicates whether the numeral is a +oo or -oo.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 125 of file FPNum.java.

126 {
127 return Native.fpaIsNumeralInf(getContext().nCtx(), getNativeObject());
128 }

## ◆ isNaN()

boolean isNaN | ( |  | ) |
| inline

Indicates whether the numeral is a NaN.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 115 of file FPNum.java.

116 {
117 return Native.fpaIsNumeralNan(getContext().nCtx(), getNativeObject());
118 }

## ◆ isNegative()

boolean isNegative | ( |  | ) |
| inline

Indicates whether the numeral is negative.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 175 of file FPNum.java.

176 {
177 return Native.fpaIsNumeralNegative(getContext().nCtx(), getNativeObject());
178 }

## ◆ isNormal()

boolean isNormal | ( |  | ) |
| inline

Indicates whether the numeral is normal.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 145 of file FPNum.java.

146 {
147 return Native.fpaIsNumeralNormal(getContext().nCtx(), getNativeObject());
148 }

## ◆ isPositive()

boolean isPositive | ( |  | ) |
| inline

Indicates whether the numeral is positive.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 165 of file FPNum.java.

166 {
167 return Native.fpaIsNumeralPositive(getContext().nCtx(), getNativeObject());
168 }

## ◆ isSubnormal()

boolean isSubnormal | ( |  | ) |
| inline

Indicates whether the numeral is subnormal.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 155 of file FPNum.java.

156 {
157 return Native.fpaIsNumeralSubnormal(getContext().nCtx(), getNativeObject());
158 }

## ◆ isZero()

boolean isZero | ( |  | ) |
| inline

Indicates whether the numeral is +zero or -zero.

Exceptions

  Z3Exception | on error

Returns
  a boolean

Definition at line 135 of file FPNum.java.

136 {
137 return Native.fpaIsNumeralZero(getContext().nCtx(), getNativeObject());
138 }

## ◆ toString()

String toString | ( |  | ) |
| inline

Returns a string representation of the numeral.

Definition at line 189 of file FPNum.java.

190 {
191 return Native.getNumeralString(getContext().nCtx(), getNativeObject());
192 }