Z3 Microsoft Research
iZ3 Documentation

Craig interpolants

For information what Craig interpolants are and how iZ3 computes them, see this paper.

File format

iZ3 reads interpolation problems in two formats, both of which are compatible with the SMT-LIB 1.2 standard, using the theory AUFLIA.

Sequence interpolant

An interpolant for a sequence of formulas A1...An is a sequence of formulas I1...In-1 such that A1 implies I1, I1 and A2 imply A3, ..., and In-1 and An-1 imply In-1. Moreover, each Ii must be expressed using just the symbols of the logic, the interpreted symbols of the theory, and symbols in common between A1..Ai and Ai+1..An.

iZ3 represents the input sequence A1..An in SMT-LIB format as a sequence of ":formula" statements. An example of this format is seq1.smt. If these formulas are unsatisfiable, iZ3 outputs an interpolant as a sequence of formulas I1..In-1.

Tree interpolants

Suppose T = (V,E,L) is a directed labeled tree, with vertex set V, edges set E and labeling function L that maps each vertex to a formula. An interpolant for this tree is a labeling function I from V to formulas, such that I of the root vertex is "false" and for every vertex v, L(v) and the conjunction of I(w) for children w of v implies I(v), and moreover, I(v) is expressed using just the symbols of the logic, the interpreted symbols of the theory, and the common symbols between the subtree rooted at v and the remainder of the tree.

A tree interpolation problem is represented in SMT-LIB format as follows. The vertices of the tree are represented by fresh Boolean symbols, except the root, which is represented by "false". For each vertex v of the tree, there is a formula of the form (implies (and w1 ... wm L(v)) v) where w1...wm are the children of v. The vertices w1..wn must precede vertex v in the file. The root vertex, represented by "false" is necessarily last. An example of this format is tree1.smt. If the set of formulas L(v) is unsatisfiable, iZ3 outputs an interpolant as a sequence of formulas I(v1)...I(vn-1) where v1...vn-1 are the vertices in the order in which they occur in the input file, excluding the root.

Command line

iZ3 is invoked on the command line like this:

   iZ3 [options] file.smt

The available options are:

   -t,--tree       interpret input as a tree interpolation problem
   -c,--check      check that the result is correct
   -p,--profile    print user time profile information
   -f,--flat       ouput flat formulas
   -o file         ouput to SMT-LIB file

The "flat" output format can be easier to read, since it does not use "let" bindings for sub-expressions. However, flat formules can also be exponentially larger.

Usage examples:

> iz3 -f seq1.smt
(not (>= x 0))
(and (not (<= y 0)) (not (>= x 0)))
> iz3.exe -t -f tree1.smt
(not (>= x 0))
(not (<= y 0))

Note that while the sequence and tree interpolation examples have the same constraints, the interpolants differ.

C language API

iZ3 provides an API for C and C++ programmers. It extends the Z3 C API by added a set of calls to support interpolation.

Limitations and bugs

Currently, tree interpolation is not fully implemented, and is subject to the following restrictions: (1) a constant symbol (nullary function symbol) may occur only along one path from root to leaf. (2) Non-nullary function symbols are considered global, that is, may occur in any interpolant formula. Note that (1) is a nuisance, but not a fundamental limitation, since a constant symbol that occurs along two branching paths may replaced by separate symbols for each path that are equated at the least common ancestor.

Contary to the specification, the function Z3_write_interpolation_problem actually writes some of the forulas in the output file using the :assumption tag rather the :formula tag. These files are still read correctly by Z3_read_interpolation_problem.

There is an incompleteness for intereger arithmetic in FOCI that sometimes impacts iZ3. The symptom of this is a message "invalid lemma written to file invalid_lemma.smt".

Last modified Fri Oct 5 2012 11:32:37