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

【问题标题】：Mutually recursive datatypes in z3 and their interaction with built-in typesz3 中的相互递归数据类型及其与内置类型的交互
【发布时间】：2017-09-21 08:34:54
【问题描述】：

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

据我了解，从the Z3 tutorial by Moura and Bjorner 开始，不可能“将递归数据类型定义嵌套在其他类型中，例如数组”。

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

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

理想情况下，我想在 Z3 中使用内置的 Z3List 类型对该类型进行编码，但我认为这是不可能的，因为 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 为 Z3Lists 支持的内置推理基础架构。有没有更好的方法来做到这一点？

【问题讨论】：

标签： logic ocaml z3 smt recursive-datastructures

【解决方案1】：

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

【讨论】：