sosy-lab
Add IEEE-754 Floating Point to Bitvector Conversion Fallback
This PR adds 2 fallback methods for FloatingPointManager.toIeeeBitvector(FloatingPointFormula):
FloatingPointManager.toIeeeBitvector(FloatingPointFormula, String), returning the BV representation as a new variable with the given name. Special FP numbers are returned as the solver sees fit.FloatingPointManager.toIeeeBitvector(FloatingPointFormula, String, Map<FloatingPointFormula, BitvectorFormula>), returning the BV representation as a new variable with the given name. Special FP numbers can be mapped to expected results, with the default behavior (if no mapping has been added) being like the previous method.
Both return a tuple BitvectorFormulaAndBooleanFormula, representing the bitvector of the input FP number, as well as the additional constraint needed as BooleanFormula. The constraint needs to be added to all assertion stacks that make use of the returned BitvectorFormula.
While implementing i found a problem in our implementation of FloatingPointType. Our returned significant precision is off by one. 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 toSMTLIBString().
The solvers generally expect this to be the case, hence why we had 4 solvers with the code type.getMantissaSize() + 1, and only one solver without the + 1
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.
I added the capability to retrieve the precision from the solver directly, instead of using the JavaSMT type, as this was needed for this implementation. ~~This addition is currently hidden from users, but could be exposed if needed.~~ I exposed this API publicly, as it seems to fit well with getSize() for bitvectors, and offers a type-independent, solver based way of getting the FP sizes.
@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
FloatingPointFormulaManagerbased 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.
Do we want to document the typical returns of solvers for special FP numbers? There are multiple well defined return values for NaN as bitvector for example.
@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()togetMantissaSizeWithSignBit()andgetMantissaSizeWithoutSignBit()and deprecate the old method.
I mostly finished this as proposed. You can take a look. 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.