使用 Z3/SMT-LIB2 定义集合理论

Question

我正在尝试定义集合理论（并集、交集等） Z3 使用 SMTLIB 接口。不幸的是，我现在的 定义挂起 z3 进行琐碎的查询，所以我想我错过了 一些简单的选项/标志。

这是固定链接：http://rise4fun.com/Z3/JomY

（声明排序集） (declare-fun emp() 设置) (declare-fun add (Set Int) Set) （宣趣杯（套套）套） (declare-fun cap (Set Set) Set) (declare-fun dif (Set Set) Set) (declare-fun sub (Set Set) Bool) (declare-fun mem (Int Set) Bool) (assert (forall ((x Int)) (not (mem x emp)))) (assert (forall ((x Int) (s1 Set) (s2 Set)) (= (mem x (cup s1 s2)) (或 (mem x s1) (mem x s2))))) (assert (forall ((x Int) (s1 Set) (s2 Set)) (= (mem x (cap s1 s2)) (和 (mem x s1) (mem x s2))))) (assert (forall ((x Int) (s1 Set) (s2 Set)) (= (mem x (dif s1 s2)) (and (mem x s1) (not (mem x s2)))))) (assert (forall ((x Int) (s Set) (y Int)) (= (mem x (add s y)) (或 (mem x s) (= x y))))) (declare-fun z3v8 () Bool) （断言（不是 z3v8）） （检查周六）

关于我缺少什么的任何提示？

另外，据我所知，没有标准的 SMT-LIB2 集合操作的编码，例如Z3.mk_set_{add,del,empty,...} （这就是我试图通过量词获得该功能的原因。） 那是对的吗？还是有其他路线？

谢谢！

兰吉特。

Answer 1

你的公式是可满足的，Z3 无法为这种公式生成模型。请注意，它必须为未解释的排序Set 生成解释。您可以考虑多种替代方案。

1- 禁用基于模型的量词实例化 (MBQI) 模块。顺便说一句，所有基于 Boogie 的工具（VCC、Dafny、Coral 等）都可以做到这一点。要禁用 MBQI 模块，我们必须使用

(set-option :auto-config false)
(set-option :mbqi false)

备注：在work-in-progress分支中，选项:mbqi已重命名为:smt.mbqi。

缺点：当 MBQI 模块被禁用时，对于包含量词的可满足公式，Z3 通常会返回 unknown。

2- 将 T 集编码为从 T 到布尔值的数组。 Z3 支持扩展数组理论。扩展理论有两个新的运算符：((_ const T) a) 常量数组，((_ map f) a b) 映射运算符。 This paper 描述了扩展数组理论，以及如何使用它来编码集合操作，例如联合和交集。 rise4fun 网站有示例。 如果这些是您的问题中唯一的量词，这是一个很好的选择，因为问题现在在一个可判定的片段中。另一方面，如果您有其他包含集合的量化公式，那么这可能会表现不佳。问题是数组理论建立的模型不知道附加量词的存在。

关于如何使用 const 和 map 对上述运算符进行编码的示例，请参见：http://rise4fun.com/Z3/DWYC

3- 将 T 集合表示为从 T 到 Bool 的函数。如果我们没有集合集或将集合作为参数的未解释函数，这种方法通常效果很好。 Z3 在线教程有一个示例（量词部分）。