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

[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

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