From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <jean.yang.writeme@gmail.com>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: **
X-Spam-Status: No, score=2.8 required=5.0 tests=DNS_FROM_RFC_POST,
	HTML_MESSAGE,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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105])
	by yquem.inria.fr (Postfix) with ESMTP id 488D8BBAF
	for <caml-list@yquem.inria.fr>; Sun,  8 Mar 2009 20:13:28 +0100 (CET)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Ar0CACO1s0lKfSwck2dsb2JhbACCIDGKI4d3PwEBAQEJCQoJEQOvMzCFEIhIAQMBA4QCBoUi
X-IronPort-AV: E=Sophos;i="4.38,325,1233529200"; 
   d="scan'208";a="36254499"
Received: from yx-out-2324.google.com ([74.125.44.28])
  by mail4-smtp-sop.national.inria.fr with ESMTP; 08 Mar 2009 20:13:27 +0100
Received: by yx-out-2324.google.com with SMTP id 31so601439yxl.3
        for <caml-list@yquem.inria.fr>; Sun, 08 Mar 2009 12:13:26 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=gamma;
        h=domainkey-signature:mime-version:sender:received:date
         :x-google-sender-auth:message-id:subject:from:to:content-type;
        bh=nrlbXlkmerhcMwS7szyYyQydQ5zlbEe3oozst9njaok=;
        b=MgbLaa3P7c/6iZiEW7V1ojFDBY6CokYcmER4o4inV0yeIoNCy0V5X5ZzRwtAjPVMj3
         oxaeq2D065DyPuymjGCITbHoBEzUA5aX5bB18eofblolLpiwakcD010nk+kd1QRfLGBh
         9r6CJ+xVDlNNBbf2NnwxEWW8gAsJqyc4hgc+0=
DomainKey-Signature: a=rsa-sha1; c=nofws;
        d=gmail.com; s=gamma;
        h=mime-version:sender:date:x-google-sender-auth:message-id:subject
         :from:to:content-type;
        b=mUxDrsVQLU4kI75URBuoIIkAdmOeUmyjAihBuBU99rxqWeYMg1reKlNMQQ3bCfYLaQ
         e0WicJgjD5QZxPjAL4EkQUcH7jLBk+KSs3utHoe1Nsz8tvxwfY4nzYCYbz42WjAcXdNr
         IG6+9XBA0gLSIRR3BcpiV0P3IvrjUzLqOaPpk=
MIME-Version: 1.0
Sender: jean.yang.writeme@gmail.com
Received: by 10.100.125.14 with SMTP id x14mr3118662anc.66.1236539606847; Sun, 
	08 Mar 2009 12:13:26 -0700 (PDT)
Date: Sun, 8 Mar 2009 15:13:26 -0400
X-Google-Sender-Auth: b65213a5b595698b
Message-ID: <1bd843010903081213j5d3e4581p9ff192eda3396f79@mail.gmail.com>
Subject: Using OCaml with SMT solvers
From: Jean Yang <jeanyang@csail.mit.edu>
To: caml-list@yquem.inria.fr
Content-Type: multipart/alternative; boundary=0016e645b9b404510d0464a0508b
X-Spam: no; 0.00; ocaml:01 smt:01 solvers:01 smt:01 solver:01 ocaml:01 solver:01 seems:03 seems:03 interface:06 interface:06 linux:07 linux:07 think:13 think:13 

--0016e645b9b404510d0464a0508b
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit

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.
*^^`

--0016e645b9b404510d0464a0508b
Content-Type: text/html; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable

Hello,<br><br>=A0 I don&#39;t know if this is the right place to ask this q=
uestion, but what is the best way of using an SMT solver with an OCaml inte=
rface on Linux?<br><br>=A0 After a brief search it seems that Z3 is the mos=
t popular solver with an OCaml interface, but unfortunately it only support=
s Windows.<br>
<br>Thanks,<br>Jean<br clear=3D"all"><br>-- <br>Jean Yang<br><a href=3D"htt=
p://web.mit.edu/jeanyang/www/">http://web.mit.edu/jeanyang/www/</a><br>Save=
 us! =A0Think before you print.<br>*^^`<br>

--0016e645b9b404510d0464a0508b--


From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <gclci-caml-list@m.gmane.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_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 <caml-list@yquem.inria.fr>; 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 <caml-list@inria.fr>; 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 <caml-list@inria.fr>; Sun, 08 Mar 2009 23:51:16 +0000
X-Injected-Via-Gmane: http://gmane.org/
To: caml-list@inria.fr
From: Chris Conway <cconway@cs.nyu.edu>
Subject:  Re: Using OCaml with SMT solvers
Date: Sun, 8 Mar 2009 23:51:07 +0000 (UTC)
Message-ID:  <loom.20090308T234734-599@post.gmane.org>
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 <news@ger.gmane.org>
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 <jeanyang <at> 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



From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <jim.d.grundy@intel.com>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.0 required=5.0 tests=AWL,HTML_MESSAGE 
	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 210D2BBAF
	for <caml-list@yquem.inria.fr>; Mon,  9 Mar 2009 02:09:23 +0100 (CET)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AkkDAIIJtEmGhogUkWdsb2JhbACCUZJZAQEBAQkLCgcRBbwThAUG
X-IronPort-AV: E=Sophos;i="4.38,326,1233529200"; 
   d="scan'208,217";a="22230863"
Received: from mga02.intel.com ([134.134.136.20])
  by mail2-smtp-roc.national.inria.fr with ESMTP; 09 Mar 2009 02:09:22 +0100
Received: from orsmga001.jf.intel.com ([10.7.209.18])
  by orsmga101.jf.intel.com with ESMTP; 08 Mar 2009 18:03:30 -0700
X-ExtLoop1: 1
X-IronPort-AV: E=Sophos;i="4.38,326,1233561600"; 
   d="scan'208,217";a="496118377"
Received: from orsmsx604.amr.corp.intel.com ([10.22.226.87])
  by orsmga001.jf.intel.com with ESMTP; 08 Mar 2009 18:08:59 -0700
Received: from orsmsx502.amr.corp.intel.com ([10.22.226.210]) by
 orsmsx604.amr.corp.intel.com ([10.250.113.17]) with mapi; Sun, 8 Mar 2009
 18:09:20 -0700
From: "Grundy, Jim D" <jim.d.grundy@intel.com>
To: "caml-list@yquem.inria.fr" <caml-list@yquem.inria.fr>
Cc: "jeanyang@csail.mit.edu" <jeanyang@csail.mit.edu>
Date: Sun, 8 Mar 2009 18:09:19 -0700
Subject: Re: Using OCaml with SMT solvers
Thread-Topic: Re: Using OCaml with SMT solvers
Thread-Index: AcmgU6xO29BTLClcQguHAJ4UOy7bng==
Message-ID: <CA1BBBBC9359F04AA639128AC0D5D1E926AE23DE@orsmsx502.amr.corp.intel.com>
Accept-Language: en-US
Content-Language: en-US
X-MS-Has-Attach:
X-MS-TNEF-Correlator:
acceptlanguage: en-US
Content-Type: multipart/alternative;
	boundary="_000_CA1BBBBC9359F04AA639128AC0D5D1E926AE23DEorsmsx502amrcor_"
MIME-Version: 1.0
X-Spam: no; 0.00; ocaml:01 smt:01 solvers:01 smt:01 solver:01 ocaml:01 solver:01 sourceforge:01 sourceforge:01 integer:01 integer:01 arithmetic:01 arithmetic:01 linear:02 linear:02 

--_000_CA1BBBBC9359F04AA639128AC0D5D1E926AE23DEorsmsx502amrcor_
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: quoted-printable

You might also want to look at the Decision Procedure Toolkit (DPT): http:/=
/dpt.sourceforge.net/

DPT is an open source (Apache 2 licensed, source forge hosted) SMT solver i=
mplemented in OCaml with good performance.  The current release supports on=
ly SAT + EUF, but future releases will soon add integer and rational linear=
 arithmetic - of course, you can always add the theory you want yourself.

Kind regards

Jim Grundy

--_000_CA1BBBBC9359F04AA639128AC0D5D1E926AE23DEorsmsx502amrcor_
Content-Type: text/html; charset="us-ascii"
Content-Transfer-Encoding: quoted-printable

<html xmlns:v=3D"urn:schemas-microsoft-com:vml" xmlns:o=3D"urn:schemas-micr=
osoft-com:office:office" xmlns:w=3D"urn:schemas-microsoft-com:office:word" =
xmlns=3D"http://www.w3.org/TR/REC-html40">

<head>
<META HTTP-EQUIV=3D"Content-Type" CONTENT=3D"text/html; charset=3Dus-ascii"=
>
<meta name=3DGenerator content=3D"Microsoft Word 11 (filtered medium)">
<style>
<!--
 /* Style Definitions */
 p.MsoNormal, li.MsoNormal, div.MsoNormal
	{margin:0in;
	margin-bottom:.0001pt;
	font-size:12.0pt;
	font-family:"Times New Roman";}
a:link, span.MsoHyperlink
	{color:blue;
	text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
	{color:purple;
	text-decoration:underline;}
span.EmailStyle17
	{mso-style-type:personal-compose;
	font-family:Arial;
	color:windowtext;}
@page Section1
	{size:8.5in 11.0in;
	margin:1.0in 1.25in 1.0in 1.25in;}
div.Section1
	{page:Section1;}
-->
</style>
<!--[if gte mso 9]><xml>
 <o:shapedefaults v:ext=3D"edit" spidmax=3D"1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
 <o:shapelayout v:ext=3D"edit">
  <o:idmap v:ext=3D"edit" data=3D"1" />
 </o:shapelayout></xml><![endif]-->
</head>

<body lang=3DEN-US link=3Dblue vlink=3Dpurple>

<div class=3DSection1>

<p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1=
0.0pt;
font-family:Arial'>You might also want to look at the Decision Procedure
Toolkit (DPT): <a href=3D"http://dpt.sourceforge.net/">http://dpt.sourcefor=
ge.net/</a><o:p></o:p></span></font></p>

<p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1=
0.0pt;
font-family:Arial'><o:p>&nbsp;</o:p></span></font></p>

<p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1=
0.0pt;
font-family:Arial'>DPT is an open source (Apache 2 licensed, source forge
hosted) SMT solver implemented in OCaml with good performance. &nbsp;The cu=
rrent
release supports only SAT + EUF, but future releases will soon add integer =
and
rational linear arithmetic &#8211; of course, you can always add the theory=
 you
want yourself.<o:p></o:p></span></font></p>

<p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1=
0.0pt;
font-family:Arial'><o:p>&nbsp;</o:p></span></font></p>

<p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1=
0.0pt;
font-family:Arial'>Kind regards<o:p></o:p></span></font></p>

<p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1=
0.0pt;
font-family:Arial'><o:p>&nbsp;</o:p></span></font></p>

<p class=3DMsoNormal><font size=3D2 face=3DArial><span style=3D'font-size:1=
0.0pt;
font-family:Arial'>Jim Grundy<o:p></o:p></span></font></p>

</div>

</body>

</html>

--_000_CA1BBBBC9359F04AA639128AC0D5D1E926AE23DEorsmsx502amrcor_--


From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <mwh@cs.umd.edu>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.5 required=5.0 tests=DNS_FROM_RFC_ABUSE 
	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 14A48BBAF
	for <caml-list@yquem.inria.fr>; Mon,  9 Mar 2009 08:13:31 +0100 (CET)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: ApgDAA5ftEmACH+TmWdsb2JhbACBTosjiDoBAQEBAQgLCgcRrh2EIYhNhAUG
X-IronPort-AV: E=Sophos;i="4.38,328,1233529200"; 
   d="scan'208";a="22236612"
Received: from server-nat-4.cs.umd.edu (HELO bacon.cs.umd.edu) ([128.8.127.147])
  by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 09 Mar 2009 08:13:24 +0100
X-CSD-MailScanner-Watermark: 1237187595.58549@BLZyMIrifv/MdcBnUb0uWQ
Received: from unknown00236c80bf8f.tiscali.co.uk (79-79-38-117.dynamic.dsl.as9105.com [79.79.38.117])
	(authenticated bits=0)
	by bacon.cs.umd.edu (8.13.1/8.14.1) with ESMTP id n297DBpU031598
	(version=TLSv1/SSLv3 cipher=AES128-SHA bits=128 verify=NO)
	for <caml-list@yquem.inria.fr>; Mon, 9 Mar 2009 03:13:13 -0400
Message-Id: <C5054BC1-8963-4DAE-B692-E52C7E549E23@cs.umd.edu>
From: Michael Hicks <mwh@cs.umd.edu>
To: caml-list@yquem.inria.fr
In-Reply-To: <CA1BBBBC9359F04AA639128AC0D5D1E926AE23DE@orsmsx502.amr.corp.intel.com>
Content-Type: text/plain; charset=WINDOWS-1252; format=flowed; delsp=yes
Content-Transfer-Encoding: quoted-printable
Mime-Version: 1.0 (Apple Message framework v930.3)
Subject: Re: [Caml-list] Re: Using OCaml with SMT solvers
Date: Mon, 9 Mar 2009 07:13:12 +0000
References: <CA1BBBBC9359F04AA639128AC0D5D1E926AE23DE@orsmsx502.amr.corp.intel.com>
X-Mailer: Apple Mail (2.930.3)
X-Greylist: Sender succeeded SMTP AUTH, not delayed by milter-greylist-4.0 (bacon.cs.umd.edu [172.24.3.34]); Mon, 09 Mar 2009 03:13:14 -0400 (EDT)
X-CSD-MailScanner-Information: Please email staff@cs.umd.edu for more information
X-MailScanner-ID: n297DBpU031598
X-CSD-MailScanner: Found to be clean
X-CSD-MailScanner-SpamCheck: not spam, SpamAssassin (not cached, score=-50,
	required 5, autolearn=not spam, ALL_TRUSTED -50.00)
X-CSD-MailScanner-From: mwh@cs.umd.edu
X-Spam: no; 0.00; ocaml:01 smt:01 solvers:01 ocaml:01 binders:01 -mike:01 smt:01 solver:01 beginner's:01 bug:01 sourceforge:01 beginners:01 wrote:01 integer:01 caml-list:01 

Another option is STP.  It's written in C++ I think, with OCaml binders.

http://people.csail.mit.edu/vganesh/STP_files/stp.html

-Mike

On Mar 9, 2009, at 1:09 AM, Grundy, Jim D wrote:

> You might also want to look at the Decision Procedure Toolkit (DPT): =
http://dpt.sourceforge.net/
>
> DPT is an open source (Apache 2 licensed, source forge hosted) SMT =20
> solver implemented in OCaml with good performance.  The current =20
> release supports only SAT + EUF, but future releases will soon add =20
> integer and rational linear arithmetic =96 of course, you can always =20=

> add the theory you want yourself.
>
> Kind regards
>
> Jim Grundy
> _______________________________________________
> 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