lista konkat w z3
Czy istnieje sposób na połączenie dwóch list w z3? Podobny do operatora @ w ML? Myślałem o zdefiniowaniu go osobiście, ale nie sądzę, że z3 obsługuje rekurencyjne definicje funkcji, tj.
define-fun concat ( (List l1) (List l2) List
(ite (isNil l1) (l2) (concat (tail l1) (insert (head l1) l2)) )
)