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.
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Reply via email to