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
benchmarks that were not solvable with any previous approach.