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=2.3 required=5.0 tests=AWL,DNS_FROM_RFC_POST, MISSING_HEADERS,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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id C27CCBBAF for ; Sun, 8 Mar 2009 20:51:27 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8EAEe+s0nRVZK1lGdsb2JhbACMaQgDhxlePwEBAQEJCQoJD65vMIUIiEgBAwEDhAIGhSI X-IronPort-AV: E=Sophos;i="4.38,325,1233529200"; d="scan'208";a="22225556" Received: from wa-out-1112.google.com ([209.85.146.181]) by mail2-smtp-roc.national.inria.fr with ESMTP; 08 Mar 2009 20:51:27 +0100 Received: by wa-out-1112.google.com with SMTP id k34so1010165wah.27 for ; Sun, 08 Mar 2009 12:51:25 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:sender:received:in-reply-to :references:date:x-google-sender-auth:message-id:subject:from:cc :content-type:content-transfer-encoding; bh=44l1gjJyAb7EkFLZ7s+vX6di1XTono2dIfY6z2xlab0=; b=iJWAms4AV4CnHjvlfZI1tsQ0xjwb6XqO29lRnq/fHR5dojycSOU45iJacnWAAX3q+F Uq0ZE8kYVE+WegEMlzI6ZWW3NRMdvwAx3Y7EzFkhmQz63SlrH/gupguWvK4zSDd+PeAQ fKc4WNoX3a62SwNI4C2P4HYfSLfbmsTC4GFIU= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:cc:content-type :content-transfer-encoding; b=Q9VkgH8tpFHK28J6hgO0SjCTB9p54iWvl0uSfoV+vBTIb8eNfd4b/iVmqVOwwNgJuy fPVJicU8ur+ISkMkih8r91mDz3OMACGCUojQ2vXLnuTdPwpqYAdjodNbe8O5bVhKP7bC i5Yhbmv9Yv+XXB6VH8xhd/Su7a8YZX8xxpmV8= MIME-Version: 1.0 Sender: peter.hawkins@gmail.com Received: by 10.114.195.19 with SMTP id s19mr3037411waf.10.1236541885938; Sun, 08 Mar 2009 12:51:25 -0700 (PDT) In-Reply-To: <1bd843010903081213j5d3e4581p9ff192eda3396f79@mail.gmail.com> References: <1bd843010903081213j5d3e4581p9ff192eda3396f79@mail.gmail.com> Date: Sun, 8 Mar 2009 12:51:25 -0700 X-Google-Sender-Auth: 272bdb97137c3422 Message-ID: Subject: Re: [Caml-list] Using OCaml with SMT solvers From: Peter Hawkins Cc: caml-list@yquem.inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; ocaml:01 smt:01 solvers:01 vectors:01 arrays:01 ocaml:01 solver:01 solver:01 cheers:01 smt:01 beginner's:01 bug:01 2009:98 beginners:01 parsing:01 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 : > Hello, > > =A0 I don't know if this is the right place to ask this question, but wha= t is > the best way of using an SMT solver with an OCaml interface on Linux? > > =A0 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! =A0Think 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 > >