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

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