Re: [Haskell-cafe] smt solver bindings

2011-12-16 Thread 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.svennings...@gmail.com wrote:
 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 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@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe


___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[Haskell-cafe] smt solver bindings

2011-12-15 Thread Dimitrios Vytiniotis

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


Re: [Haskell-cafe] smt solver bindings

2011-12-15 Thread Daniel Peebles
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 around?

 Thanks!
 d-



 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] smt solver bindings

2011-12-15 Thread Josef Svenningsson
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 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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe