z3 - smtlib 中的参数函数

Question

我知道有一种方法可以在 SMTLIB 中声明参数数据类型。有没有办法定义一个接受这种类型的函数？例如标准文档有：

( declare - datatypes ( ( Pair 2) ) (
( par ( X Y ) ( ( pair ( first X ) ( second Y )) ))))

现在如何声明一个接受参数Pair类型的函数？

Answer 1

SMTLib不允许参数函数定义。请注意，内部函数，如 +、- 等，可以是多排序/参数的，例如，它们在整数和实数上工作得很好。但是用户定义的函数不允许多排序。也就是说，您可以编写一个接受 a 的函数(Pair Int Bool)，但不能编写一个接受(Pair a b)wherea和b是类型变量的函数；即，多态。

这在https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf的第 4.1.5 节中进行了解释：

使用排序或术语的命令所需的排序良好检查始终针对当前签名进行。声明或定义已在当前签名中的符号是错误的。这尤其意味着，与理论函数符号相反，用户定义的函数符号不能被重载。(29)

后来在脚注 29 中，它说：

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

TLDR；不，您不能在 SMTLib 中定义参数函数。但随着逻辑变得更加丰富，这可能会在未来发生变化。当前的解决方法是“单态化”过程，即在您使用的每个具体类型处生成函数的新版本。这可以手动完成，也可以由为您生成 SMTLib 的高级工具自动完成。