无法在 Z3 中使用 Array 定义递归类型答案

【问题标题】：Cannot define recursive type with Array in Z3无法在 Z3 中使用 Array 定义递归类型
【发布时间】：2016-10-09 12:30:02
【问题描述】：

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

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

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

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

【问题讨论】：

标签： arrays function z3 smt algebraic-data-types

【解决方案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，所以这里显然有问题。

【讨论】：