5

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?

2 Answers 2

3

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

4
  • (I should add that your 'last' function also falls into that category of functions for which our technique yields a complete decision procedure.)
    – Philippe
    Aug 16, 2011 at 11:29
  • I agree with Philippe. BTW, in your script, you can define last using define-fun macro facility. Macros are automatically unrolled by Z3. The following link contains an example on how to do it: rise4fun.com/Z3/9xVs Aug 16, 2011 at 17:24
  • @Philippe, is the program that you wrote to unroll the recursive function definitions available for reuse? Does your program take SMT-LIB programs as input? Mar 27, 2012 at 16:39
  • @reprogrammer I can give you git access if you want. We currently do not support SMT-LIB as an input format, but use a subset of Scala instead. Depending on your needs we could make something work. It would probably be best if you contact me by email.
    – Philippe
    Mar 29, 2012 at 11:17
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 .

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.