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