Flexible interpolation with local proof transformations
Roberto Bruttomesso, Simone Fulvio Rollini, Natasha Sharygina, Aliaksei Tsitovich · 2010
Model checking based on Craig’s interpolants ultimately re-lies on efficient engines, such as SMT-Solvers, to log proofs of unsatisfiability and to derive the desired interpolant by means of a set of algorithms known in literature. These algo-rithms, however, are designed for proofs that do not contain mixed predicates. In this paper we present a technique for transforming the propositional proof produced by an SMT-Solver in such a way that mixed predicates are eliminated. We show a number of cases in which mixed predicates arise as a consequence of state-of-the-art solving procedures (e.g. lemma on demand, theory combination, etc.). In such cases our technique can be applied to allow the reuse of known interpolation algorithms. We demonstrate with a set of ex-periments that our approach is viable. 1.