如何在 Z3 中以 SMTLIB 格式表达集合成员资格？

Question

我正在尝试使用 SMTLIB 格式来表达 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)

函数 emptyset 和 member 似乎在 CVC4 中按预期解析，但在 Z3 中却没有。

通过检查 API（例如，此处：https://z3prover.github.io/api/html/group__capi.html），Z3 确实以编程方式支持空集和成员资格，但是如何表达这些在 SMTLIB 语法中？

Answer 1

z3 和 CVC4 对集合使用的符号略有不同，这确实令人讨厌。在 z3 中，集合本质上是一个范围为 bool 的数组。以此类推，你的程序编码为：

(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)

z3 按原样接受并生成 unsat。但是你会发现现在CVC4不喜欢这个程序了

如果 SMTLib 运动标准化了集合论 (http://smtlib.cs.uiowa.edu/) and there has indeed been a proposal along these lines (https://www.kroening.com/smt-lib-lsm.pdf)，那就太好了，但我认为它还没有被求解器采用，也没有被 SMTLib 委员会批准。

如何在 Z3 中以 SMTLIB 格式表达集合成员资格？

How to express set membership in SMTLIB format in Z3?

z3

smt

cvc4