Add IEEE-754 Floating Point to Bitvector Conversion Fallback

[baierd]

This PR adds a fallback method for FloatingPointManager.toIeeeBitvector(FloatingPointFormula):

• FloatingPointManager.toIeeeBitvector(FloatingPointFormula, BitvectorFormula), returns a BooleanFormula that is the result of the equality of the FP input with the BV input (BV is equal to the floating-points bit representation according to the IEEE 754-2008 floating-point format). Special FP numbers are returned as the solver sees fit.

Tests for this method have been added. This includes the SMTLIB2 output of it, and the native toIeeeBitvector() method, showing us what solver can parse what output.

Furthermore, i added common FP type checks in the wrapping function of AbstractFloatingPointFormulaManager

[baierd]

@kfriedberger the SMTLIB2 standard defines the size of an FP as mantissa + exponent with the mantissa including the sign bit. Our current implementation excludes it, and we do not document this properly in all cases, especially the FP type constructor.

This is problematic, as the standard defines the size of a BV representation of a FP as mantissa + exponent, which is off by 1 in our returned values (this is how i noticed btw.).

My proposal (already WIP):

• 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.
• Announce the FP type constructor to be deprecated in the near future due to this.
• Add new constructors for FP type that specify the inclusion in the method name.
• Add methods to get the sizes of mantissa and exponent to FloatingPointFormulaManager based on the solvers terms instead of our types (similar to what we do for BV width), allowing assertions and checking the solvers interpretation for our type.

I don't want to change the current FP-Type constructor, as users expect this to not change behavior.

What do you think? I am happy about thoughts/ideas.

Edit: it would probably be a good idea to also update the API for getMantissaSize() to getMantissaSizeWithSignBit() and getMantissaSizeWithoutSignBit() and deprecate the old method.

[baierd]

@kfriedberger @PhilippWendler i now removed the 2 toIeeeBitvector() fallback methods that you reviewed, and moved to a single one that simply takes a BitvectorFormula and returns the BooleanFormula representing the FP = BV equality.

[PhilippWendler]

The expression getFormulaCreator().getFormulaType(pTerm) is evaluated up to four times on every wrap call. Why not refactor it out into a variable?

Furthermore, checking whether the type is a floating-point type if we check equals() later on anyway is redundant. So I would recommend to execute only one of these checks.

Then the method becomes basically if ... check1 else check2. Now it is useless to delegate from wrapFloatingPoint to wrapFloatingPointAndAssertType. So just put a single check into each of these two methods - much simpler than now.

[baierd]

Good points! I incorporated them. Thank you!

I originally wanted to switch to using "assert" one we ran all tests and confirmed that we use the API as expected. We might still do that. @kfriedberger whats your opinion on this?

[PhilippWendler]

I just noticed the following: It seems one can use the currently proposed method symmetrically, both for converting from a float to a bitvector and vice versa. After all it creates only an equality between a bv and a float, so I could use it to create an equality between a bitvector constant and a nondet float variable, right?

That would mean that the name toIeeeBitvector is bad because it specifies only one direction and instead the name should indicate the mentioned equality between a float and its bitvector representation. That would also eliminate the awkward bitvectorFormulaSetToBeEqualToFpNumber parameter name.

Then the method should also be referenced in the JavaDoc of the current inverse of toIeeeBitvector.

Btw.: Are there tests for something like I mentioned above?

[PhilippWendler]

First, there are no "returned values" here. Second, if behavior is simply mentioned as "not defined" it means that probably almost no caller can safely use it without wrapping it in lots of ITEs, creating a trap in the API. After all, the best way to do something should also be the easiest way.

But I suspect that "not defined" is not really true and one can rely on some behavior rules, just that these are more vague than for other operations, right? What are these rules?

For example, can I rely on the fact that if the float is a NaN that there is at least one bv value that is determined as equal to it? And that no bv value that has a defined float representation could compare as equal to a NaN value?

[baierd]

But I suspect that "not defined" is not really true and one can rely on some behavior rules, just that these are more vague than for other operations, right? What are these rules?

SMTLIB2 applies. Meaning that, from the point of view of SMTLIB2, there is only one NaN etc. The solvers do accept all valid NaN BV representations when transforming from BV to FP as NaN. But they return just one canonical FP NaN representation per default. I added a test for this.
If a user wants custom behavior for special values, it has to be added by the user uniformly over all FPs. (When i realized that, i removed the version of this method that had the ability to add FP number mappings ;D )

Btw. i checked the default BV representations of NaN in all solvers. Some examples:
MathSAT5: 0 11111111 10000000000000000000000
Z3: 0 11111111 00000000000000000000001
Bitwuzla: 0 11111111 11111111111111111111111
CVC5: 1 11111111 11111111111111111111111

[baierd]

For example, can I rely on the fact that if the float is a NaN that there is at least one bv value that is determined as equal to it? And that no bv value that has a defined float representation could compare as equal to a NaN value?

All BV NaN representations seem to work as NaN. When transformed to FP, they are canonized. They do not compare equal as FPs.

Fun fact: no SMT solver returns the same bit representation for NaN as bitvector that is used in the floating-point number when transforming via toIeeeBitvector().

[PhilippWendler]

Now the JavaDoc just says "Behavior for special FP values (NaN, Inf, etc.), is solver dependent." Wasn't there an explanation about how to handle this at some point, i.e., the hint to handle special values manually by adding conditions?

[baierd]

Yes, but everyone working with SMT should know how to do this. It might even be dangerous to mention it here; if they don't also modify other sources of BV/FP constants/conversions, unexpected behavior might ensue.

If we knew enough about how these things work or the details, i would be in favor of providing this information. Currently, i don't think that we have the full picture.