sbv v4.1 Release NotesRelease Date: 2015-03-06 // over 7 years ago
Add support for the ABC solver from Berkeley. Thanks to Adam Foltzer for the required infrastructure! See: http://www.eecs.berkeley.edu/~alanmi/abc/ And Alan Mishchenko for adding infrastructure to ABC to work with SBV.
Upgrade the Boolector connection to use a SMT-Lib2 based interaction. NB. You need at least Boolector 2.0.6 installed!
Tracking changes in the SMT-Lib floating-point theory. If you are using symbolic floating-point types (i.e., SFloat and SDouble), then you should upgrade to this version and also get a very latest (unstable) Z3 release. See http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml for details.
Introduce a new class, 'RoundingFloat', which supports floating-point operations with arbitrary rounding-modes. Note that Haskell only allows RoundNearestTiesToAway, but with SBV, we get all 5 IEEE754 rounding-modes and all the basic operations ('fpAdd', 'fpMul', 'fpDiv', etc.) with these modes.
Allow Floating-Point RoundingMode to be symbolic as well
Improve the example
Data/SBV/Examples/Misc/Floating.hsto include rounding-mode based addition example.
Changes required to make SBV compile with GHC 7.10; mostly around instance NFData declarations. Thanks to Iavor Diatchki for the patch.
Export a few extra symbols from the Internals module (mainly for Cryptol usage.)