list concat in z3

Question

Is there a way to concat two lists in z3? Similar to the @ operator in ML? I was thinking of defining it myself but I don't think z3 supports recursive function definitions, i.e.,

define-fun concat ( (List l1) (List l2) List 
   (ite (isNil l1) (l2) (concat (tail l1) (insert (head l1) l2)) )
)

Answer 1

You are correct that SMT-Lib2 does not allow recursive function definitions. (In SMT-Lib2, function definitions are more like macros, they are good for abbreviations.)

The usual trick is to declare such symbols as uninterpreted functions, and then assert the defining equations as quantified axioms. Of course, as soon as quantifiers come into play the solver can start returning unknown or timeout for "difficult" queries. However, Z3 is pretty good at many goals arising from typical software verification tasks, so it should be able to prove many properties of interest.

Here's an example illustrating how you can define len and append over lists, and then prove some theorems about them. Note that if a proof requires induction, then Z3 is likely to time-out (as in the second example below), but future versions of Z3 might be able to handle inductive proofs as well.

Here's the permalink for this example on the Z3 web-site if you'd like to play around: http://rise4fun.com/Z3/RYmx

; declare len as an uninterpreted function
(declare-fun len ((List Int)) Int)

; assert defining equations for len as an axiom
(assert (forall ((xs (List Int)))
          (ite (= nil xs)
               (= 0                     (len xs))
               (= (+ 1 (len (tail xs))) (len xs)))))

; declare append as an uninterpreted function
(declare-fun append ((List Int) (List Int)) (List Int))

; assert defining equations for append as an axiom
(assert (forall ((xs (List Int)) (ys (List Int)))
            (ite (= nil xs)
                 (= (append xs ys) ys)
                 (= (append xs ys) (insert (head xs) (append (tail xs) ys))))))

; declare some existential constants
(declare-fun x () Int)
(declare-fun xs () (List Int))
(declare-fun ys () (List Int))

; prove len (insert x xs) = 1 + len xs
; note that we assert the negation, so unsat means the theorem is valid
(push)
(assert (not (= (+ 1 (len xs)) (len (insert x xs)))))
(check-sat)
(pop)

; prove (len (append xs ys)) = len xs + len ys
; note that Z3 will time out since this proof requires induction
; future versions might very well be able to deal with it..
(push)
(assert (not (= (len (append xs ys)) (+ (len xs) (len ys)))))
(check-sat)
(pop)

Answer 2

While Levent's code works, if you're willing to set a bound on the recursion depth, Z3 normally has much less trouble with your assertions. You don't even need to rely on MBQI, which often takes far too much time to be practical. Conceptually, you'll want to do:

; the macro finder can figure out when universal declarations are macros
(set-option :macro-finder true)

(declare-fun len0 ((List Int)) Int)
(assert (forall ((xs (List Int))) (= (len0 xs) 0)))

(declare-fun len1 ((List Int)) Int)
(assert (forall ((xs (List Int))) (ite (= xs nil)
                                       0
                                       (+ 1 (len0 (tail xs))))))

(declare-fun len2 ((List Int)) Int)
(assert (forall ((xs (List Int))) (ite (= xs nil)
                                       0
                                       (+ 1 (len1 (tail xs))))))

... and so on. Writing all of this down manually will probably be a pain, so I'd recommend using a programmatic API. (Shameless plug: I've been working on Racket bindings and here's how you'd do it there.)