Given a typical list datatype:
(declare-datatypes (X)(
(Lst
(nil)
(insert
(head X)
(tail Lst)))))
I'm trying to create a function that returns whether a given element is in a given list. It looks like I have to use an uninterpreted function. I've tried different approaches without success. For example:
(declare-fun is-in-lst ((Int)(Lst Int)) Bool)
(assert (forall((elem Int)(lst (Lst Int)))
(=
(is-in-lst elem lst)
(and
(is-insert lst)
(or
(= elem (head lst))
(is-in-lst elem (tail lst)))))))
(declare-const l1 (Lst Int))
(assert (is-in-lst 6 l1))
(assert (is-in-lst 5 l1))
Is this doable in Z3? If so, what would be the best way to address the problem? Thank you
The latest SMTLib standard allows for recursive definitions. Also List is predefined in Z3, so you don't need to define it yourself. You can code your function as:
(define-fun-rec elem ((e Int) (l (List Int))) Bool
(ite (= l nil) false (or (= e (head l)) (elem e (tail l)))))
(declare-const l1 (List Int))
(assert (elem 6 l1))
(assert (elem 5 l1))
(check-sat)
(get-value (l1))
For this, z3 responds:
sat
((l1 (let ((a!1 (insert 6 (insert 4 (insert 7 (insert 5 nil))))))
(insert 0 (insert 1 (insert 3 (insert 2 a!1)))))))
You might have to get a recent version of Z3 from their nightly builds, as support for recursive-functions is rather new and thus the latest official release (4.6.0) may or may not work with this. (You can get nightly builds from https://github.com/Z3Prover/bin/tree/master/nightly.)