7

定理证明工具 z3 需要花费大量时间来解决一个公式，我相信它应该能够轻松处理。为了更好地理解这一点并可能优化我对 z3 的输入，我想查看 z3 在其求解过程中生成的内部约束。从命令行使用 z3 时，如何打印 z3 为其后端求解器生成的公式？

4

1 回答 1

12

Z3 命令行工具没有这样的选项。此外，Z3 包含几个求解器和预处理步骤。目前尚不清楚哪个步骤对您有用。Z3 源代码可在https://github.com/Z3Prover/z3获得。当 Z3 在调试模式下编译时，它提供了一个额外的命令行选项-tr:<tag>。此选项可用于有选择地转储信息。例如，源文件nlsat_solver.cpp包含以下指令：

TRACE("nlsat", tout << "starting search...\n"; display(tout); 
               tout << "\nvar order:\n"; 
               display_vars(tout););

命令行选项-tr:nlsat将指示 Z3 执行上述指令。tout是跟踪输出流。它将存储在文件中.z3-trace。Z3 源码中充满了这些TRACE命令。由于代码可用，我们也可以在代码中添加自己的跟踪命令。

如果您发布您的示例，我可以告诉您哪些 Z3 组件用于预处理和解决它。然后，我们可以选择我们应该启用哪些“标签”进行跟踪。

编辑（在发布约束后）：您的示例是混合整数和实数非线性算术。Z3 中新的非线性算术求解器 (nlsat) 不支持to_int. 因此，Z3 通用求解器用于解决您的问题。尽管这个求解器几乎可以接受所有内容，但它甚至对于非线性实数算术都不完整。此求解器的非线性支持基于：区间分析和 Grobner 基计算。此求解器在文件夹中实现src/smt（在不稳定分支中）。算术模块在文件中实现theory_arith*。一个好的跟踪命令行选项是 -tr:after_reduce. 它将在预处理后显示一组约束。瓶颈是算术模块（theory_arith*）。

补充说明：

  • 问题出在一个不可判定的片段中：混合整数和实数非线性算术。也就是说，不可能为这个片段编写一个健全而完整的求解器。当然，我们可以编写一个求解器来解决我们在实践中找到的实例。我相信可以扩展nlsat来处理to_int.

  • 如果你避免to_int，你将能够使用nlsat。问题将出现在非线性实数算术片段中。我知道这可能很难，因为这to_int似乎是您编码中的关键。

  • z3.codeplex.com 的“unstable”分支中的代码比“master”分支中的正式版本组织得更好。我将很快将它与“master”分支合并。如果您想使用源代码，可以检索“不稳定”分支。

  • “不稳定”分支使用新的构建系统。您可以构建具有跟踪支持的发布版本。您只需要-t在生成 Makefile 时使用该选项。

python 脚本/mk_make.py -t

  • Z3 在调试模式下编译时，AUTO_CONFIG=false默认为该选项。因此，要重现“发布”模式的行为，您必须提供命令行选项AUTO_CONFIG=true。
于 2012-10-27T18:37:55.053 回答