z3中的函数声明

Question

在z3中是否可以声明一个将另一个函数作为参数的函数？例如,这个

(declare-fun foo ( ((Int) Bool) ) Int)

似乎并没有起作用.谢谢.

Answer 1

正如莱昂纳多所说,SMT-库并没有让高阶函数.这不仅仅是一种语法限制:使用高阶函数的推理(通常)超出了SMT求解器可以处理的范围.(虽然在某些特殊情况下可以使用未解释的函数.)

如果你确实需要推理高阶函数,那么交互式定理证明是主要的选择武器:Isabelle,HOL,Coq就是其中的一些例子.

但是,有时您希望高阶函数不要推理它们,而只是简化编程任务.SMT-Lib输入语言不适合最终用户在实际情况下通常需要的高级编程.如果那是你的用例,那么我建议不要直接使用SMT-Lib,而是使用一种编程语言,可以访问Z3(或其他SMT求解器).有多种选择,具体取决于哪种主机语言最适合您的用例:

• 如果您是Python用户,Z3 4.0附带的Z3Py是要走的路,
• 如果您是Scala用户,请查看Scala ^ Z3.
• 如果Haskell是您的首选语言,那么请看看SBV.

每个绑定都有自己的功能集,Z3Py可能是最通用的,因为它直接由Z3人员支持.(它还提供了对其他选择无法访问的Z3内部的访问,至少目前是这样.)

Answer 2

不,这是不可能的.但是,您可以定义一个以数组作为参数的函数.

(declare-fun foo((Array Int Bool))Int)

您可以使用此技巧来模拟您的问题中的高阶函数.

这是一个例子:http://rise4fun.com/Z3/qsED

在Z3指南包含有关Z3和SMT的更多信息.