[Haskell-cafe] [ANN] New release of SBV (v7.0), now with incremental solving

Levent Erkok erkokl at gmail.com
Thu Jul 20 08:10:17 UTC 2017


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

This release adds incremental solving capabilities to SBV: Users can now
interact with the underlying solver using a typed API capturing the SMTLib
language, issuing commands, getting model values, and asserting further
constraints on-the-fly. The possibility of issuing multiple check-sat
commands allows incremental assertion of facts, a key feature of modern
constraint solving systems.

  Hackage: https://hackage.haskell.org/package/sbv
  Homepage: http://leventerkok.github.io/sbv/
  Release notes: https://github.com/LeventErkok/sbv/blob/master/CHANGES.md
  SMTLib initiative: http://smtlib.cs.uiowa.edu/

Feedback and bug reports are most welcome!

-Levent.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170720/d3f2c1a6/attachment.html>


More information about the Haskell-Cafe mailing list