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...

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Maria Paola Bonacina, Mnacho Echenim
• Keywords: Automated Reasoning, Boolean Reasoning, CADE 2007, Rewrite-based Theorem Prover, Satisfiability Modulo Theories