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.

     {
         super(ctx, obj);
     }

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

◆ toString()

String toString ( )

inline

Returns a string representation of the numeral.

Definition at line 189 of file FPNum.java.

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

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ FPNum()

Member Function Documentation

◆ getExponent()

◆ getExponentBV()

◆ getExponentInt64()

◆ getSign()

◆ getSignBV()

◆ getSignificand()

◆ getSignificandBV()

◆ getSignificandUInt64()

◆ isInf()

◆ isNaN()

◆ isNegative()

◆ isNormal()

◆ isPositive()

◆ isSubnormal()

◆ isZero()

◆ toString()