Re: Using OCaml with SMT solvers

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 --]

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

[Michael Hicks]

Another option is STP.  It's written in C++ I think, with OCaml binders.

http://people.csail.mit.edu/vganesh/STP_files/stp.html

-Mike

On Mar 9, 2009, at 1:09 AM, Grundy, Jim D wrote:

> 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
> _______________________________________________
> 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: 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

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 --]