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=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 ; 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 ; Mon, 9 Mar 2009 03:13:13 -0400 Message-Id: From: Michael Hicks To: caml-list@yquem.inria.fr In-Reply-To: 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: 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