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=none 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 9C9AABC69 for ; Tue, 2 Oct 2007 18:21:48 +0200 (CEST) X-IronPort-AV: E=Sophos;i="4.21,220,1188770400"; d="scan'208";a="17199778" Received: from mga02.intel.com ([134.134.136.20]) by mail4-smtp-sop.national.inria.fr with ESMTP; 02 Oct 2007 18:21:48 +0200 Received: from orsmga001.jf.intel.com ([10.7.209.18]) by orsmga101.jf.intel.com with ESMTP; 02 Oct 2007 09:21:46 -0700 X-ExtLoop1: 1 X-IronPort-AV: E=Sophos;i="4.21,220,1188802800"; d="scan'208";a="237835123" Received: from azsmsx334.amr.corp.intel.com ([10.2.121.57]) by orsmga001.jf.intel.com with ESMTP; 02 Oct 2007 09:21:22 -0700 Received: from azsmsx343.amr.corp.intel.com ([143.182.253.5]) by azsmsx334.amr.corp.intel.com with Microsoft SMTPSVC(6.0.3790.1830); Tue, 2 Oct 2007 09:21:22 -0700 Received: from [10.10.35.173] ([10.10.35.173]) by azsmsx343.amr.corp.intel.com with Microsoft SMTPSVC(6.0.3790.1830); Tue, 2 Oct 2007 09:21:21 -0700 Message-ID: <47027001.3070506@intel.com> Date: Tue, 02 Oct 2007 09:21:21 -0700 From: Jim Grundy User-Agent: Mail/News 1.5.0.2 (X11/20060508) MIME-Version: 1.0 To: caml-list@yquem.inria.fr Subject: Announcing The Decision Procedure Toolkit Version 1.1 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-OriginalArrivalTime: 02 Oct 2007 16:21:22.0019 (UTC) FILETIME=[454A9330:01C80510] X-Spam: no; 0.00; smt:01 solver:01 solver:01 smt:01 solvers:01 model:01 parametric:01 emphasizes:01 ocaml:01 sava:01 2.0:98 sourceforge:01 sourceforge:01 functions:01 arithmetic:01 We are pleased to announce the open source availability of the Decision Procedure Toolkit (DPT). DPT is a modern SMT solver. This release provides a MiniSAT-like DPLL solver, a DPLL(T) style theory combination mechanism, and a solver for the theory of Uninterpreted Functions (EUF). The next release will add a linear arithmetic solver and a cooperation mechanism for more than one theory. DPT is an open source project licensed under the Apache 2.0 license. You can download DPT from sourceforge: http://sourceforge.net/projects/dpt DPT is intended to serve as a platform for experiments in SMT solvers and their applications. Subsequent releases will include features like model generation, proof production and interpolants. We also expect to support parametric theories and the HOL logic. The DPT design philosophy emphasizes flexible interfaces and transparent implementation over raw speed. DPT is implemented in OCaml. These decisions not withstanding, speed is good, and so we have made a reasonable effort to ensure DPT is fast. Further announcements about DPT will be made on the dpt-announce mailing list. You can subscribe to the list via the project web site. Kind regards, Amit Goel, Jim Grundy and Sava Krstic -- Jim Grundy, Research Scientist. Intel Corporation, Strategic CAD Labs Mail Stop RA2-451, 2501 NW 229th Ave, Hillsboro, OR 97124-5503, USA Phone: +1 971 214-1709 Fax: +1 971 214-1771 http://www.intel.com/technology/techresearch/people/bios/grundy_j.htm Key Fingerprint: 5F8B 8EEC 9355 839C D777 4D42 404A 492A AEF6 15E2