Can Z3 check the satisfiability of recursive functions on bounded data structures?

Question

I know that Z3 cannot check the satisfiability of formulas that contain recursive functions. But, I wonder if Z3 can handle such formulas over bounded data structures. For example, I've defined a list of length at most two in my Z3 program and a function, called last, to return the last element of the list. However, Z3 does not terminate when asked to check the satisfiability of a formula that contains last.

Is there a way to use recursive functions over bounded lists in Z3?

Answer 1

(Note that this related to your other question as well.) We looked at such cases as part of the Leon verifier project. What we are doing there is avoiding the use of quantifiers and instead "unrolling" the recursive function definitions: if we see the term length(lst) in the formula, we expand it using the definition of length by introducing a new equality: length(lst) = if(isNil(lst)) 0 else 1 + length(tail(lst)). You can view this as a manual quantifier instantiation procedure.

If you're interested in lists of length at most two, doing the manual instantiation for all terms, then doing it once more for the new list terms should be enough, as long as you add the term:

isCons(lst) => ((isCons(tail(lst)) => isNil(tail(tail(lst))))

for each list. In practice you of course don't want to generate these equalities and implications manually; in our case, we wrote a program that is essentially a loop around Z3 adding more such axioms when needed.

A very interesting property (very related to your question) is that it turns out that for some functions (such as length), using successive unrollings will give you a complete decision procedure. Ie. even if you don't constrain the size of the datastructures, you will eventually be able to conclude SAT or UNSAT (for the quantifier-free case).

You can find more details in our paper Satisfiability Modulo Recursive Programs, or I'm happy to give more here.

Answer 2

You may be interested in the work of Erik Reeber on SULFA, the ``Subclass of Unrollable List Formulas in ACL2.'' He showed in his PhD thesis how a large class of list-oriented formulas can be proven by unrolling function definitions and applying SAT-based methods. He proved decidability for the SULFA class using these methods.

See, e.g., http://www.cs.utexas.edu/~reeber/IJCAR-2006.pdf .