How to express set membership in SMTLIB format in Z3?

Question

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?

Answer 1

It's indeed annoying z3 and CVC4 use slightly different notations for sets. In z3, a set is essentially an array with the range of bool. Based on this analogy, your program is coded as:

(declare-const a (Set Int))

(assert (= a ((as const (Set Int)) false)))
(assert (select a 12))

(assert (= a (union a a)))
(assert (subset a a))
(assert (= a (intersection a a)))
(check-sat)

which z3 accepts as is and produces unsat. But you'll find that CVC4 doesn't like this program now.

It would be great if the SMTLib movement standardized the theory of sets (http://smtlib.cs.uiowa.edu/) and there has indeed been a proposal along these lines (https://www.kroening.com/smt-lib-lsm.pdf) but I don't think it has been adopted by solvers nor sanctioned by the SMTLib committee yet.