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.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 ; 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" To: "caml-list@yquem.inria.fr" Cc: "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: 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

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

 

DPT is an open source (Apache 2 licensed, source forge hosted) SMT solver implemented in OCaml with good performance.  The cu= rrent release supports only 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_--