A Craig interpolant is a formula that acts as an explanation for the unsatisfiability of a logical formula. Interpolating Z3 (iZ3) is a version of the Z3 theorem prover that can produce Craig interpolants from proofs. To be more specific, suppose “A” and “B” are logical formulas and we can prove “A implies B”. An interpolant for this implication is a formula I expressed only using symbols that are common to A and B that makes the following formulas valid:
- “A implies I”
- “I implies B”
The power of interpolants is that they put a proof in a syntactic form that allows it to be generalized. This ability can be applied, for example, to extract proofs about sequential circuits or programs from proofs about specific execution sequences, or to derive abstractions from counterexamples.
Capabilities of iZ3
iZ3 can derive Craig interpolants from proofs in first-order logic, modulo certain theories, including:
- Integer linear arithmetic
- The theory of arrays
iZ3 handles quantified formulas, but does not always produce a quantifier-free interpolant when a quantifier-free interpolant exists. iZ3 can also produce sequence interpolants and tree interpolants, which are useful for program verification and constraint Horn clause (CHC) solving, as in the Duality CHC solver.
For more information on using iZ3, see the iZ3 tutorial.
Obtaining iZ3
iZ3 was a part of Z3 up to version 4.7.1. Releases including iZ3 can be downloaded from the Z3 github repository. However iZ3 is not maintained in current releases of Z3.
Papers
The following paper describes an older version of iZ3 that used a method of decomposing Z3 proofs into lemmas and applying the FOCI interpolating prover to these lemmas. The current version constructs interpolants directly from Z3 proofs.
Interpolants from Z3 proofs (Kenneth L. McMillan), In International Conference on Formal Methods in Computer-Aided Design, FMCAD ’11, Austin, TX, USA, October 30 – November 02, 2011, 2011. [bibtex] [pdf]