New results on rewrite-based satisfiability procedures

Program analysis and verication require decision procedures to reason on theories of data structures. Many problems can be reduced to the satisability of sets of ground literals in theory T. If a sound and complete inference system for rst-order logic is guaranteed to terminate on T-satisability problems, any theorem-proving strategy with that system and a fair search plan is a T-satisability procedure. We prove termination of a rewrite-based rst-order engine on the theories of records, integer osets, integer osets modulo and lists. We give a modularity theorem stating sucient conditions for termination on a combinations of theories, given termination on each. The above theories, as well as others, satisfy these conditions. We introduce several sets of benchmarks on these theories and their combinations, including both parametric synthetic benchmarks to test scalability, and real-world problems to test performances on huge sets of literals. We compare the rewrite-based theorem prover E with the validity checkers CVC and CVC Lite. Contrary to the folklore that a general-purpose prover cannot compete with reasoners with built-in theories, the experiments are overall favorable to the theorem prover, showing that not only the rewriting approach is elegant and conceptually simple, but has important practical implications.