我理解一个人不能在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中也是可能的，尽管通常这些将需要量词，因此由于您进入半确定区域，因此可能导致求解器做出“未知”响应。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句