Match expressions vs Or expressions

[philzook58]

I was trying a couple different encodings of append in the style of minikanren using define-fun-rec and was a bit surprised that these two encodings didn't amount to about the same thing. The first seems to work poorly, hanging forever. The second returns instantly. I was wondering if someone might have any comments about why this would be the case.

(define-sort LInt () (List Int))
(define-fun-rec appendo ((x LInt) (y LInt) (z LInt)) Bool
  (or
    (and (= x nil) (= y z))
    (exists ((w Int) (ws LInt) (res LInt)) 
        (and 
          (= x (insert w ws))
          (= z (insert w res)) 
          (appendo ws y res)
        ))
  )
)

(declare-const x LInt)
(declare-const y LInt)
(declare-const z LInt)
;(assert (appendo nil nil nil))
;(assert (appendo (insert 0 nil) nil (insert 0 nil)))
;(assert (appendo nil (insert 0 nil) (insert 0 nil)))
;(assert (appendo x y z))
;(assert (appendo x y (insert 4 (insert 0 nil))))
(assert (appendo x y (insert 42 nil)))
(check-sat)
(get-model)

(define-sort LInt () (List Int))
(define-fun-rec appendo ((x LInt) (y LInt) (z LInt)) Bool
  (match x (
    (nil (= y z))
    ((insert w ws) 
      (match z (
        (nil false) ; impossible
        ((insert v vs) (and (= v w) (appendo ws y vs)))
      ))
  )))
)

(declare-const x LInt)
(declare-const y LInt)
(declare-const z LInt)
;(assert (appendo x y z))
(assert (appendo x y (insert 42 nil)))
(check-sat) ;sat
(get-model)

[NikolajBjorner]

z3 uses if-then-else to determine evaluation order and unfolding priorities for recursive functions.
So if you rewrite a recursive definition with or instead of match (which is translated to if-then-else) it doesn't work.