DPLL( T): Fast Decision Procedures

11 years 5 months ago
DPLL( T): Fast Decision Procedures
The logic of equality with uninterpreted functions (EUF) and its extensions have been widely applied to processor verification, by means of a large variety of progressively more sophisticated (lazy or eager) translations into propositional SAT. Here we propose a new approach, namely a general DPLL(X) engine, whose parameter X can be instantiated with a specialized solver SolverT for a given theory T, thus producing a system DPLL(T). We describe this DPLL(T) scheme, the interface between DPLL(X) and SolverT , the architecture of DPLL(X), and our solver for EUF, which includes incremental and backtrackable congruence closure algorithms for dealing with the built-in equality and the integer successor and predecessor symbols. Experiments with a first implementation indicate that our technique already outperforms the previous methods on most benchmarks, and scales up very well.
Harald Ganzinger, George Hagen, Robert Nieuwenhuis
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where CAV
Authors Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
Comments (0)