[Caml-list] Using OCaml with SMT solvers

[Jean Yang]

Hello,

I don't know if this is the right place to ask this question, but what is
the best way of using an SMT solver with an OCaml interface on Linux?

After a brief search it seems that Z3 is the most popular solver with an
OCaml interface, but unfortunately it only supports Windows.

Thanks,
Jean

--
Jean Yang
http://web.mit.edu/jeanyang/www/
Save us! Think before you print.
*^^`

[Virgile Prevosto]

Hello,

Le dim. 08 mars 2009 15:13:26 CET,
Jean Yang <jean...@csail.mit.edu> a écrit :

> I don't know if this is the right place to ask this question, but
> what is the best way of using an SMT solver with an OCaml interface
> on Linux?
>

alt-ergo (http://alt-ergo.lri.fr) is written in Ocaml. Alternatively,
you may be interested in the why infrastructure to call various
external provers (http://why.lri.fr)

Best regards,
--
E tutto per oggi, a la prossima volta.
Virgile

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Chris Conway]

Jean Yang <jeanyang <at> csail.mit.edu> writes:

>
> Hello,  I don't know if this is the right place to ask this question, but what
is the best way of using an SMT solver with an OCaml interface on Linux?  After
a brief search it seems that Z3 is the most popular solver with an OCaml
interface, but unfortunately it only supports Windows.

I have written an OCaml binding for CVC3. It is available here:
https://code.launchpad.net/~cconway/+junk/cvc3-ocaml

Regards,
Chris