arrays - 无法使用 Z3 中的 Array 定义递归类型

Question

我可以在 Z3 中定义以下递归数据类型:

(declare-datatypes ()
   ((Tree
      (leaf (content Int))
      (node (left Tree) (right Tree)))))

但我无法定义以下内容。我需要先申报吗？或者，如果不允许，我如何获得等效定义(其中一个构造函数具有相同类型的任意字段，由整数索引)？

(declare-datatypes ()
   ((Tree
      (leaf (content Int))
      (node (children (Array Int Tree))))))

Answer 1

这个(四岁)问题与您的问题非常相关:"a datatype contains a set in Z3" .在对这个问题的回答中，Leonardo de Moura 说这是不可能的，而 Nikolaj Bjørner 就如何解决这个限制给出了非常详细的解释。您可能知道他们在 2008 年撰写了介绍 Z3 的原始论文，请参阅 Z3: An Efficient SMT Solver .如果幸运的话，也许其中之一会验证 Z3 中仍然不支持递归混合数组和数据类型。

此外，您所要求的与 rise4fun Z3 tutorial 中“相互递归数据类型”标题下提供的树示例非常相似。 ，除了您的问题使用数组，而rise4fun 上的示例使用列表。我想知道是否可以修改rise4fun 上的列表支持示例以向每个列表节点添加索引。像这样的东西:

(declare-datatypes () ((Tree leaf (node (value Int) (children TreeList)))
                        (TreeList nil (cons (car Tree) (cdr TreeList) (index Int)))))
(assert
    (forall ((treeList TreeList))
        (implies
            (and
                (distinct treeList nil)
                (distinct (cdr treeList) nil)
            )
            (=
                (index (cdr treeList))
                (+ 1 (index treeList))
            )
        )
    )
)
(check-sat)

不幸的是，Z3 给出了 unsat对于这个例子，显然这里有问题。