2

我正在尝试使用 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 语法表达这些？

4

1 回答 1

3

确实很烦人 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/）那就太好了，而且确实有沿着这些思路提出的建议（https://www.kroening.com/smt- lib-lsm.pdf），但我认为它尚未被求解器采用，也未被 SMTLib 委员会批准。

于 2020-11-25T21:34:18.287 回答