[Haskell] [ANNOUNCE] New release of SBV (v3.1)

Levent Erkok erkokl at gmail.com
Sat Jul 12 19:49:20 UTC 2014


I'm pleased to announce v3.1 release of SBV, a library for integrating SMT
solvers into Haskell.

This release coincides with GHC 7.8.3: A a prior bug in the 7.8 series
caused SBV to crash under heavy load. GHC 7.8.3 fixes this bug; so if
you're an SBV user, please upgrade to both GHC 7.8.3 and your version of
SBV.

Also new in this release are two oft-requested features:

- Parallel solving capabilities: Using multiple SMT solvers at the same
time to get the fastest result (speed), or get all results (to make sure
they all behave the same way, safety).

- A variant of symbolic if-then-else (called sBranch) that can call the
external solver during simulation before it symbolically simulates "then"
and "else" branches. This is useful for programming with recursive
functions where termination depends on symbolic values.

Full release notes:
https://github.com/LeventErkok/sbv/blob/master/CHANGES.md

SBV web page: http://leventerkok.github.io/sbv/

As usual, bug reports and feedback are most welcome!

-Levent.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell/attachments/20140712/fdc96834/attachment.html>


More information about the Haskell mailing list