Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Using OCaml with SMT solvers
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Peter Hawkins <hawkinsp@c...>
Subject: Re: [Caml-list] Using OCaml with SMT solvers

STP is one option (for the quantifier-free theory of finite bit
vectors and arrays). It has an OCaml interface.

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.


2009/3/8 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
> Save us!  Think before you print.
> *^^`
> _______________________________________________
> Caml-list mailing list. Subscription management:
> Archives:
> Beginner's list:
> Bug reports: