Dimitrios:
The SBV library (http://hackage.haskell.org/package/sbv) can indeed
use Z3 as a backend SBV solver. However, it uses Z3 via SMT-Lib2, not
via it's C-API. It aims to provide a much higher level interface,
integrating with Haskell as smoothly as possible, keeping the
SMT-solver
I've a quick question:
Are there Haskell wrappers for the Z3 C API around?
Thanks!
d-
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Not that I know of, but I would like them too. There are a few bindings to
yices, but I don't think yices has the feature I want in it.
On Thu, Dec 15, 2011 at 1:04 PM, Dimitrios Vytiniotis
dimit...@microsoft.com wrote:
I've a quick question:
Are there Haskell wrappers for the Z3 C API
On Thu, Dec 15, 2011 at 7:04 PM, Dimitrios Vytiniotis
dimit...@microsoft.com wrote:
I've a quick question:
Are there Haskell wrappers for the Z3 C API around?
I believe sbv recently got support for Z3 but I don't know if it uses the
C API. Neither have I tried the Z3 backend, I only played