I'm trying to use the SMTLIB format to express set membership in Z3:
(declare-const a (Set Int))
;; the next two lines parse correctly in CVC4, but not Z3:
(assert (= a (as emptyset (Set Int))))
(assert (member 12 a))
;; these work in both solvers
(assert (= a (union a a)))
(assert (subset a a))
(assert (= a (intersection a a)))
(check-sat)
The functions emptyset
and member
seem to parse as expected in CVC4, but not in Z3.
From checking the API (e.g., here: https://z3prover.github.io/api/html/group__capi.html), Z3 does support empty sets and membership programatically, but how does one express these in SMTLIB syntax?