[Haskell-cafe] smt solver bindings

[Levent Erkok]

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 transparent to the user.

I'm actively developing and using SBV
(http://github.com/LeventErkok/sbv), so any comments/feedback would be
most welcome. Do let me know if you decide to use it and see any
issues..

-Levent.

On Thu, Dec 15, 2011 at 12:17 PM, Josef Svenningsson
<josef.svenningsson at gmail.com> wrote:
> On Thu, Dec 15, 2011 at 7:04 PM, Dimitrios Vytiniotis
> <dimitris at 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 with the Yices
> backend. If you contact Levent Erkök, the author of sbv, he should be able
> to give you more information.
>
>  https://github.com/LeventErkok/sbv
>
> Thanks,
>
> Josef
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>