search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
242 stars 34 forks source link

Data.SBV.Dynamic's versions of division/modulus are not Haskell compliant #495

Closed LeventErkok closed 1 year ago

LeventErkok commented 4 years ago

The following functions:

svDivide, svQuot, svRem, svQuotRem

exported from Data.SBV.Dynamic directly use SMTLib's version of these operations, which are different than Haskell's.

Data.SBV versions of sDiv/sMod etc.; do the "proper" translation, see here:

https://github.com/LeventErkok/sbv/blob/b47ca083096aeda84586d8d7b1e7c777b1b19d09/Data/SBV/Core/Model.hs#L1599-L1656

We should either document this discrepancy in the dynamic interface, or move the "translation" code to the dynamic side so they behave the same.

LeventErkok commented 1 year ago

Actually, this is documented in the functions and probably is the right definition; just gotta be careful!