Using OCaml with SMT solvers

Using OCaml with SMT solvers

[Jean Yang]

[-- Attachment #1: Type: text/plain, Size: 392 bytes --]

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.
*^^`

[-- Attachment #2: Type: text/html, Size: 501 bytes --]

Re: [Caml-list] Using OCaml with SMT solvers

[Peter Hawkins]

Hi...

STP is one option (for the quantifier-free theory of finite bit
vectors and arrays). It has an OCaml interface.
http://people.csail.mit.edu/vganesh/STP_files/stp.html

I also have a binding for MONA if that's of interest to anyone.

More generally, have you considered communicating with a solver of
your choice via file I/O (i.e. writing out the query to a file which
you give to the solver, and parsing the solver's output)? You wouldn't
need an ocaml binding for the solver, although you will pay a
performance cost.

Cheers,
Peter


2009/3/8 Jean Yang <jeanyang@csail.mit.edu>:
> 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.
> *^^`
>
> _______________________________________________
> 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
>
>

Re: [Caml-list] Using OCaml with SMT solvers

[Virgile Prevosto]

Hello,

Le dim. 08 mars 2009 15:13:26 CET,
Jean Yang <jeanyang@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

Re: Using OCaml with SMT solvers

[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

Re: Using OCaml with SMT solvers

[Grundy, Jim D]

[-- Attachment #1: Type: text/plain, Size: 430 bytes --]

You might also want to look at the Decision Procedure Toolkit (DPT): http://dpt.sourceforge.net/

DPT is an open source (Apache 2 licensed, source forge hosted) SMT solver implemented in OCaml with good performance.  The current release supports only SAT + EUF, but future releases will soon add integer and rational linear arithmetic - of course, you can always add the theory you want yourself.

Kind regards

Jim Grundy

[-- Attachment #2: Type: text/html, Size: 2607 bytes --]