First-order logic provides a convenient formalism for describing a wide variety
of verification conditions. Two main approaches to checking such conditions
are pure first-order automated theorem proving (ATP) and automated theorem
proving based on satisfiability modulo theories (SMT). Traditional ATP systems are
designed to handle quantifiers easily, but often have difficulty reasoning with
respect to theories. SMT systems, on the
other hand, have built-in support for many useful theories, but have a
much more difficult time with quantifiers. One clue on how to get the best of
both worlds can be found in the legacy system Simplify which combines
built-in theory reasoning with quantifier instantiation heuristics.
Inspired by Simplify and motivated by a desire to provide a competitive
alternative to ATP systems, this paper describes a methodology for reasoning
about quantifiers in SMT systems. We present the methodology in the context of
the Abstract DPLL Modulo Theories framework. Besides adapting many of Simplify's
techniques, we also introduce a number of new heuristics. Most important is
the notion of *instantiation level* which provides an effective mechanism
for prioritizing and managing the large search space inherent in quantifier
instantiation techniques.
These techniques have been implemented in the SMT system CVC3. Experimental
results show that our methodology enables CVC3 to solve a significant number of
quantified benchmarks that were not solvable with previous approaches.