For now, there are a few severe drawbacks in the FP implementation:
- Doesn't work float to double transformation and vise versa:
mkFp(someFloat, sort) and mkFp(someFloat.toDouble(), sort return different FP values since toDouble changes the bits. We need to detect it somehow and make fp creation consistent.
- There is no overload for fp creation from int value
- There are no tests for
mkFp(BV, BV, BV)
- Multiple bugs in custom size FP: some combinations don't work, choose masks carefully for tests, add limits and checks in the constructors
- Operation implemented as part of the KFpValue:
isNaN, isInfinity, isNormal, etc.
- Add support for the FP in Bitwuzla
- Replace
Long values in KFpDecl with Bv
- KFp128 should have
BV instead of long values for its significand
- Replace numbers with bit-vectors where it's possible (for example, in creation, in the internal storage, etc.)
- Additional tests for operations (along with extra methods, like
fpToFp)
- Documentations for implemented classes and methods
For now, there are a few severe drawbacks in the FP implementation:
mkFp(someFloat, sort)andmkFp(someFloat.toDouble(), sortreturn different FP values sincetoDoublechanges the bits. We need to detect it somehow and make fp creation consistent.mkFp(BV, BV, BV)isNaN,isInfinity,isNormal, etc.Longvalues in KFpDecl withBvBVinstead of long values for its significandfpToFp)