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