Quantifier-Free Interpolation in Combinations of Equality Interpolating Theories

The use of interpolants in verification is gaining more and more importance. Since theories used in applica- tions are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly re-use interpolation algorithms for the component theories. We show that a sufficient and necessary condition to do this for quantifier-free interpolation is that the component theories have the ‘strong (sub-)amalgamation’ property. Then, we provide an equivalent syntactic characterization and show that such characterization covers most theories commonly employed in verification. Finally, we design a combined quantifier-free inter- polation algorithm capable of handling both convex and non-convex theories; this algorithm subsumes and extends most existing work on combined interpolation.