UnitTestBot / UnitTestBot/ksmt

Incomplete FP support

Open
#24 0 comments 0 reactions 1 assignee View on GitHub

@CaelmBleidd is already working on this.

Since Sep 5, 2022.

Dominant language
Kotlin
Stars
42
Forks
17
PR merge metrics
No merged PRs in 30d

Description

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

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.