On Shostak's decision procedure for combinations of theories

Abstract

Decision procedures are increasingly being employed for deciding or simplifying propositional combinations of ground equalities involving uninterpreted function symbols, linear arithmetic, arrays, and other theories. Two approaches for constructing decision procedures for combinations of ground theories were pioneered in the late seventies. In the approach of Nelson and Oppen, decision procedures for two disjoint theories are combined by introducing variables to name subterms and iteratively propagating any deduced equalities between variables from one theory to another. Shostak employs a different approach that works far more efficiently in practice. He uses an optimized implementation of the congruence closure procedure for ground equality over uninterpreted function symbols to combine theories that are canonizable and algebraically solvable. Many useful theories have these properties. Shostak's algorithm is subtle and complex and his description of this procedure is lacking in rigor. We present, for the first time, a careful development and clarification of Shostak's procedure that corrects several mistakes in Shostak's original presentation. Our analysis serves as a useful basis for the implementation, extension, and further optimization of Shostak's decision procedure.

Supported by by NSF Grant CCR-930044, ONR Contract No. N00014-95-C-0168, NSF Grant CCR-9224858, and ARPA contract A721. We are indebted to Rob Shostak for the original ideas studied in this paper. We thank John Rushby, Sam Owre, Deepak Kapur, Harald Ruess, Oliver Möller, and Tomas Uribe, and the anonymous referees for valuable feedback and comments.