|
|
|---|
For information what Craig interpolants are and how iZ3 computes them, see this paper.
iZ3 reads interpolation problems in two formats, both of which are compatible with the SMT-LIB 1.2 standard, using the theory AUFLIA.
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.
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.
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 unsat interpolant: (not (>= x 0)) (and (not (<= y 0)) (not (>= x 0)))
> iz3.exe -t -f tree1.smt unsat interpolant: (not (>= x 0)) (not (<= y 0))
Note that while the sequence and tree interpolation examples have the same constraints, the interpolants differ.
iZ3 provides an API for C and C++ programmers. It extends the Z3 C API by added a set of calls to support interpolation.
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".