0

我正在尝试对 Z3 中的集合进行建模，以便能够找到涉及集合的约束的模型。

我目前使用数组表示一个集合。如果数组中的对应条目为真，则元素属于该集合。然后我有一些在约束中使用的公理。

这是 SMT 2.0 中的示例。

(define-sort Set (T) (Array T Bool))

(declare-fun |Set#Card| ((Set Int)) Int)
(assert (forall ((s (Set Int)))
      (!
        (<= 0 (|Set#Card| s))
          :pattern ((|Set#Card| s)))))

(declare-fun |Set#Singleton| (Int) (Set Int))
(assert (forall ((r Int))
      (!
        (select (|Set#Singleton| r) r)
       :pattern ((|Set#Singleton| r)))))
(assert (forall ((r Int) (o Int))
      (iff (select (|Set#Singleton| r) o) (= r o))))
(assert (forall ((r Int)) (= (|Set#Card| (|Set#Singleton| r)) 1)))

(declare-fun s () (Set Int))
(assert (= 1 (|Set#Card| s)))
;(assert (= 1 (|Set#Card| (|Set#Singleton| 1))))
;(assert (not (= 1 (|Set#Card| (|Set#Singleton| 1)))))
(check-sat)
(get-info :reason-unknown)
(get-model)

我的问题是我得到了unknown，因此在大多数情况下没有模型。我认为我的公理化太弱了。在上面的示例中，我想获得一个s包含一个元素的集合的模型。

有谁知道我如何使用 Z3 来获取涉及集合的约束模型？

每个答案都有帮助。即，也许我误解了Z3能做什么和不能做什么。也欢迎有关如何处理此问题的想法（其他工具建议，...）。

4

1 回答 1

1

问题是 Z3 将无法构建满足以下断言的模型：

(assert (forall ((r Int) (o Int))
      (iff (select (|Set#Singleton| r) o) (= r o))))

一种可能的解决方法是定义|Set#Singleton|而不是公理化它。我们可以使用const数组运算符来定义它，并且store. 这是一个可能的定义：

(define-fun |Set#Singleton| ((r Int)) (Set Int)
            (store ((as const (Set Int)) false) r true))

这是具有此定义的修改示例的链接。Z3sat在我使用定义后返回一个模型。

在文本界面中，我们必须使用as构造来指定我们想要的常量数组的种类。请注意，我们可以使用 Z3 中可用的扩展数组理论对多个集合操作进行编码。这篇论文有更多的细节。但是，这种方法不能对|Set#Card|函数进行编码。

另一种选择是对unknown结果使用“候选模型”。这不是理想的解决方案，但有几个用户这样做。

于 2013-09-16T15:17:50.707 回答