CDCL(Γ+T) and decision procedures with speculative inferences

CDCL(Γ+T) is a reasoning method that integrates tightly a superposition-based first-order inference system, the parameter Γ, in a CDCL(T) based SMT-solver. The original name is DPLL((Γ+T), but if one uses CDCL(T) in place of DPLL(T), as it has become common, then one should say CDCL(Γ+T). CDCL(Γ+T) is presented as a transition system, where the Γ-transitions deal with non-ground clauses and uninterpreted symbols, while the CDCL(T) transitions deal with ground clauses and interpreted symbols; both see unit ground clauses made of uninterpreted symbols. They communicate through the trail that represents the candidate model built by the SMT-solver, as Γ uses literals in the trail as premises. Thus, the Γ-inferences are model-driven. CDCL(Γ+T) is refutationally complete, and combines both built-in and axiomatized theories. It allows speculative inferences to induce termination on satisfiable inputs and is a decision procedure for several theories, including axiomatizations of type systems relevant to software verification:

Maria Paola Bonacina