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
239 stars 33 forks source link

Fix the Ord instance for FP and FloatingPoint #701

Closed lsrcz closed 2 months ago

lsrcz commented 2 months ago

This pull request fixes the Ord instance for FP and FloatingPoint. The operator (>=) and (<=) will give True when comparing NaNs.

I originally thought that this comes from the underlying libBF library, as I've fixed a bug there yesterday. (https://github.com/GaloisInc/libBF-hs/pull/32). However, after I switch to the fixed version, the bug is still there.

My theory for this bug in the sbv repo is that the instance derived by the compiler may look like this:

a <= b = not $ a > b

And the fix would be manually implementing the operators.

lsrcz commented 2 months ago

I've updated it to throw errors on comparing different precisions.

LeventErkok commented 2 months ago

Great!

I'll make a stylistic change (I don't like otherwise, my pet peeve), and will bump the libBF dependency.