T-Decision by Decomposition

10 years 8 months ago
T-Decision by Decomposition
Much research concerning Satisfiability Modulo Theories is devoted to the design of efficient SMT-solvers that integrate a SATsolver 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...
Maria Paola Bonacina, Mnacho Echenim
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Maria Paola Bonacina, Mnacho Echenim
Comments (0)