UnitTestBot / UnitTestBot/ksmt
Incomplete FP support
Open
@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:
- Doesn't work float to double transformation and vise versa:
mkFp(someFloat, sort)andmkFp(someFloat.toDouble(), sortreturn different FP values sincetoDoublechanges 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
Longvalues in KFpDecl withBv - KFp128 should have
BVinstead 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
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.