From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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_FAIL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id D8803BBAF for ; Mon, 9 Mar 2009 00:51:16 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AukCAM32s0lQW+UCe2dsb2JhbACVKgEBFiIErmKEVIhNhAUG X-IronPort-AV: E=Sophos;i="4.38,326,1233529200"; d="scan'208";a="36259007" Received: from main.gmane.org (HELO ciao.gmane.org) ([80.91.229.2]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-SHA; 09 Mar 2009 00:51:16 +0100 Received: from list by ciao.gmane.org with local (Exim 4.43) id 1LgSm4-0005Z1-13 for caml-list@inria.fr; Sun, 08 Mar 2009 23:51:16 +0000 Received: from cpe-72-229-116-34.nyc.res.rr.com ([72.229.116.34]) by main.gmane.org with esmtp (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Sun, 08 Mar 2009 23:51:16 +0000 Received: from cconway by cpe-72-229-116-34.nyc.res.rr.com with local (Gmexim 0.1 (Debian)) id 1AlnuQ-0007hv-00 for ; Sun, 08 Mar 2009 23:51:16 +0000 X-Injected-Via-Gmane: http://gmane.org/ To: caml-list@inria.fr From: Chris Conway Subject: Re: Using OCaml with SMT solvers Date: Sun, 8 Mar 2009 23:51:07 +0000 (UTC) Message-ID: References: <1bd843010903081213j5d3e4581p9ff192eda3396f79@mail.gmail.com> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Complaints-To: usenet@ger.gmane.org X-Gmane-NNTP-Posting-Host: main.gmane.org User-Agent: Loom/3.14 (http://gmane.org/) X-Loom-IP: 72.229.116.34 (Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.0.7) Gecko/2009030422 Ubuntu/8.10 (intrepid) Firefox/3.0.7) Sender: news X-Spam: no; 0.00; ocaml:01 smt:01 solvers:01 smt:01 solver:01 ocaml:01 solver:01 writes:01 binding:02 seems:03 chris:06 chris:06 interface:06 interface:06 linux:07 Jean Yang 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