Suggested improvements for API related to floats

[PhilippWendler]

While using the API related to the floating-point theory in CPAchecker, we noticed several things that should be improved.

Boolean named "sign"

At least FloatingPointFormulaManager.makeNumber(BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type), FloatingPointNumber.of(boolean sign, BigInteger exponent, BigInteger mantissa, int exponentSize, int mantissaSize), and FloatingPointNumber.getSign() use a boolean named "sign". Out of these three places, only the latter documents whether true means positive or negative. Of course, the documentation should be completed such that this is documented everywhere.

However, in general I consider a boolean named "sign" to not be a good API, because it is not obvious what it means and it is too easy to make mistakes. Even already now we have proof for that: A developer who is highly experienced with both floats and JavaSMT made a mistake and mixed up the meaning of this boolean. If they did this, all other developers are even more likely to do so. So I would recommend to get rid of the name "sign" for a boolean in the public API completely. For the factory methods, it is unfortunately still easy to make a mistake even if the parameter is renamed, but at least it is better than now. For FloatingPointNumber.getSign() I recommend to expose isNegative() (and maybe isPositive()) instead and make getSign() @Deprecated.

makeNumber(FloatingPointNumber)

The interface FloatingPointFormulaManager is clearly missing a makeNumber(FloatingPointNumber) method. Either this method can delegate to makeNumber(BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type) or vice versa in AbstractFloatingPointFormulaManager, so solver implementations even do not need more effort to provide it.

Missing documentation of technicalities

There are some technical details about how floats are represented, e.g., whether the exponent is stored with or without bias, whether the significant has the hidden bit or not, and maybe more (I am not an expert in this area). None of the related JavaSMT methods documents which of these apply. This should be added, and (similar to the "sign" bit case) one should consider to make the APIs less error prone by for example moving this information into the name of methods and/or exposing less such difficult-to-use APIs publicly. Relevant are at least:

• FloatingPointFormulaManager.makeNumber(BigInteger exponent, BigInteger mantissa, boolean signBit, FloatingPointType type)
• FloatingPointNumber.of(boolean sign, BigInteger exponent, BigInteger mantissa, int exponentSize, int mantissaSize)
• FloatingPointNumber.getExponent() and FloatingPointNumber.getMantissa()
• FloatingPointNumber.of(String bits, int exponentSize, int mantissaSize) (which likely uses IEEE754 representation, so it could just document that)

Lack of connection between FloatingPointNumber and FormulaType.FloatingPointType

While browsing through the code it seems surprising that there is no connection between FloatingPointNumber and FormulaType.FloatingPointType and that both of them independently store exponent and mantissa sizes. One might consider letting FloatingPointNumber simply use a FloatingPointType instance instead. This would likely simplify some code in FloatingPointNumber, and potentially make it less tedious to copy around these values for user code as well. It also eliminates all potential bugs where someone mixes up the exponent and mantissa sizes, for example, which is easy because the compiler will not warn about it. (Luckily it seems that JavaSMT seems to always have exponent before mantissa in parameter lists, so it is consistent, but external code might not follow this pattern.)

[PhilippWendler]

Apparently, the documentation for FloatingPointNumber.getSign() is even wrong and the real semantics are the exact opposite. If this is true, it should be fixed ASAP, of course, and it is an even stronger proof of how bad the pattern of naming a boolean "sign" is.

[kfriedberger]

Thank you for reporting the issue related to floating-point (FP) numbers and the sign bit.

The documentation has been updated and improved in commit bef62a7.

The FP theory adheres strictly to the SMT-LIB standard for FP, which is based on IEEE 754. This standard defines the representation and usage of the sign bit, exponent, and mantissa. The initial flag-based implementation for the sign bit was likely sufficient for most users or received limited attention. However, transitioning to an enum-based approach is certainly an option if it would provide better clarity or flexibility.

Regarding the separation of FPNumber and FPType: FPType extends FormulaType, whereas FPNumber is unrelated to Formula. Keeping them distinct avoids unnecessary mixing of concerns, and I would prefer to maintain this separation for better modularity and design clarity.

[kfriedberger]

Boolean named "sign"

-> fixed: "sign" was marked deprecated and is replaced by a proper enum value.

makeNumber(FloatingPointNumber)

-> fixed: new method was added into the API.

Missing documentation of technicalities

-> fixed: documentation was updated and improved.

Lack of connection between FloatingPointNumber and FormulaType.FloatingPointType

-> will not be fixed, because is wanted by design.

[PhilippWendler]

I notice that the information about bias etc. was added only to FloatingPointNumber, not to FloatingPointFormulaManager.makeNumber(). Is this intended?

Your last comment likely has a typo in the last heading and you wanted to write "Lack of connection between FloatingPointNumber and FormulaType.FloatingPointType" there?