我是否正确理解不能在 Z3 或 SMTLIB2 中创建“多态”函数？例如我想写一些类似的东西：
(declare-fun Prop (A) Bool)
(declare-fun x1 () Int)
(declare-fun x2 () Bool)
(assert (and (Prop x1) (Prop x2)))
（我想我可以通过为
Int + Bool 然后让 Prop 为联合类型工作，但想要
首先仔细检查不能直接使用参数多态性？）
谢谢！
【问题讨论】：
确实是这样。 SMTLib 使用多排序的一阶逻辑；所以在你的例子中 A 可以是任何类型，但它必须是已知的类型；不是类型参数。
话虽如此，SMTLib 确实允许未解释的排序；也就是说，您可以引入没有基础表示的新排序。 （就像未解释的函数一样。）然后，您可以使用这种注入函数，并模拟您想要的。 （我知道，糟糕的双关语。）
下面是一个示例，您可以如何使用自己喜欢的语言 Ranjit 做到这一点： https://gist.github.com/LeventErkok/163362a59060188f5e62
运行时，它会生成以下 SMT-Lib 代码，其中显示了您需要自己生成、给予或接受的内容：https://gist.github.com/LeventErkok/920aba57cf8cb1810b4a
这是该示例的 Haskell 输出：
Satisfiable. Model:
x1 = 0 :: SInteger
x2 = False
当然，您可以花哨并查询 SMT 求解器，以了解构建过程中使用的未解释函数的解释；但是 SMTLib 本身并不支持这些。虽然如果你问得好，Z3 会给你一个模型，如果你愿意解析有点模糊和不幸的非标准输出。这是这个例子：https://gist.github.com/LeventErkok/54cee74eb3def22dfb5f
另请注意，您通常需要在注射时给出某些公理；就像它们是一对一的并且彼此脱节；这在 SMTLib 中也是可能的，但通常这些都需要量词，因此可能会导致求解器响应“未知”，因为您进入了半可判定区域。
【讨论】：