[SMT-LIB] Announcing the Decision Procedure Toolkit Version 1.1

[Jim Grundy]

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