为 Z3 和/或 SMT(v2.6) 建模通用数据类型

Question

我想在 SMT v2.6 中对泛型数据类型的行为进行建模。我使用 Z3 作为约束求解器。我根据official example 建模了一个通用列表作为参数化数据类型，方法如下：

(declare-datatypes (T) ((MyList nelem (cons (hd T) (tl MyList)))))

我希望列表就数据类型而言是通用的。稍后，我想通过以下方式声明常量：

(declare-const x (MyList Int))
(declare-const y (MyList Real))

但是，现在我想在通用数据类型 MyList 上定义函数（例如，长度操作、空操作等），以便它们可重用于所有 T。你知道我怎么能做到这一点吗？我确实尝试过：

(declare-sort K)
(define-fun isEmpty ((in (MyList K))) Bool
    (= in nelem)
) 

但这给了我一个错误信息；我想，要让这个例子工作 Z3 需要做一些类型推断。

如果您能给我一个提示，那就太好了。

Answer 1

SMT-Lib 不允许多态用户定义函数。 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 第 4.1.5 节指出：

排序良好的检查，对于使用排序或术语的命令来说是必需的， 总是相对于当前签名完成。这是一个错误 声明或定义一个已经在当前的符号 签名。这尤其意味着，与理论相反 函数符号，用户自定义函数符号不能重载。

在脚注 29 中进一步扩展：

不重载用户定义符号的动机是为了简化 它们由求解器处理。此限制仅对 想要扩展脚本使用的理论签名的用户 带有一个新的多态函数符号——即，其等级将 如果它是理论符号，则包含参数排序。例如， 想要在任意列表上声明“反向”函数的用户， 必须为每个（具体）定义不同的反向功能符号 脚本中使用的列表排序。此限制可能会在 未来的版本。

因此，正如您所怀疑的，您不能在用户级别定义“多态”函数。但正如脚注所示，未来可能会取消这一限制，随着 SMT 求解器得到更广泛的部署，这种情况很可能会发生。然而，具体什么时候会发生，谁也说不准。