z3 - 数据类型包含 Z3 中的集合

Question

如何创建包含一组其他对象的数据类型。基本上，我正在执行以下代码:

(define-sort Set(T) (Array Int T))
(declare-datatypes () ((A f1 (cons (value Int) (b (Set B))))
  (B f2 (cons (id Int) (a  (Set A))))
 ))

但是 Z3 告诉我 A 和 B 的未知排序。如果我删除“设置”，它就像指南中所说的那样工作。
我试图改用 List 但它不起作用。有谁知道如何使它工作？

Answer 1

您正在解决一个经常出现的问题:
我如何混合数据类型和数组(作为集合、多集合或
范围内的数据类型)？

如上所述，Z3 不支持混合数据类型
和单个声明中的数组。
一种解决方案是为
混合数据类型+数组理论。 Z3 包含程序化
用于开发自定义求解器的 API。

开发这个例子还是很有用的
说明能力和局限性
量词和触发器的编码理论。
让我仅使用 A 来简化您的示例。
作为解决方法，您可以定义辅助排序。
但是，解决方法并不理想。它说明了一些
公理“黑客”。它依赖于操作语义
量词在搜索过程中是如何实例化的。

(set-option :model true) ; We are going to display models.
(set-option :auto-config false)
(set-option :mbqi false) ; Model-based quantifier instantiation is too powerful here


(declare-sort SetA)      ; Declare a custom fresh sort SetA
(declare-datatypes () ((A f1 (cons (value Int) (a SetA)))))

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

然后定义 (Set A), SetA 之间的双射。

(declare-fun injSA ((Set A)) SetA)
(declare-fun projSA (SetA) (Set A))
(assert (forall ((x SetA)) (= (injSA (projSA x)) x)))
(assert (forall ((x (Set A))) (= (projSA (injSA x)) x)))

这几乎就是数据类型声明所说的。
为了加强有理有据，您可以将序数与 A 的成员相关联
并强制 SetA 的成员在有根据的排序中更小:

(declare-const v Int)
(declare-const s1 SetA)
(declare-const a1 A)
(declare-const sa1 (Set A))
(declare-const s2 SetA)
(declare-const a2 A)
(declare-const sa2 (Set A))

根据到目前为止的公理，a1 可以是它自身的成员。

(push)
(assert (select sa1 a1))
(assert (= s1 (injSA sa1)))
(assert (= a1 (cons v s1)))
(check-sat)
(get-model)
(pop)

我们现在将一个序数与 A 的成员关联起来。

(declare-fun ord (A) Int)
(assert (forall ((x SetA) (v Int) (a A))
    (=> (select (projSA x) a)
        (> (ord (cons v x)) (ord a)))))
(assert (forall ((x A)) (> (ord x) 0)))

默认情况下，Z3 中的量词实例化是基于模式的。
上面的第一个量化断言不会被实例化
相关实例。可以改为断言:

(assert (forall ((x1 SetA) (x2 (Set A)) (v Int) (a A))
    (! (=> (and (= (projSA x1) x2) (select x2 a))
        (> (ord (cons v x1)) (ord a)))
       :pattern ((select x2 a) (cons v x1)))))

像这样的公理，使用两种模式(称为多模式)
很贵。他们为每一对产生实例化
of (select x2 a) and (cons v x1)

之前的成员约束现在无法满足。

(push)
(assert (select sa1 a1))
(assert (= s1 (injSA sa1)))
(assert (= a1 (cons v s1)))
(check-sat)
(pop)

但模型还不一定很好形成。
集合的默认值为“true”，即
意味着该模型意味着存在一个成员周期
没有的时候。

(push)
(assert (not (= (cons v s1) a1)))
(assert (= (projSA s1) sa1))
(assert (select sa1 a1))
(check-sat)
(get-model)
(pop)

我们可以通过使用来近似更忠实的模型
以下方法来强制执行该集合
用于数据类型是有限的。
例如，每当对集合 x2 进行成员资格检查时，
我们强制集合的“默认”值为“false”。

(assert (forall ((x2 (Set A)) (a A))
    (! (not (default x2))
        :pattern ((select x2 a)))))

或者，只要集合出现在数据类型构造函数中
它是有限的

(assert (forall ((v Int) (x1 SetA))
    (! (not (default (projSA x1)))
        :pattern ((cons v x1)))))


(push)
(assert (not (= (cons v s1) a1)))
(assert (= (projSA s1) sa1))
(assert (select sa1 a1))
(check-sat)
(get-model)
(pop)

在包含附加公理的整个过程中，
Z3 产生答案“未知”，此外
生成的模型表明域 SetA
是有限的(单例)。所以虽然我们可以修补默认值
这个模型仍然不满足公理。它满足
公理仅模实例化。