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]

the naming is not optimal: toIEEEBitvector(fp, bv) should be renamed to equal/bitsEqual/bitwiseEqual(fp, bv), because this is the exact meaning: assignment/equality of bits and a symmetrical nature. The parameter name is ugly, too.

I chose toIEEEBitvector(fp, bv) as the SMTLIB2 standard defines this new implementation as the canonical way of implementing the functionality that we offer with the method toIEEEBitvector(fp). I would argue that changing the name could lead to users not understanding that this offers the same functionality.

Note: It returns a BooleanFormula only because the standard defines it that way. We could theoretically switch the bitvector and bool, such that a BitvectorFormula is returned, and a BooleanFormula is needed as argument. Alternativly: we can always just return a tuple of <BitvectorFormula, BooleanFormula>.

If it works for special cases like NaN, Inf, Subnormal, etc, then fine for me.

It works due to SMTLIB(2) only defining each special FP number only once. Hence "all" bitvector NaN representations return the "same" NaN (as defined by SMTLIB2). If translated back, the original bitvector is returned. I added tests for all special FP numbers that check this.

[PhilippWendler]

I agree that the current name is bad as mentioned in #512 (comment).

[PhilippWendler]

I had a look over the API, but no in-depth review.