Introduction
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 for two or more formulas that are mutually unsatisfiable. To be more specific, suppose we have a conjunction of formulas (and A B) that is unsatisfiable. An interpolant for this conjunction is a formula I expressed only using symbols that are common to A and B. The interpolant I makes the following formulas valid:
(implies A I)
(implies B (not I))
In other words, an interpolant tells us something that is true about A, and shows us why A is inconsistent with B, while abstracting away the symbols that are unique to A.
As an example, consider the following input to iZ3:
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(compute-interpolant
(and (= a b) (= a c))
(and (= b d) (not (= c d))))
You can try out this example and those that follow interactively on the RiSE4fun site. This input declares four integer-valued variables a, b, c and d. It then asks iZ3 to compute an interpolant for the conjunction of two formulas, (and (= a b) (= a c)), and (and (= b d) (not (= c d)))). The common symbols between these two formulas include b and c, but not a and d. So an interpolant can’t use the symbols a and d. If you try this input in iZ3, you should see an output like the following:
unsat
(= b c)
This tells us that iZ3 thinks the two formulas are mutually unsatisfiable, and that the formula (= b c) is an interpolant. In fact, it is implied by our first formula, inconsistent with our second formula, and contains only common symbols.
Interpolant formulas like the one above are used in many software analysis tools as a way of generalizing from particular examples. That is, an interpolant for (and A B) gives us a general fact about A that explains its inconsistency with B and might be useful for reasoning about A in other contexts. This property of interpolants allows a tool to prove correct a particular execution path of a program, and derive from this proof a general fact that may be useful in proving other paths (ultimately leading to a full program proof by constructing an inductive invariant).
Theories supported by iZ3
iZ3 can compute interpolants for formulas that combine three theories: equality with uninterpreted function symbols, integer linear arithmetic, and (non-extensional) arrays. These theories are particularly useful for reasoning about programs, which do a lot of operations on integers and arrays. Uninterpreted function symbols can be used as abstractions of operations we don’t know how to handle.
Theory of equality with uninterpreted function symbols
Here’s an example in the theory of equality with uninterpreted function symbols.
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(compute-interpolant
(and (= (f a) c) (= (f b) d))
(and (= a b) (not (= (g c) (g d)))))
Notice that the common symbols in this case do not include the function symbols f and g. In fact, the interpolant we get doesn’t include these symbols:
unsat
(not (and (not (= c d)) (= a b)))
Stare at this formula a moment, and you’ll see its equivalent to “if a = b, then c = d.”
Theory of linear integer arithmetic
Here’s a tricky example using linear integer arithmetic:
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(compute-interpolant
(= y (* 2 x))
(= y (+ (* 2 z) 1)))
Notice that our first formula implies that y is even, while our second formula implies that y is odd. Thus, the formulas are inconsistent. One interpolant for these formulas is (exists (x Int) (= y (* 2 x))). This is a way to say that y is even (that is, it is even if it is 2 times x for some integer x). However, iZ3 tries to avoid introducing quantifiers in interpolants, because quantifiers make can life hard for the tools that consume interpolants. Instead, here is the result that iZ3 produces:
unsat
(<= 0 (+ (* (- 1) y) (* 2 (div y 2))))
Parsing this into more familiar notation, we have 2(y/2) >= y, where the slash is integer division with non-negative remainder. This is equivalent to saying that y is even without using a quantifier. As an aside, you might object that the symbol div is not in common to both formulas. In fact, iZ3 always allows the operators of background theories (the interpreted symbols) to occur in interpolants. This includes constants like -1, and relations like <=.
Theory of arrays
The theory of arrays is quite useful for expressing program semantics. An array is a map from a domain sort to a range sort. iZ3 supports only arrays from sort Int to sort Int. The standard SMT-LIB operators select and store can be used to manipulate arrays.
Here a simple interpolation problem using arrays:
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const a (Array Int Int))
(declare-const b (Array Int Int))
(compute-interpolant
(= b (store (store a x 0) y 0))
(and (= z x) (= (select b z) 1)))
iZ3’s output is:
unsat
(= 0 (select b x))
That is, storing a zero at location y can’t change the zero previously stored at location x. When using the theory of arrays, we can’t always obtain interpolants without quantifiers. iZ3 makes an effort to produce quantifier-free results, but sometimes produces a quantifier even when one isn’t needed.
Formulas with quantifiers
iZ3 has some limited support for formulas with quantifiers. Here’s an example:
(declare-const i Int)
(declare-fun P (Int) Bool)
(declare-fun Q (Int) Bool)
(compute-interpolant
(and (forall ((x Int)) (=> (Q x) (P x)))
(forall ((x Int)) (not (P x))))
(Q i))
The first formula says that predicate Q is stronger than predicate P and that P never holds. The second says that Q is true for some constant i. Here is iZ3’s output:
unsat
(forall ((%0 Int)) (not (Q %0)))
The interpolant says, using a quantifier, that iZ3 never holds. The funny symbol with a percent sign is just a name for a bound variable. Z3 can’t decide all formulas with quantifiers. When it gives up, it prints unknown as the result.
Sequence interpolants
Sequence interpolants are a generalization of interpolants. Suppose we have an inconsistent conjunction of a sequence of formuls (and A1 A2 ... AN). A sequence interpolant for this conjunction would be a sequence of formulas I1, I2 ... I(N-1) such that the following hold:
(implies A1 I1)
(implies (and I1 A2) I2)
(implies (and I2 A3) I3)
...
(implies (and I(N-1) AN) false)
That is, the sequence interpolant forms a sort of sequential proof that the conjunction is onconsistent. In addition, we have a restriction on the symbols in the sequence interpolant. That is Ij must be expressed using the symbols common to A1 ... Aj and A(j+1) ... AN.
Here is an example sequence interpolation problem:
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)
(compute-interpolant
(and (= a b) (= a c))
(= c d)
(and (= b e) (not (= d e))))
Here is iZ3’s output:
unsat
(= b c)
(= b d)
Sequence interpolants are commonly used to construct sequential proofs for code execution sequences or bounded model checking sequences. These proofs can be used for abstraction refinement in a variety of ways.
Tree interpolants
Tree interpolants are a further generalization of interpolants. They are useful for constructing modular proofs for programs with procedures.We are given an unsatisfiable formulas T and set of syntactic positions P from T, such that each position in P occurs only under conjunctions. An interpolant is a map I from P to T.
We write T|p for the subformula of T at position p. Further, we’ll say thet abstraction of the formula at position p, written T[I,p], is T|p with each position q below p replaced by T|q.
For each position p in P, the interpolant formula I(p) must satisfy this condition:
(implies A[I,p] I(p))
Further, I(p) must be expressed using the symbols that occur below p and also occur not below p.
In the formula T, we mark the positions in P with the special unary operator interp. Here is an example of a tree interpolation problem for iZ3:
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(compute-interpolant
(and
(= b c)
(interp (and (= a 0) (= a b)))
(interp (and (= c d) (= d 1)))))
Here is iZ3’s output:
unsat
(= 0 b)
(= c 1)
iZ3 outputs interpolant formulas for the marked positions in the order in which they occur in the formula. Notice that the first interpolant (= 0 b) is implied by the first marked formula (and (= a 0) (= a b)) and that it does not contain the symbol a, which is unique to that subformula. Similarly (= c 1) is implied by the second marked subformula and does not contain the symbol d.
The subformulas marked for interpolation can be nested arbitrarily. iZ3 can’t eliminate uninterpreted function symbols (except for constants) from the interpolant, so these are considered global and may occur in the interpolant in any position. Currently iZ3 has a limitation on the occurrence of constant symbols: the same constant may not occur in two marked subformulas unless one is a subformula of the other. You work around this limitation by renaming one occurrence of the constant and setting the two versions equal at their least common ancestor.
Using iZ3 incrementally
Sometimes it is useful to incrementally construct a set of formulas for interpolation. That is, we might start with a large collection of formulas and try asserting them one at a time until they become inconsistent. We would then like to compute an interpolant based on the proof of unsatisfiability already obtained. This can be done in iZ3 with the command get-interpolant.
Here is an example:
(set-option :produce-interpolants true)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(assert (! (= a b) :named f1))
(assert (! (= a c) :named f2))
(check-sat)
(assert (! (= b d) :named f3))
(assert (! (not (= c d)) :named f4))
(check-sat)
(get-interpolant f1 f2 f3 f4)
Note the we first have to set the option produce-interpolants to warn iZ3 that we will be needing interpolants. When we assert the formulas, we give them names so we can refer to them later. After we get an unsat result, we can then compute a sequence interpolant. Here is iZ3’s output:
sat
unsat
(= a b)
(= b c)
(= c d)
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.
Conclusion
iZ3 can compute interpolants for inconsistent conjunctions, including sequence interpolants and tree interpolants. It handles linear integer arithmetic, uninterpreted function symbols and the theory of arrays, with limited support for quantifiers.