Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Incomplete FP support #24

Open
CaelmBleidd opened this issue Sep 5, 2022 · 0 comments
Open

Incomplete FP support #24

CaelmBleidd opened this issue Sep 5, 2022 · 0 comments
Assignees

Comments

@CaelmBleidd
Copy link
Member

CaelmBleidd commented Sep 5, 2022

For now, there are a few severe drawbacks in the FP implementation:

  1. 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.
  2. There is no overload for fp creation from int value
  3. There are no tests for mkFp(BV, BV, BV)
  4. Multiple bugs in custom size FP: some combinations don't work, choose masks carefully for tests, add limits and checks in the constructors
  5. Operation implemented as part of the KFpValue: isNaN, isInfinity, isNormal, etc.
  6. Add support for the FP in Bitwuzla
  7. Replace Long values in KFpDecl with Bv
  8. KFp128 should have BV instead of long values for its significand
  9. Replace numbers with bit-vectors where it's possible (for example, in creation, in the internal storage, etc.)
  10. Additional tests for operations (along with extra methods, like fpToFp)
  11. Documentations for implemented classes and methods
@CaelmBleidd CaelmBleidd self-assigned this Sep 5, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant