Refactor `FloatingPointNumber` by daniel-raffler · Pull Request #594 · sosy-lab/java-smt

daniel-raffler · 2026-02-10T11:19:07Z

Hello,

after #513 the only way to create a FloatingPointNumber is to use FloatingPointNumber.of(String, FloatingPointType) or FloatingPointNumber.of(Sign, BigInteger, BigInteger, FloatingPointType). Both methods accept a FloatingPointType for the exponent and mantissa size. Versions of FloatingPointNumber.of(...) that accept mantissa and exponent size as separate integer arguments have been deprecated as it was not clear if the hidden bit should be included in the mantissa size, or not

However, when reading out the mantissa/exponent size of there is no way to get the FloatingPointType from an existing FoatingPointNumber. Instead, the sizes have to be accessed separately though FloatingPointNumber.getExponentSizeand FloatingPointNumber.getMantissaSizeWith(out)HiddenBit, which can be error prone:

public FloatingPointType getFloatingPointType(FloatingPointNumber pFloat) {
    return FormulaType.getFloatingPointTypeFromSizesWithoutHiddenBit(
        pFloat.getExponentSize(), pFloat.getMantissaSizeWithHiddenBit()); // there is a bug here
  }

In this PR we try to fix the issue by adding a new method FloatingPointNumber.getFloatingPointType() to get the FloatingPointType of a FloatingPointNumber. We also change the implementation, so that the FloatingPointType is stored directly when creating a new FloatingPointNumber, and add some additional sanity checks for the sizes

…er, FloatingPointType)`

…nteger, BigInteger, int, int)` We have two deprecated arguments here, and users are supposed to choose how to replace `FormulaType.getFloatingPointType()`, and if the hidden bit is supposed to be counted or not

baierd · 2026-02-10T16:23:32Z

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

-      staticImports =
-          "org.sosy_lab.java_smt.api.FormulaType"
-              + ".getFloatingPointTypeFromSizesWithoutHiddenBit")
+  @SuppressWarnings("InlineMeSuggester")


Why is inline me not working anymore? Sometimes its a little tricky to find the correct expression for it.

I removed this one because the user is supposed to choose between getFloatingPointTypeFromSizesWithHiddenBit and getFloatingPointTypeFromSizesWithoutHiddenBit for the replacement

baierd · 2026-02-10T16:23:47Z

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

  @Deprecated(
      since = "2026.01, because mantissa arguments with/without sign bits can be misleading",
      forRemoval = true)
+  @SuppressWarnings("InlineMeSuggester")


Why is inline me not working anymore? Sometimes its a little tricky to find the correct expression for it.

It wasn't working before 😉 These warnings showed up after I removed some redundant checks and the method was just a single expression. Now that some null checks have been added again the @SuppressWarnings isn't actually needed, and I removed it again

baierd · 2026-02-10T16:24:21Z

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

-        floatingPointType.getExponentSize(),
-        floatingPointType.getMantissaSizeWithoutHiddenBit());
+    Preconditions.checkArgument(
+        exponent.compareTo(BigInteger.ZERO) >= 0, "Exponent must not be negative");


You can use the BigInteger signum for this.

Thanks for the hint!

baierd · 2026-02-10T16:24:45Z

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

  @Deprecated(
      since = "2026.01, because mantissa arguments with/without sign bits can be misleading",
      forRemoval = true)
+  @SuppressWarnings("InlineMeSuggester")


Why is inline me not working anymore? Sometimes its a little tricky to find the correct expression for it.

baierd · 2026-02-10T16:26:36Z

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

+        FloatingPointType.class,
+        FormulaType.getSinglePrecisionFloatingPointType(),
+        FormulaType.getDoublePrecisionFloatingPointType());
    setDefault(FloatingPointType.class, getSinglePrecisionFloatingPointType());


Seems like we set this twice now?

Yes, you're right. I've removed the setDefault

baierd · 2026-02-10T16:28:14Z

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

   */
  public static FloatingPointType getFloatingPointTypeFromSizesWithHiddenBit(
      int exponentSize, int mantissaSizeWithHiddenBit) {
+    checkArgument(


Maybe we should stick to the standards wording here, in that it should be "greather than 1".

From:

:sorts-description "All nullary sort symbols of the form (_ FloatingPoint eb sb), where eb and sb are numerals greater than 1."

Thanks, I've updated the error messages

baierd · 2026-02-10T16:29:43Z

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

    // size with hidden bit
    var exponentSize = floatingPointType.getExponentSize();
    var mantissaSizeWithoutHiddenBit = floatingPointType.getMantissaSizeWithoutHiddenBit();
+    Preconditions.checkArgument(exponentSize >= 0, "Exponent size must not be negative");


We should check this only once, and that location is clearly the type (so that we are failing early). This also applies to the other duplicate checks in this class.

Thanks, the extra check has been removed

baierd · 2026-02-10T16:31:06Z

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

+    Preconditions.checkArgument(
+        mantissa.compareTo(BigInteger.ZERO) >= 0, "Mantissa must not be negative");
+    Preconditions.checkArgument(
+        exponent.bitLength() <= floatingPointType.getExponentSize(),


Shouldn't this be a ==?

No, I think this should be fine. The exponent may have leading zeroes that are not counted by BigInteger.bitLength

baierd · 2026-02-10T16:31:42Z

@kfriedberger is this change/idea OK for you?

We already have `setDistinctValues`, making the `setDefault` redundant

daniel-raffler added 11 commits February 9, 2026 15:17

Add getFloatingPointType() to FloatingPointNumber

4184945

Add range check in `FloatingPointNumber.of(Sign, BigInteger, BigInteg…

ebc249c

…er, FloatingPointType)`

Add error messages for the range checks

23d9e43

Add range check in FloatingPointNumber.of(String, FloatingPointType)

10ca608

Remove redundant checks

39d3ceb

Remove @InlineMe suggestion for `FloatingPointNumber.of(boolean, BigI…

7f7e76a

…nteger, BigInteger, int, int)` We have two deprecated arguments here, and users are supposed to choose how to replace `FormulaType.getFloatingPointType()`, and if the hidden bit is supposed to be counted or not

Add range check for FloatingPointTypes

d7c72f1

Add missing dot

f210f50

Fix null checks

3b76d59

Fix equals check

5e4b516

Fix CI

b828076

daniel-raffler requested a review from baierd February 10, 2026 11:19

daniel-raffler added enhancement API labels Feb 10, 2026

Improve error messages

a6c3f69

baierd assigned daniel-raffler Feb 10, 2026

baierd requested changes Feb 10, 2026

View reviewed changes

daniel-raffler added 5 commits February 10, 2026 20:24

Use BigInteger.signum() to check if exponent and mantissa are positive

f235685

Use Smtlib phrasing for error messages

a63de2f

Remove redundant check

8c734ac

Remove unused @SuppressWarnings for InlineMe

bd275a0

Remove default value for FloatingPointType in api SanityTest

3ecb482

We already have `setDistinctValues`, making the `setDefault` redundant

Conversation

daniel-raffler commented Feb 10, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

baierd commented Feb 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

2 participants