[Haskell-cafe] ANN: Haskell bindings for Z3: package z3 0.3.2 released
iago.abal at gmail.com
Thu Mar 27 10:18:16 UTC 2014
I am happy to announce a new version of the z3 package
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
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
* 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
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 part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe