Skip to content

Commit 2f26a45

Browse files
author
BaierD
committed
Make single/double precision checks for FloatingPointNumber public and add a JavaDoc
1 parent 4709172 commit 2f26a45

File tree

1 file changed

+17
-5
lines changed

1 file changed

+17
-5
lines changed

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

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -68,20 +68,32 @@ public static FloatingPointNumber of(String bits, int exponentSize, int mantissa
6868
return of(sign, exponent, mantissa, exponentSize, mantissaSize);
6969
}
7070

71-
private boolean isSinglePrecision() {
71+
/**
72+
* Returns true if this floating-point number is an IEEE-754-2008 single precision type with 32
73+
* bits length consisting of an 8 bit exponent, a 23 bit mantissa and a single sign bit.
74+
*
75+
* @return true for IEEE-754 single precision type, false otherwise.
76+
*/
77+
public boolean isIEEE754SinglePrecision() {
7278
return getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE
7379
&& getMantissaSize() == SINGLE_PRECISION_MANTISSA_SIZE;
7480
}
7581

76-
private boolean isDoublePrecision() {
82+
/**
83+
* Returns true if this floating-point number is an IEEE-754-2008 double precision type with 64
84+
* bits length consisting of an 11 bit exponent, a 52 bit mantissa and a single sign bit.
85+
*
86+
* @return true for IEEE-754 double precision type, false otherwise.
87+
*/
88+
public boolean isIEEE754DoublePrecision() {
7789
return getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE
7890
&& getMantissaSize() == DOUBLE_PRECISION_MANTISSA_SIZE;
7991
}
8092

8193
/** compute a representation as Java-based float value, if possible. */
8294
public float floatValue() {
8395
Preconditions.checkArgument(
84-
isSinglePrecision(),
96+
isIEEE754SinglePrecision(),
8597
"Can not represent floating point number %s as Java-based float value.",
8698
this);
8799
var bits = getBits();
@@ -91,10 +103,10 @@ public float floatValue() {
91103
/** compute a representation as Java-based double value, if possible. */
92104
public double doubleValue() {
93105
Preconditions.checkArgument(
94-
isSinglePrecision() || isDoublePrecision(),
106+
isIEEE754SinglePrecision() || isIEEE754DoublePrecision(),
95107
"Can not represent floating point number %s as Java-based double value.",
96108
this);
97-
if (isSinglePrecision()) {
109+
if (isIEEE754SinglePrecision()) {
98110
// lets be nice to the user and automatically convert from single to double precision
99111
return floatValue();
100112
}

0 commit comments

Comments
 (0)