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 total order comparison for arbitrary floating point #703

Closed lsrcz closed 2 months ago

lsrcz commented 2 months ago

This pull request fixes the total order comparison for arbitrary floating-point numbers and resolves issue #702.

For arbFPIsEqualObjectH, the bfIsInf clause has been removed because the == operator for BitFloat can handle the comparison correctly.

For arbFPCompareObjectH, the bfCompare function from libBF is used. This function provides a total order that differentiates between +0 and -0, while treating all NaN values as equal.