13

我正在尝试使用 SMTLIB 接口为 Z3 定义集合理论（并集、交集等）。不幸的是，我当前的定义将 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 sy)) (或 (mem xs) (= xy)))))

(declare-fun z3v8 () Bool)
（断言（不是 z3v8））
（检查周六）

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

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

谢谢！

兰吉特。

4

1 回答 1

13

你的公式是可以满足的，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)映射运算符。本文描述了扩展数组理论，以及如何使用它来编码集合操作，例如并集和交集。rise4fun网站有示例。如果这些是您的问题中唯一的量词，这是一个很好的选择，因为问题现在在一个可判定的片段中。另一方面，如果您有其他包含集合的量化公式，那么这可能会表现不佳。问题是数组理论建立的模型不知道附加量词的存在。

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

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

于 2013-07-17T22:03:00.300 回答