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 prcedures 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 that are canonizable and algebraically soluable. Many useful theories have these properties. Shostak's algorithm is subtle and complex and his description of this procedure is alcking 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.
展开▼
