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

[Peter Hawkins <hawkinsp@cs.stanford.edu>]

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