logic - z3 中的相互递归数据类型及其与内置类型的交互

Question

我目前正在尝试使用 Z3 为具有多态列表的非类型语言编码简单的程序逻辑。

据我了解，来自the Z3 tutorial by Moura and Bjorner ，不可能“将递归数据类型定义嵌套在其他类型(例如数组)内”。

所以，假设我有以下 OCaml 类型:

type value =
    | Num of float
    | String of string
    | List of value list

理想情况下，我想使用内置的 Z3List 类型在 Z3 中编码此类型，但我认为这是不可能的，因为 Z3 不支持递归数据类型和其他类型之间的相互递归。有人可以证实情况确实如此吗？

如果是这样，我想唯一可能的方法是我为值列表定义自己的类型，例如 my_list，并且类型 my_list 和 value 相互递归。在 OCaml 中:

type value =
    | Num    of float
    | String of string
    | List   of my_list
and my_list =
    | Cons   of value * my_list
    | nil

但这意味着我将无法利用 Z3 支持 Z3List 的内置推理基础设施。有更好的方法吗？

Answer 1

您必须将扁平版本与 my_list 一起使用是正确的。 好消息是，Z3 中列表的内置推理使用与其他数据类型相同的机制，因此您可以通过平面数据类型声明获得相同的推理支持。