使用 Z3/SMT-LIB2 定义集合论 [英] Defining a Theory of Sets with Z3/SMT-LIB2

问题描述

我正在尝试定义集合理论(并集、交集等)Z3 使用 SMTLIB 接口.不幸的是，我目前的定义挂起 z3 以进行微不足道的查询，所以我想我错过了一些简单的选项/标志.

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

<前>(声明排序集)(declare-fun emp() 集)(declare-fun add (Set Int) Set)(declare-fun 杯子 (Set Set) Set)(declare-fun帽(Set Set) Set)(declare-fun dif (Set Set) Set)(declare-fun sub (Set Set) Bool)(declare-fun mem (Int Set) Bool)(断言(forall((x Int))(不是(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)) (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)) (或 (mem x s) (= x y)))))(declare-fun z3v8 () Bool)(断言(不是 z3v8))(检查周六)

关于我遗漏了什么的任何提示?

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

谢谢！

兰吉特.

解决方案

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

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

(set-option :auto-config false)(设置选项: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 在线教程有一个例子(量词部分).

I'm trying to define a theory of sets (union, intersection etc.) for Z3 using the SMTLIB interface. Unfortunately, my current definition hangs z3 for a trivial query, so I guess I'm missing some simple option/flags.

here's the permalink: 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)

Any hint as to what I'm missing?

Also, from what I can tell there is no standard SMT-LIB2 encoding of the set operations e.g. Z3.mk_set_{add,del,empty,...} (which is why I'm trying to get that functionality via quantifiers.) Is that correct? Or is there another route?

Thanks!

Ranjit.

解决方案

Your formula is satisfiable, and Z3 is not capable to produce a model for this kind of formula. Note that, it will have to generate an interpretation for the uninterpreted sort Set. There are a couple of alternatives you may consider.

1- Disable the model-based quantifier instantiation (MBQI) module. BTW, all Boogie-based tools (VCC, Dafny, Coral, etc) do that. To disable the MBQI module, we have to use

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

Remark: in the work-in-progress branch, the option :mbqi has been renamed to :smt.mbqi.

Cons: when the MBQI module is disable, Z3 will usually return unknown for satisfiable formulas that contain quantifier.

2- Encode sets of T as Arrays from T to Boolean. Z3 supports extended array theory. The extended theory has two new operators: ((_ const T) a) constant arrays, ((_ map f) a b) map operator. This paper describes the extended array theory, and how to encode set operations such as union and intersection using it. The rise4fun website has examples. This is a good alternative if these are the only quantifiers in your problem because the problem is now in a decidable fragment. On the other hand, if you have additional quantified formulas that contain sets, then this will probably perform poorly. The problem is that the model built by the array theory is unaware of the existence of the additional quantifiers.

For example of how to encode the above operators using const and map see: http://rise4fun.com/Z3/DWYC

3- Represent sets of T as functions from T to Bool. This approach usually works well if we don't have sets of sets, or uninterpreted functions that take sets as arguments. the Z3 online tutorial has an example (Quantifiers section).

这篇关于使用 Z3/SMT-LIB2 定义集合论的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！