DPLL(T): Fast decision procedures

Abstract

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 prepositional SAT. Here we propose a new approach, namely a general DPLL(X) engine, whose parameter X can be instantiated with a specialized solver Solverτ for a given theory T, thus producing a system DPLL(T). We describe this DPLL(T) scheme, the interface between DPLL(X) and Solverτ, 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. © Springer-Verlag Berlin Heidelberg 2004.