From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <virgile.prevosto@m4x.org>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: *
X-Spam-Status: No, score=1.0 required=5.0 tests=AWL,SPF_NEUTRAL 
	autolearn=disabled version=3.1.3
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by yquem.inria.fr (Postfix) with ESMTP id 7DB23BBAF
	for <caml-list@yquem.inria.fr>; Sun,  8 Mar 2009 22:34:41 +0100 (CET)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AiMEAKjWs0mBaB4igWdsb2JhbACVKgEBFiK8JAeDfgY
X-IronPort-AV: E=Sophos;i="4.38,325,1233529200"; 
   d="scan'208";a="25250819"
Received: from mx1.polytechnique.org ([129.104.30.34])
  by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 08 Mar 2009 22:34:41 +0100
Received: from gavalla (88-121-10-103.rev.libertysurf.net [88.121.10.103])
	(using TLSv1 with cipher DHE-RSA-AES128-SHA (128/128 bits))
	(No client certificate requested)
	by ssl.polytechnique.org (Postfix) with ESMTP id 7C0C514005267
	for <caml-list@yquem.inria.fr>; Sun,  8 Mar 2009 22:34:40 +0100 (CET)
Date: Sun, 8 Mar 2009 22:34:39 +0100
From: Virgile Prevosto <virgile.prevosto@m4x.org>
To: caml-list@yquem.inria.fr
Subject: Re: [Caml-list] Using OCaml with SMT solvers
Message-ID: <20090308223439.2cbd16b5@gavalla>
In-Reply-To: <1bd843010903081213j5d3e4581p9ff192eda3396f79@mail.gmail.com>
References: <1bd843010903081213j5d3e4581p9ff192eda3396f79@mail.gmail.com>
X-Mailer: Claws Mail 3.7.0 (GTK+ 2.14.7; x86_64-pc-linux-gnu)
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-AV-Checked: ClamAV using ClamSMTP at svoboda.polytechnique.org (Sun Mar  8 22:34:40 2009 +0100 (CET))
X-Org-Mail: virgile.prevosto.1996@polytechnique.org
X-Spam: no; 0.00; ocaml:01 smt:01 solvers:01 smt:01 solver:01 ocaml:01 lri:01 lri:01 2009:98 tutto:98 oggi:98 volta:98 caml-list:01 external:03 provers:05 

Hello,

Le dim. 08 mars 2009 15:13:26 CET,
Jean Yang <jeanyang@csail.mit.edu> a =E9crit :

>   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?
>=20

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)=20

Best regards,
--=20
E tutto per oggi, a la prossima volta.
Virgile