Delayed Theory Combination vs. Nelson-oppen for satisfiability modulo theories: A comparative analysis

Most state-of-the-art approaches for Satisfiability Modulo Theories (SMT (T)) rely on the integration between a SAT solver and a decision procedure for sets of literals in the background theory T(T -slover). Often T is the combination T1 ∪ T2 of two (or more) simpler theories (SMT(T1 ∪ T2)), s.t. the specific Ti-solvers must be combined. Up to a few years ago, the standard approach to SMT(T1 ∪ T2)was to integrate the SAT solver with one combined T1 ∪ T2-solver, obtained from two distinct Ti-solvers by means of evolutions of Nelson and Oppen's (NO) combination procedure, in which the Ti-solvers deduce and exchange interface equalities. Nowadays many state-of-the-art SMT solvers use evolutions of a more recent SMT(T1 ∪ T2) procedure called Delayed Theory Combination (DTC), in which each Ti-solvers interacts directly and only with the SAT solver, in such a way that part or all of the (possibly very expensive) reasoning effort on interface equalities is delegated to the SAT solver itself. ...