在Z3中打印内部求解器公式

Question

定理证明工具z3花费了很长时间来解决一个公式，我认为它应该轻松处理。为了更好地理解并可能优化我的输入到z3，我想看到z3作为其求解过程的一部分生成的内部约束。

当使用命令行从z3时，如何打印z3为其后端求解器生成的公式？

- user1779685

Answer 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命令。由于代码是可用的，因此我们还可以在代码中添加自己的跟踪命令。

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

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

附加说明：

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

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

• "不稳定"分支中的代码比 "主" 分支中的官方版本更好组织。我很快就会将其与 "主" 分支合并。如果您想玩源代码，可以检索 "不稳定" 分支。

• "不稳定"分支使用新的构建系统。您可以使用选项 -t 生成 Makefile 时构建带有跟踪支持的发布版本。

python scripts/mk_make.py -t

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

- Leonardo de Moura

---

感谢您的及时回复。 - user1779685

谢谢您提供源代码的链接，我之前并不知道它已经发布了。正如您所建议的，我将尝试使用标签和跟踪来转储选择性信息。如果您能给出可能涉及的模块的提示，那将非常有帮助——这也将帮助我调整约束条件——我相信我可能没有以最佳方式使用z3来解决这个问题。stackoverflow不允许我粘贴该代码：可能超过了他们发布的行限制。我将尝试将其作为新帖子再次发布或者提取约束的部分并发布可理解的部分。 - user1779685

(assert (>= a b)) (assert (and (< a 128.0) (>= a 1.0))) (assert (and (< b 128.0) (>= b 0.5))) (assert (and (< c 128.0) (>= 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)) 0.5 (ite (and (>= a 1.0) (< a 2.0)) 1.0 (ite (and (>= a 2.0) (< a 4.0)) 2.0 (ite (and (>= a 4.0) (< a 8.0)) 4.0 (ite (and (>= a 8.0) (< a 16.0)) 8.0 (ite (and (>= a 16.0) (< a 32.0)) 16.0 (ite (and (>= a 32.0) (< a 64.0)) 32.0 (ite (and (>= a 64.0) (< a 128.0)) 64.0 (ite (and (>= a 128.0) (< a 256.0)) 128.0 256.0))))))))))) - user1779685

（assert（= a-plus-b-real（+ a b））） （assert（= overflow（> = a-plus-b-real（+ two-to-exp-a two-to-exp-a）））） （assert（或 （和（不溢出） （= 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））） （和溢出 （= 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））））））； - user1779685

约束的部分在上面，约束概述： 它主要涉及实数算术。所有声明都是针对实数类型的。变量上有实数操作，如+、*、/。它还使用to_real和to_int。 当我使用较小的两个p值（例如(to_real (^ 2 10))）时，我很快就得到了反例（正如预期的那样），但是当我给出更大的值（例如(to_real (^ 2 23))）时，z3似乎会卡住，而这正是我真正需要做的事情（最终，我断言两个实数值之间的不等式）。抱歉——从格式化文件发布时，格式似乎已经混乱了。 - user1779685

更新：这是z3约束文件的链接。提前致谢。 - user1779685