定理证明工具z3花费了很长时间来解决一个公式,我认为它应该轻松处理。为了更好地理解并可能优化我的输入到z3,我想看到z3作为其求解过程的一部分生成的内部约束。
当使用命令行从z3时,如何打印z3为其后端求解器生成的公式?
定理证明工具z3花费了很长时间来解决一个公式,我认为它应该轻松处理。为了更好地理解并可能优化我的输入到z3,我想看到z3作为其求解过程的一部分生成的内部约束。
当使用命令行从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
命令。由于代码是可用的,因此我们还可以在代码中添加自己的跟踪命令。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
AUTO_CONFIG=false
。因此,要重现“发布”模式的行为,必须提供命令行选项 AUTO_CONFIG=true
。