An Instantiation Scheme for Satisfiability Modulo Theories

State-of-the-art theory solvers generally rely on an instantiation of the axioms of the theory, and depending on the solvers, this instantiation is more or less explicit. This paper introduces a generic instantiation scheme for solving SMT problems, along with syntactic criteria to identify the classes of clauses for which it is complete. The instantiation scheme itself is simple to implement, and we have produced an implementation of the syntactic criteria that guarantee a given set of clauses can be safely instantiated. We used our implementation to test the completeness of our scheme for several theories of interest in the SMT community, some of which are listed in the last section of this paper.