在Z3是有可能宣布一个函数，另一个函数作为参数？ 例如，这
(declare-fun foo ( ((Int) Bool) ) Int)
不相当似乎工作。 谢谢。
Answer 1:
正如莱昂纳多所说，SMT-库不允许高阶函数。 这不仅是一个语法限制：与高阶函数推理（一般）超出了SMT求解器可以处理。 （虽然未解释的功能可以在一些特殊情况下使用。）
如果确实需要辩解与高阶函数，然后交互式定理证明是选择的主要武器： 伊莎贝尔 ， HOL ， 勒柯克是一些例子。
但是，有时你想要的高阶函数不要理他们，而仅仅以简化编程任务。 SMT-Lib的输入语言不适合高级编程最终用户通常需要在实际情况。 如果这是你的使用情况，那么我建议不使用SMT-Lib的直接，但随着一种编程语言，使您可以访问Z3（或其他SMT求解器），而工作。 有几种选择，这取决于宿主语言是最适合你的使用情况：
- 如果你是一个Python用户， Z3Py只是附带Z3 4.0是要走的路，
- 如果你是一个Scala的用户，然后看看斯卡拉^ Z3 。
- 如果Haskell是您的首选语言，然后看看SBV 。
每个绑定都有自己的功能集，Z3Py可能是最通用的，因为它是直接由Z3乡亲的支持。 （它也提供了对保持为不可访问的其他的选择，至少暂时Z3内件。）
Answer 2:
不，这是不可能的。 但是，您可以定义一个函数，它接受一个数组作为参数。
（声明乐趣富（（阵列整数BOOL））智力）
您可以使用这种伎俩来模拟像在你的问题的高阶功能。
下面是一个例子： http://rise4fun.com/Z3/qsED
在Z3指南包含有关Z3和SMT的更多信息。
文章来源: function declaration in z3
