在 z3 中打印内部求解器公式答案

【问题标题】：printing internal solver formulas in z3在 z3 中打印内部求解器公式
【发布时间】：2012-10-27 18:09:41
【问题描述】：

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

【问题讨论】：

标签： z3 smt theorem-proving formal-verification

【解决方案1】：

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 命令。既然有代码，我们也可以在代码中添加自己的trace命令。

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

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

补充说明：

问题出在一个不可判定的片段中：混合整数和实数非线性算术。也就是说，不可能为这个片段编写一个健全而完整的求解器。当然，我们可以编写一个求解器来解决我们在实践中找到的实例。我相信可以扩展nlsat 来处理to_int。
如果您避免使用to_int，您将能够使用nlsat。问题将出现在非线性实数算术片段中。我知道这可能很难，因为 to_int 似乎是您编码中的关键。
z3.codeplex.com 的“unstable”分支中的代码比“master”分支中的正式版本组织得更好。我将很快将它与“master”分支合并。如果您想使用源代码，可以检索“不稳定”分支。
“不稳定”分支使用新的构建系统。您可以构建具有跟踪支持的发布版本。您只需要在生成 Makefile 时使用选项-t。

python 脚本/mk_make.py -t

在调试模式下编译Z3时，默认选项AUTO_CONFIG=false。因此，要重现“发布”模式的行为，您必须提供命令行选项AUTO_CONFIG=true。

【讨论】：

感谢您的及时回复。
也感谢源代码的链接：我不知道它已经发布了。正如您所建议的，我将尝试使用标签和跟踪来转储选择性信息。如果您可以提供有关可能涉及哪些模块的提示，那将非常有帮助 - 它还可以帮助我调整约束 - 我相信我可能没有以最佳方式使用 z3 来解决这个问题。 stackoverflow 不允许我粘贴该代码：可能超出了帖子的行数限制。我将尝试将其作为新帖子再次发布，或者在易于理解的同时提取部分约束和帖子部分。
(assert (>= a b)) (assert (and (= a 1.0))) (assert (and (= b 0.5))) (assert (and (= c 0.5))) (assert (= two-to-p (to_real (^ 2 23)))) ;计算 a (assert (= two-to-exp) 的指数-a (ite (and (>= a 0.5) (= a 1.0) (= a 2.0) (= a 4.0) (= a 8.0) (= a 16.0) (= a 32.0) (= a 64.0) (= a 128.0) (
(assert (= a-plus-b-real (+ a b))) (assert (= overflow (>= a-plus-b-real (+ two-to-exp-a 二-to-exp-a)))) (assert (or (and (not overflow) (= two-to-exp-a-plus-b two-to-exp-a) (= a-plus-b (* (/ (to_real (to_int (* (/a-plus-b-real two-to-exp-a-plus-b) two-to-p))) two-to-p) two-to-exp-a -plus-b))) (and overflow (= two-to-exp-a-plus-b (+ two-to-exp-a two-to-exp-a)) (= a-plus-b (* (/ (to_real(to_int (* (/a-plus-b-real two-to-exp-a-plus-b) two-to-p))) two-to-p) two-to-exp-a -plus-b)))));
部分约束如上，约束总结：主要涉及实数运算。所有声明都是针对 Real 类型的。对变量有诸如 +、*、/ 之类的实数操作。它还使用 to_real 和 to_int。当我对二到 p 使用较小的值时，我很快得到了一个反例（如预期的那样），例如 (to_real (^ 2 10))，但是当我给出较大的值时 z3 似乎会窒息，例如，(to_real (^ 2 23））这是我真正需要做的（最后，我断言两个实际值之间的不等式）。抱歉 - 从格式化文件发布时，格式似乎搞砸了。