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

Question

我目前正在尝试使用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和值是相互递归的。在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中的列表中的内置推理使用与其他数据类型相同的机制，因此您将获得与平面数据类型声明相同的推理支持。