数据类型包含 Z3 中的集合 [英] a datatype contains a set in Z3

问题描述

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

how can I make a datatype that contains a set of another objects. Basically, I am doing the following code:

(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 但它不起作用.有人知道如何使它工作吗?

But Z3 tells me unknown sort for A and B. If I remove "Set" it works just as the guide states. I was trying to use List instead but it does not work. Anyone knows how to make it work?

推荐答案

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

You are addressing a question that comes up on a regular basis: how can I mix data-types and arrays (as sets, multi-sets or data-types in the range)?

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

As stated above Z3 does not support mixing data-types and arrays in a single declaration. A solution is to develop a custom solver for the mixed datatype + array theory. Z3 contains programmatic APIs for developing custom solvers.

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

It is still useful to develop this example to illustrate the capabilities and limitations of encoding theories with quantifiers and triggers. Let me simplify your example by just using A. As a work-around you can define an auxiliary sort. The workaround is not ideal, though. It illustrates some axiom 'hacking'. It relies on the operational semantics of how quantifiers are instantiated during search.

(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 之间的双射.

Then define bijections between (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 的成员在有根据的排序中更小:

This is almost what the data-type declaration states. To enforce well-foundedness you can associate an ordinal with members of A and enforce that members of SetA are smaller in the well-founded ordering:

(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 可以是其自身的成员.

With the axioms so far, a1 can be a member of itself.

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

我们现在将序号与 A 的成员关联起来.

We now associate an ordinal number with the members of 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 中的量词实例化是基于模式的.上面的第一个量化断言不会被实例化相关实例.可以改为断言:

By default quantifier instantiation in Z3 is pattern-based. The first quantified assert above will not be instantiated on all relevant instances. One can instead assert:

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

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

Axioms like these, that use two patterns (called a multi-pattern) are quite expensive. They produce instantiations for every pair of (select x2 a) and (cons v x1)

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

The membership constraint from before is now unsatisfiable.

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

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

but models are not necessarily well formed yet. the default value of the set is 'true', which would mean that the model implies there is a membership cycle when there isn't one.

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

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

We can approximate more faithful models by using the following approach to enforce that sets that are used in data-types are finite. For example, whenever there is a membership check on a set x2, we enforce that the 'default' value of the set is 'false'.

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

或者，每当一个集合出现在数据类型构造函数中时它是有限的

Alternatively, whenever a set occurs in a data-type constructor it is finite

(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是有限的(单例).所以虽然我们可以修补默认值这个模型仍然不满足公理.它满足仅公理模实例化.

Throughout the inclusion of additional axioms, Z3 produces the answer 'unknown' and furthermore the model that is produced indicates that the domain SetA is finite (a singleton). So while we could patch the defaults this model still does not satisfy the axioms. It satisfies the axioms modulo instantiation only.

这篇关于数据类型包含 Z3 中的集合的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！