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

Question

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

据我了解，从the Z3 tutorial by Moura and Bjorner到"nest recursive data-type definitions inside other types, such as arrays"是不可能的。

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

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

理想情况下，我想在 Z3 中使用内置的 Z3List 类型对这种类型进行编码，但我认为这是不可能的，因为 Z3 不支持递归数据类型和 其他类型。有人可以确认是这种情况吗？

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

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

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

Answer 1

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

Mutually recursive datatypes in z3 and their interaction with built-in types