Skip to content

Commit bef62a7

Browse files
committed
improve the documentation of FloatingPointNumber.
The sign bit represents a negative number, as used by SMTLIB and IEEE 754. This is a first step for #433.
1 parent 720ccad commit bef62a7

File tree

1 file changed

+15
-3
lines changed

1 file changed

+15
-3
lines changed

src/org/sosy_lab/java_smt/api/FloatingPointNumber.java

+15-3
Original file line numberDiff line numberDiff line change
@@ -27,13 +27,25 @@ public abstract class FloatingPointNumber {
2727
public static final int DOUBLE_PRECISION_EXPONENT_SIZE = 11;
2828
public static final int DOUBLE_PRECISION_MANTISSA_SIZE = 52;
2929

30-
/** Whether the number is positive (TRUE) or negative (FALSE). */
30+
/**
31+
* Whether the number is positive (FALSE) or negative (TRUE).
32+
*
33+
* <p>See IEEE 754 or <a href="https://smt-lib.org/theories-FloatingPoint.shtml">SMTLIB FP
34+
* theory</a> for details on the sign bit.
35+
*/
3136
public abstract boolean getSign();
3237

33-
/** The exponent of the floating-point number, given as numeric value. */
38+
/**
39+
* The exponent of the floating-point number, given as numeric value from binary representation.
40+
* The number is unsigned (not negative) and does not include the bias that is used in IEEE 754.
41+
*/
3442
public abstract BigInteger getExponent();
3543

36-
/** The mantissa (aka significand) of the floating-point number, given as numeric value. */
44+
/**
45+
* The mantissa (aka significand) of the floating-point number, given as numeric value from binary
46+
* representation. The mantissa does not include the hidden bit that is used to denote normalized
47+
* numbers in IEEE 754.
48+
*/
3749
public abstract BigInteger getMantissa();
3850

3951
public abstract int getExponentSize();

0 commit comments

Comments
 (0)