A Combination Method for Generating Interpolants

Greta Yorsh and Madanlal Musuvathi

We present a combination method for generating interpolants for a class
of first-order theories. Using interpolant-generation procedures for
individual theories as black-boxes, our method generates interpolants
for the combined theory. Our method extends that of McMillan to a class
of first-order theories, which we characterize as equality-interpolating
Nelson-Oppen theories. We show that this class includes many useful
theories such as the quantifier-free theories of uninterpreted
functions, linear inequalities over reals, and Lisp structures. Our
method provides a way to integrate interpolant generation within
existing Nelson-Oppen-style decision procedures (such as Simplify,
Verifun, ICS, and CVC-Lite).

We have implemented this method in Zap, a symbolic reasoning engine in
development at Microsoft Research.

To access the technical report: PDF
<ftp://ftp.research.microsoft.com/pub/tr/TR-2004-108.pdf>