[Haskell-cafe] ANN: Haskell bindings for Z3: package z3 0.3.2 released

[Iago Abal]

I am happy to announce a new version of the z3 package

  http://hackage.haskell.org/package/z3

the (unofficial) Haskell bindings for Microsoft's Z3 theorem prover.

We didn't announce this package before, but we believe that now
it is stable enough to be useful for a broader audience.

These bindings are especially appropriate in the following cases:
* If your program runs lot of queries, and probably would benefit
  from incremental solving. Here the performance benefit w.r.t.
  translating each query to SMT-LIB and calling an external solver
  should be significant.
* If you need to extract interpretations for arrays and functions.
* If you need to access specific Z3 features such as Quantifiers
  or Solvers.

We offer three different interfaces:
* Z3.Base: a low-level interface, it just performs marshalling.
* Z3.Monad: introduces a class MonadZ3 and a concrete monad Z3 that
  does some bookkeeping for you. Most people seem to be using this
  interface.
* Z3.Lang: a high-level interface in the form of an embedded
  language. This interface has been deprecated in the current
  release, we will continue to develop it, but it will be in
  separate package.

The bindings are still incomplete as there are some API functions
that have not been added yet. The infrastructure is there, and adding
support for new API functions is (most of the times) straightforward.
We appreciate that, if you fork the project and add extra functions,
then you send the changes back to us.

These bindings still use the old Z3 API of Z3 3.x versions, but there
is some support for the new API that some people is using
satisfactorily. (Z3 4.0  was released while we were still exploring
the design of the library and we preferred not to switch to the new
API at that time). Full support for the new API should come in the
next release.

Iago
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140327/e044cce8/attachment.html>