This site uses cookies for analytics, personalized content and ads. By continuing to browse this site, you agree to this use. Learn more

Be sure to follow along with the examples by clicking the "edit" link in the corner. See what the tool says, try your own formulas, and experiment!

iZ3 is an interpolating version of the state-of-the art theorem prover Z3 from Microsoft Research. This guide assumes you are already familiar with Z3.

In addition to all the functions of Z3, iZ3 can produce Craig interpolants for
two or more formulas that are mutually unsatisfiable. The Craig interpolant is a formula that acts as
an explanation for the unsatisfiability.
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:

load in editor(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))))

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).

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.

Here's an example in the theory of equality with uninterpreted function symbols.

load in editor(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`

."

Here's a tricky example using linear integer arithmetic:

load in editor(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 `<=`

.

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:

load in editor(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.

iZ3 has some limited support for formulas with quantifiers. Here's an example:

load in editor(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 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:

load in editor(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 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 `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.

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:

load in editor(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)

`z3.codeplex.com`

. Use
the `Source`

tab and choose the `unstable`

branch. The file `README`

has build and installation
instructions.
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.