You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
The text was updated successfully, but these errors were encountered:
For now, there are a few severe drawbacks in the FP implementation:
mkFp(someFloat, sort)
andmkFp(someFloat.toDouble(), sort
return different FP values sincetoDouble
changes the bits. We need to detect it somehow and make fp creation consistent.mkFp(BV, BV, BV)
isNaN
,isInfinity
,isNormal
, etc.Long
values in KFpDecl withBv
BV
instead of long values for its significandfpToFp
)The text was updated successfully, but these errors were encountered: