Fix Floating-Point Mantissa Not Including Sign Bit #513

baierd · 2025-09-02T08:13:13Z

While implementing PR 512 i found a problem in our implementation of FloatingPointType and number. Our returned significant precision is off by one, see SMTLib2 standard page for Floating-Points. E.g. for single precision FP, we return significant size 23. But the standard defines exponent and significant as:

eb defines the number of bits in the exponent;
sb defines the number of bits in the significand, *including* the hidden bit.

Hence it should be 24.
As a consequence, we also return this wrongly for FormulaType method toSMTLIBString().
This is fixed in this PR.
We also encode the significant without the hidden bit in toString(), and subsequently in fromString.
While this is in general not as bad, i changed it to include the hidden bit now (in both), so that it is in-line with the standard.
These behavior changes should be communicated clearly to users!

The solvers generally expect the hidden bit to be part of the significant, hence why we had 4 solvers with the code type.getMantissaSize() + 1, and only one solver without the + 1 (MathSAT5).

The general behavior of FP creation/solving is correct IFF you know that the mantissa does not include the sign bit.

Also, we don't communicate any information about our interpretation of FP precisions, hence the users might think that by building FormulaType.getFloatingPointType(8, 24) (first input is exponent, second is significant) they get a single precision FP-type, but in reality they get a total size of 33 bits currently. Our static implementation of the single/double precisions is fine however.

This PR adds/changes the following:

Add new constructors for FP type that specify the sign bit inclusion in the method name. Also, update the API for getMantissaSize() to getMantissaSizeWithHiddenBit() and getMantissaSizeWithoutHiddenBit().
Use the less ambiguous API in our internal implementation, reducing confusion about magic +-1
Including the hidden bit in the documentation of relevant API, as well as the parameter names.
Deprecate the old FP type constructor and mantissa size getters.
Return the correct SMTLIB2 interpretation for FloatingPointType.toSMTLIBString().
Change behavior of FloatingPointType.toString() and FloatingPointType.fromString() to include the hidden bit in the significant.
Deprecated public constants for FP single/double precisions, as they do not specify the in/exclusion of the hidden bit and will be moved to internal API. Also added new constants that are not public for mantissas that specify the hidden bit exclusion.
Adds tests for FP precision sizes, as well as FloatingPointType.toString() etc.

I feel like the API changes reduce the magic + 1 and - 1 by a large amount, increasing readability of the code. My guess is that users, especially new users, will benefit from that. The deprecation warning needs to be discussed/done.

…BV transformation and width comparison

…he type/mantissa with/without sign bit and add sign bit to toString and toSMTLIBString representations

…a with/without sign bit and use those as far as possible to make the code unambiguous for mantissas

…n bit and add some assertions for mantissa/exponent

PhilippWendler · 2025-09-02T08:41:43Z

What is the actual effect of this MR (supposed to be)? Is it purely an API improvement that adds new methods and deprecates some old ones, or does it actually change the behavior in some cases? From your previous off-line explanations and from the title ("Fix") I would assume that there was actually broken behavior that is now fixed. But in the description of the MR I do not find anything related to this and it reads as if there is just new stuff and no behavior changes. Please make clear which is the case, and if no existing behavior is actually broken and needs to be changed, reflect this in the MR title.

Fix FP type etc. to include the sign bit, and switch to what the standard defines in our internal implementation. Only MathSAT5 expects the mantissa to not include the sign bit.

This wording doesn't really make sense. The FloatingPointType class itself (I assume this is what you mean) is not broken and does not need to be fixed, and the MR also does not attempt to fix it nor changes anything in it (except for toString()). What is broken and fixed is only that there are existing methods with unclear names and missing documentation.

baierd · 2025-09-02T08:58:32Z

What is the actual effect of this MR (supposed to be)? Is it purely an API improvement that adds new methods and deprecates some old ones, or does it actually change the behavior in some cases?

The behavior is unchanged. It only improves the API, adds new methods, and improves code readability/maintainability.

The main problem is that the standard defines the mantissa to include the sign bit, but our API does not. 4/5 SMT solvers with FP support in JavaSMT handle it the same way. Only some parts of the related API are documented, hence users might assume that our API works like the standard or the majority of the solvers describe it. This PR aims to fix this ambiguity. I improved the wording above.

PhilippWendler · 2025-09-02T09:00:33Z

For the record: I find it good that you decided to not add getMantissaSizeWithSignBit() and getExponentSize() to FloatingPointFormulaManager as it was done in #512. These methods are not necessary, encourage bad code (users should pass around FP size information as FloatingPointType instances instead of two ints), and their implementations contained redundant code that duplicated already existing code in JavaSMT (making it more error prone).

PhilippWendler

It think I found several bugs. It seems this strongly highlights the need for more tests covering this.

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

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

src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java

PhilippWendler · 2025-09-02T11:32:06Z

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

    @Override
    public String toSMTLIBString() {
-      return "(_ FloatingPoint " + exponentSize + " " + mantissaSize + ")";
+      return "(_ FloatingPoint " + exponentSize + " " + getMantissaSizeWithSignBit() + ")";


Hm, this seems to be a desired behavior change of this MR, isn't it?

So it would mean that there are not just API improvements but also an actual bug fix. Hopefully this method is rarely used?

The SMTLIB2 standard says that our previous implementation is wrong here, as statet above As a consequence, we also return this wrongly for toSMTLIBString() etc.. Example from the standard: - Float32 is a synonym for (_ FloatingPoint 8 24). As a consequence i would change it and communicate this to the users.

I updated the initial PR text accordingly.

This one-line-fix could have been part of a separate PR, which might have been accepted much easier.

Where can I find (new or updated) tests for that method?

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

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java

…Number and use new mantissa API instead of the old

…able name

…hod earlier

… the mantissa size of FPs when parsing FP types from strings

…ead of calculating it by hand each time

…ize()

…or() method

baierd · 2025-09-07T11:02:05Z

too many open questions.

The whole PR never ever mentions once that the SMTLIB definition could be found online: https://smt-lib.org/theories-FloatingPoint.shtml

Sorry 😅, i assumed you guys know. My bad.

…ons as sign bit to "hidden" bit

…to FP sizes and the hidden bit

…LIB2String()

… there are 2 possible replacements and the user should decide which fits best

…stead of a const BV

…ng the solver to check equality instead of equals()

… them so that we can remove them from the public API

… as we don't want to use the deprecated public API

baierd · 2025-09-12T10:15:24Z

Just for clarification: we're returning 23 because we don't include the hidden bit in the significand size. Here hidden bit refers to the first digit of the significand, which is dropped from the floating point representation. So, for instance, instead of 1.100111*2^-3 only .100111*2^-3 will be written out. This saves precious space and the hidden bit can always be restored by looking at the exponent.
Some of the new names here suggest to me that the sign bit was missing from the old size. This is a bit unfortunate, as the sign is never included in the size of the significand. It just happends to have the same size (= 1) as the hidden bit, so the math works out. However, these are really different concepts, and I think we should be careful to not add any more confusion for the users
Maybe we could still find some better names?

Ha, this is true. One should have really looked into the SMTLIB standard before doing all this work:
 :notes
 "eb defines the number of bits in the exponent;
  sb defines the number of bits in the significand, *including* the hidden bit.
 " 
So all cases of "with(out)SignBit" need to be renamed to "with(out)HiddenBit". And for getTotalSize() we might need to rediscuss the name.

I renamed all API referencing the sign bit to reference the hidden bit instead.

The total size is easier in my opinion, as the total size always includes the hidden bit.

baierd · 2025-09-12T10:16:17Z

too many open questions.

The whole PR never ever mentions once that the SMTLIB definition could be found online: https://smt-lib.org/theories-FloatingPoint.shtml

I updated the PR text with all the changes and added the reference.

PhilippWendler · 2025-09-12T10:19:36Z

And for getTotalSize() we might need to rediscuss the name.

The total size is easier in my opinion, as the total size always includes the hidden bit.

No, it doesn't. If we want getTotalSize() to return 32 for single precision, then the total size includes exponent size + mantissa size without hidden bit + sign bit (the current code for this is wrong because it misses the sign bit, it just happens to compute the same result).

…lculation explicit in the code

baierd · 2025-09-12T10:51:13Z

And for getTotalSize() we might need to rediscuss the name.

The total size is easier in my opinion, as the total size always includes the hidden bit.

No, it doesn't. If we want getTotalSize() to return 32 for single precision, then the total size includes exponent size + mantissa size without hidden bit + sign bit (the current code for this is wrong because it misses the sign bit, it just happens to compute the same result).

Fair point, the description was wrong! I fixed the JavaDoc in both getTotalSize() calls and made it more explicit in the code. I need to check whether we have more incorrect references to the components of the total size though.

Still, i would argue that we need to rename getTotalSize() because of this?

PhilippWendler · 2025-09-12T11:07:49Z

Still, i would argue that we need to rename getTotalSize() because of this?

If all other methods that do not include the hidden bit are called ...WithoutHiddenBit, and then we have a method called getTotalSize(), wouldn't you assume that "total" includes everything, i.e., also the hidden bit? At least I thought it should be considered.

baierd · 2025-09-12T17:58:50Z

Still, i would argue that we need to rename getTotalSize() because of this?

If all other methods that do not include the hidden bit are called ...WithoutHiddenBit, and then we have a method called getTotalSize(), wouldn't you assume that "total" includes everything, i.e., also the hidden bit? At least I thought it should be considered.

That is a fair point!
@kfriedberger what do you think?

kfriedberger · 2025-09-12T18:32:12Z

I agree with Philipp and would also assume that totalSize covers all three components, i.e., exponent, mantissa, and sign bit.

baierd · 2025-09-12T19:42:33Z

I agree with Philipp and would also assume that totalSize covers all three components, i.e., exponent, mantissa, and sign bit.

I see it the same way, but would you rename getTotalSize()?

PhilippWendler · 2025-09-15T06:26:22Z

I agree with Philipp and would also assume that totalSize covers all three components, i.e., exponent, mantissa, and sign bit.

Nobody has argued against this. The current question is what should the relation between getTotalSize() and the hidden mantissa bit be, in particular whether the method should be renamed because it does count in the hidden bit.

PhilippWendler

It seems there were some mistakes introduced in the change from "sign bit" to "hidden bit". I am not sure whether I found all, somebody else should also review everything in detail.

PhilippWendler · 2025-09-15T06:32:01Z

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FloatingPointFormulaManager.java

+    int mantissaSizeWithoutHiddenBit = pTargetType.getMantissaSizeWithoutHiddenBit();
    int size = pTargetType.getTotalSize();
-    assert size == mantissaSize + exponentSize + 1;
+    // total size = mantissa without hidden bit + hidden bit + exponent


Suggested change

// total size = mantissa without hidden bit + hidden bit + exponent

// total size = mantissa without hidden bit + size bit + exponent

PhilippWendler · 2025-09-15T06:34:48Z

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractNativeApiTest.java

+    assertThat(msat_get_bv_type_size(env, msat_term_get_type(bvNumber))).isEqualTo(totalBVSize);
+
+    int exponent = 8;
+    int mantissaWithoutSign = 23; // excluding hidden bit


Outdated name.

PhilippWendler · 2025-09-15T06:36:07Z

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java

    int expWidth = Integer.parseInt(matcher.group(2));
-    int mantWidth = Integer.parseInt(matcher.group(3));
+    // The term representation in MathSAT5 does not include the hidden bit
+    int mantWidthWithoutSignBit = Integer.parseInt(matcher.group(3));


Outdated name.

PhilippWendler · 2025-09-15T06:41:51Z

src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java

    final long signSort = getFormulaCreator().getBitvectorType(1);
    final long expoSort = getFormulaCreator().getBitvectorType(type.getExponentSize());
-    final long mantSort = getFormulaCreator().getBitvectorType(type.getMantissaSize());
+    final long mantSort =


Does Z3's mkFpaFp expect the mantissa to be passed with our without hidden bit? If the former, the bitvector below is also created incorrectly.

PhilippWendler · 2025-09-15T07:17:52Z

src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java

          mant,
          pType.getExponentSize(),
-          pType.getMantissaSize());
+          pType.getMantissaSizeWithSignBit());


Even with the current changes, this is still a behavioral change, and it is unclear whether it is a bug fix or breaks something.

I think all changes in Z3FormulaCreator need to be checked carefully against the Z3 docs to make sure that they really match.

PhilippWendler · 2025-09-15T07:28:09Z

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

+   * format, according to the given type. The sum of the sizes of exponent and mantissa (including
+   * the hidden bit) of the target type needs to be equal to the size of the bitvector.


This is wrong, right? It needs to refer to the sign bit, but exclude the hidden bit.

PhilippWendler · 2025-09-15T07:28:24Z

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

   * Create a formula that produces a representation of the given floating-point value as a
   * bitvector conforming to the IEEE format. The size of the resulting bitvector is the sum of the
-   * sizes of the exponent and mantissa of the input formula plus 1 (for the sign bit).
+   * sizes of the exponent and mantissa (including the hidden bit) of the input formula.


Same as above.

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

PhilippWendler · 2025-09-15T07:30:31Z

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

  /**
   * Returns true if this floating-point number is an IEEE-754-2008 single precision type with 32
-   * bits length consisting of an 8 bit exponent, a 23 bit mantissa and a single sign bit.
+   * bits length consisting of an 8 bit exponent, a 24 bit mantissa (including the hidden bit).


The sentence is grammatically wrong now, and it misses the sign bit.

PhilippWendler · 2025-09-15T07:31:05Z

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

  /**
   * Returns true if this floating-point number is an IEEE-754-2008 double precision type with 64
-   * bits length consisting of an 11 bit exponent, a 52 bit mantissa and a single sign bit.
+   * bits length consisting of an 11 bit exponent, a 53 bit mantissa (including the hidden bit).


Same as above.

kfriedberger · 2025-09-20T09:26:19Z

I agree with Philipp and would also assume that totalSize covers all three components, i.e., exponent, mantissa, and sign bit.

Nobody has argued against this. The current question is what should the relation between getTotalSize() and the hidden mantissa bit be, in particular whether the method should be renamed because it does count in the hidden bit.

A user might prefer shorter significant names, ... so getTotalSize() is sufficient and does not need a renaming.

…as it is used when constructing Co-authored-by: Philipp Wendler <[email protected]>

…t users explicitly have to choose one of the 2 successor methods

…() for CVC4/5 to reflect what we do in the method better

BaierD added 12 commits September 2, 2025 09:59

Add native Mathsat test for mantissa not including the sign bit with …

f99f39c

…BV transformation and width comparison

Add note about mantissa und sign bit in FloatingPointNumber.java

737718c

Add JavaDoc to FormulaType.FloatingPointType and add methods to get t…

d50ad4c

…he type/mantissa with/without sign bit and add sign bit to toString and toSMTLIBString representations

Add JavaDoc to FloatingPointNumber and add methods to get the mantiss…

a4240e6

…a with/without sign bit and use those as far as possible to make the code unambiguous for mantissas

Extend FP tests with new mantissa API to be unambiguous about the sig…

c452a8f

…n bit and add some assertions for mantissa/exponent

Update Bitwuzla with new unambiguous FP mantissa size getters

a6f92b7

Update CVC4 with new unambiguous FP mantissa size getters

ca4a3f7

Update CVC5 with new unambiguous FP mantissa size getters

7bed3f5

Update MathSAT5 with new unambiguous FP mantissa size getters

73c1451

Update Z3 with new unambiguous FP mantissa size getters

1ca40f9

Update SolverVisitorTest with new unambiguous FP mantissa size getters

6d80321

Fix off-by-one FP mantissa bug when casting BV to FP

44310e0

baierd self-assigned this Sep 2, 2025

Remove changes left over from PR 512 (to be added back with PR 512!)

475ce68

baierd mentioned this pull request Sep 2, 2025

Add IEEE-754 Floating Point to Bitvector Conversion Fallback #512

Open

Fix bug in test using the wrong mantissa size for an FP

bb3760d

baierd requested a review from kfriedberger September 2, 2025 09:00

BaierD added 2 commits September 2, 2025 13:27

Apply checkstyle naming/grammar suggestions

31b0b38

Fix off-by-one error for mantissa for getFloatingPointTypeWithSignBit()

4b07b9b

PhilippWendler requested changes Sep 2, 2025

View reviewed changes

BaierD added 7 commits September 2, 2025 13:42

Update naming of mantissa arguments in constructors for FloatingPoint…

e444b52

…Number and use new mantissa API instead of the old

Fix accidentally added off-by-one bug in CVC4 when building FPs

f1ff09f

Use new FP mantissa getter in CVC4 and remove magic -1 + improve vari…

eddaf77

…able name

Unify constructors of FloatingPointType by delegating to the same met…

1dae5d1

…hod earlier

Use the SMTLIB2 standards interpretation of including the sign bit in…

7755fe6

… the mantissa size of FPs when parsing FP types from strings

Add method for total type size in FloatingPointNumber and use it inst…

83cd136

…ead of calculating it by hand each time

Rename method for total type size in FloatingPointNumber to getTotalS…

96a2565

…ize()

BaierD added 2 commits September 5, 2025 18:11

Use the correct getter for mantissas in Z3FormulaCreator for FPs

1aba81d

Split BV to FP to BV tests and remove solverSupportsNativeFPToBitvect…

dd83ed4

…or() method

BaierD added 10 commits September 7, 2025 14:54

Update all names referencing the hidden bit in Floating-Point precisi…

c83f96f

…ons as sign bit to "hidden" bit

Revert some changes back to sign bit that were accidentally changed

e8f44d8

Improve some JavaDoc in FloatingPointFormulaManager.java in relation …

00dc033

…to FP sizes and the hidden bit

Add tests for FP type (precision) toString(), fromString(), and toSMT…

20a8f48

…LIB2String()

Remove @InlineMe annotation for deprecated call getMantissaSize(), as…

6769850

… there are 2 possible replacements and the user should decide which fits best

Remove @InlineMe annotation for deprecated call getMantissaSize(), as…

015c145

… there are 2 possible replacements and the user should decide which fits best

Disable parts of FP to IEEE BV tests for Z3, as it returns a query in…

9aff78a

…stead of a const BV

Enable FP to IEEE BV precision tests for Z3 and Bitwuzla fully by usi…

ddac078

…ng the solver to check equality instead of equals()

Re-add removed FP single/double mantissa size constants and deprecate…

52d6e30

… them so that we can remove them from the public API

Add FP single/double precision sizes to FloatingPointNumberTest.java,…

5dd10ca

… as we don't want to use the deprecated public API

Fix incorrect JavaDoc for FP precision total size API and make the ca…

e08a75a

…lculation explicit in the code

PhilippWendler requested changes Sep 15, 2025

View reviewed changes

baierd and others added 5 commits September 22, 2025 13:48

Explicitly name sign bit in FloatingPointNumber constructor JavaDoc, …

bd8c6bd

…as it is used when constructing Co-authored-by: Philipp Wendler <[email protected]>

Remove @InlineMe from deprecated method getFloatingPointType() so tha…

55901fc

…t users explicitly have to choose one of the 2 successor methods

Rename wrongly named variable in Mathsat5 FP impl

b835125

Rename wrongly named variable in CVC4 FP impl

056ca12

Change comment about total FP precision size in fromIeeeBitvectorImpl…

234452d

…() for CVC4/5 to reflect what we do in the method better

	// total size = mantissa without hidden bit + hidden bit + exponent
	// total size = mantissa without hidden bit + size bit + exponent

		* format, according to the given type. The sum of the sizes of exponent and mantissa (including
		* the hidden bit) of the target type needs to be equal to the size of the bitvector.

Fix Floating-Point Mantissa Not Including Sign Bit #513

Are you sure you want to change the base?

Fix Floating-Point Mantissa Not Including Sign Bit #513

Uh oh!

Conversation

baierd commented Sep 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

PhilippWendler commented Sep 2, 2025

Uh oh!

baierd commented Sep 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

PhilippWendler commented Sep 2, 2025

Uh oh!

PhilippWendler left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

baierd commented Sep 7, 2025

Uh oh!

baierd commented Sep 12, 2025

Uh oh!

baierd commented Sep 12, 2025

Uh oh!

PhilippWendler commented Sep 12, 2025

Uh oh!

baierd commented Sep 12, 2025

Uh oh!

PhilippWendler commented Sep 12, 2025

Uh oh!

baierd commented Sep 12, 2025

Uh oh!

kfriedberger commented Sep 12, 2025

Uh oh!

baierd commented Sep 12, 2025

Uh oh!

PhilippWendler commented Sep 15, 2025

Uh oh!

PhilippWendler left a comment

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!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kfriedberger commented Sep 20, 2025

baierd commented Sep 2, 2025 •

edited

Loading

baierd commented Sep 2, 2025 •

edited

Loading