Liste concat in z3
Gibt es eine Möglichkeit, zwei Listen in z3 zusammenzufassen? Ähnlich dem @ -Operator in ML? Ich habe darüber nachgedacht, es selbst zu definieren, aber ich glaube nicht, dass z3 rekursive Funktionsdefinitionen unterstützt, d. H.
<code>define-fun concat ( (List l1) (List l2) List (ite (isNil l1) (l2) (concat (tail l1) (insert (head l1) l2)) ) ) </code>