T-decision by decomposition

Much research concerning Satisfiability Modulo Theories is devoted to the design of efficient SMT-solvers that integrate a SAT-solver with T-satisfiability procedures. The rewrite-based approach to T-satisfiability procedures is appealing, because it is general, uniform and it makes combination of theories simple. However, SAT-solvers are unparalleled in handling the large Boolean part of T-decision problems of practical interest. In this paper we present a decomposition framework that combines a rewrite-based theorem prover and an SMT-solver in an off-line mode, in such a way that the prover "compiles the theory away," so to speak. Thus, we generalize the rewrite-based approach from T-satisfiability to T-decision procedures, making it possible to use the rewrite-based prover for theory reasoning and the SAT-solver in the SMT-solver for Boolean reasoning. We prove the practicality of this framework by giving decision procedures for the theories of records, integer offsets and arrays.