Strategies for combining decision procedures

Implementing efficient algorithms for combining decision procedures has been a challenge and their correctness precarious. In this paper we describe an inference system that has the classical Nelson–Oppen procedure at its core and includes several optimizations: variable abstraction with sharing, canonization of terms at the theory level, and Shostak's streamlined generation of new equalities for theories with solvers. The transitions of our system are fine-grained enough to model most of the mechanisms currently used in designing combination procedures. In particular, with a simple language of regular expressions we are able to describe several combination algorithms as strategies for our inference system, from the basic Nelson–Oppen to the very highly optimized one recently given by Shankar and Rueß. Presenting the basic system at a high level of generality and non-determinism allows transparent correctness proofs that can be extended in a modular fashion when new features are introduced in the system.