数据类型包含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的未知排序.如果我删除"Set",它就像指南所说的一样.我试图使用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))

到目前为止,公理可以成为一个成员.

(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)))))

像这样的公理,使用两种模式(称为多模式)非常昂贵.它们为每对(选择x2 a)和(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是有限的(单个).因此,虽然我们可以修补默认值,但这个模型仍然不能满足公理.它仅满足公理模数实例化.