如何在 Z3 中以 SMTLIB 格式表示集合成员？答案

【问题标题】：How to express set membership in SMTLIB format in Z3?如何在 Z3 中以 SMTLIB 格式表示集合成员？
【发布时间】：2020-11-25 08:11:03
【问题描述】：

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

【问题讨论】：

标签： z3 smt cvc4

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

【讨论】：