用Z3/SMT-LIB2定义集合论

Question

我正在尝试使用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,...} (这就是为什么我试图通过量词来获得该功能.)这是正确的吗？还是有另一条路线？

谢谢!

兰吉特.

Answer 1

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

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

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