[DPT-Announce] Annoucing DPT 1.1
Brought to you by:
amit_goel,
jim_grundy
From: <jg...@ic...> - 2007-10-02 00:01:57
|
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. Kind regards, Amit Goel, Jim Grundy and Sava Krstic |