首页 文章

用Z3 / SMT-LIB2定义集合论

提问于
浏览 次
12

我正在尝试使用SMTLIB接口为Z3定义集合理论（并集，交集等） . 不幸的是，我的当前定义为一个简单的查询挂起z3，所以我想我错过了一些简单的选项/标志 .

这是永久链接：http://rise4fun.com/Z3/JomY

(declare-sort Set)
(declare-fun emp () Set)
(declare-fun add (Set Int) Set)
(declare-fun cup (Set Set) 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)) (or (mem x s1) (mem x s2)))))
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
            (= (mem x (cap s1 s2)) (and (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)) (or (mem x s) (= x y)))))

(declare-fun z3v8 () Bool)
(assert (not z3v8))
(check-sat)

有什么迹象表明我缺少什么？

而且，据我所知，没有设定操作的标准SMT-LIB2编码，例如 Z3.mk_set_{add,del,empty,...} （这就是我试图通过量词获得该功能的原因 . ）这是正确的吗？还是有另一条路线？

谢谢！

兰吉特 .

z3 smt

1 回答

  • 11

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

    1-禁用基于模型的量词实例化（MBQI）模块 . 顺便说一句，所有基于Boogie的工具（VCC，Dafny，Coral等）都是这样做的 . 要禁用MBQI模块，我们必须使用

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

    备注：在正在进行的分支中，选项 :mbqi 已重命名为 :smt.mbqi .

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

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

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

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

    回复于

相关问题