如何在 Z3 Java API 中声明带有类型参数的数据类型？

Question

使用 Z3 可以声明采用类型参数的自定义数据类型（即记录）。例如，一个

Pair

的第一个和第二个元素分别采用

T1

和

T2

类型，声明如下（取自 Z3 指南）：

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))

此类型声明可用于创建具有不同元素类型的对。例如，常数

p1

和

p2

都是具有不同元素类型的对（分别为

Int String

和

Bool Int

）：

(declare-const p1 (Pair Int String))
(declare-const p2 (Pair Bool Int))

我想使用 Z3 的 Java API 声明这样一个参数化数据类型。但是，那里的数据类型声明似乎没有向数据类型声明添加类型参数的功能。

Z3 的 Java API 确实在其

mkDatatypeSort

类中提供了一个方法

Context

来在 Z3 中声明一个新的数据类型（Link）。但是，此方法不接受任何类型参数的参数。此外，构造函数（作为

mkDatatypeSort

的第二个参数）不允许定义类型参数。

我预计可以在 Z3 的 Java API 中声明带有类型参数的数据类型，但我做不到。我是不是遗漏了什么或者这个特性在 Java API 中不存在？

是否可以使用 Java API 声明此类数据类型？

Answer 1

z3 API（无论是 C/C++/Java/Python）不允许创建参数化类型。

请注意，参数化类型本质上是 SMTLib 中的一个优点：本质上，每个具有不同种类的实例化将是其自身的单独类型，彼此无关。所以，我们的想法是自己做：编写一个接受相关排序的函数，并动态创建相应的“单态”类型。您必须每次都稍微更改访问器名称以避免冲突，或者您可以添加足够的类型注释以使求解器找出相关类型。 （我会选择前者，因为它更简单，但后者也绝对有可能。）