在 Leon 验证器中，即使在 Leon 中进行归纳推理，为什么会有不同的选项使用相同的求解器？例如。所有 3 个选项：fairz3、smt-z3 和 unrollz3 似乎都使用 z3 求解器并在 leon 中执行归纳推理。
问问题
61 次
1 回答
1
所有三个选项都在原则上做事，但在实现上略有不同（导致不同的性能/可靠性）。
该fairz3选项使用本机 Z3 api（通过ScalaZ3库），同时smt-z3与 Z3 进程标准输入通信（通过Scala SMT-LIB 库使用 SMT-LIB 标准）。为了使用smt-z3，您需要确保z3命令在您的 PATH 中。
有了fairz3，Leon 和 Z3 在同一个进程中运行，这意味着 Z3 中的崩溃会导致整个进程崩溃，而 Leon 没有什么可以阻止它。使用时smt-z3，我们将 Z3 作为一个单独的进程运行，我们可以将 Leon 与该进程隔离开来。如果进程没有响应（或者如果 Leon 决定让求解器超时），则可以随时终止该进程。
这个fair名字是由于历史原因。Leon 的原始实现基于 Z3 的原生 API（显然出于性能原因，直接在 Z3 中构建公式树而不是在 Leon 中构建它们然后为 Z3 翻译它们会更快）。Leon 中的求解器最终被命名为FairZ3Solver，并Fair公平地展开了函数。所有展开逻辑都与 Z3 通信混合在一起。
Leon 中有第二个（新的）实现的归纳展开（称为UnrollingSolver），它独立于底层求解器（Z3、CVC4、RandomSolver）。这种展开与由fairz3. 当您使用时，unrollz3您正在使用它UnrollingSolver（也与 一起使用smt-z3），底层求解器是 Z3 的本机界面（不使用 SMT-LIB 文本界面）。的主要区别FairZ3Solver在于，除了更通用之外，展开是在 Leon 树上完成的。这会稍微影响性能。
于 2015-05-09T23:09:57.513 回答