在z3中打印内部求解器公式 [英] printing internal solver formulas in z3

问题描述

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

The theorem proving tool z3 is taking a lot of time to solve a formula, which I believe it should be able to handle easily. To understand this better and possibly optimize my input to z3, I wanted to see the internal constraints that z3 generates as part of its solving process. How do I print the formula that z3 produces for its back-end solvers, when using z3 from the command line?

推荐答案

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

Z3 command line tool does not have such option. Moreover, Z3 contains several solvers and pre-processing steps. It is unclear which step would be useful for you. The Z3 source code is available at https://github.com/Z3Prover/z3. When Z3 is compiled in debug mode, it provides an extra command line option -tr:<tag>. This option can be used to selectively dump information. For example, the source file nlsat_solver.cpp contains the following instruction:

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

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

The command line option -tr:nlsat will instruct Z3 to execute the instruction above. tout is the trace output stream. It will be stored in the file .z3-trace. The Z3 source is full of these TRACE commands. Since the code is available, we can also add our own trace commands in the code.

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

If you post your example, I can tell you which Z3 components are used to preprocess and solve it. Then, we can select which "tags" we should enable for tracing.

EDIT (在不稳定的分支中) . 算术模块在文件theory_arith*中实现. 良好的跟踪命令行选项是-tr:after_reduce.预处理后，它将显示一组约束. 瓶颈是算术模块(theory_arith*).

EDIT (after the constraints were posted): Your example is in the mixed integer & real nonlinear arithmetic. The new nonlinear arithmetic solver (nlsat) in Z3 does not support to_int. Thus, the Z3 general purpose solver is used to solve your problem. Although this solver accepts almost everything, it is not even complete for nonlinear real arithmetic. The nonlinear support on this solver is based on: interval analysis and Grobner basis computations. This solver is implemented in the folder src/smt (in the unstable branch). The arithmetic module is implemented in the files theory_arith*. A good tracing command line option is -tr:after_reduce. It will display the set of constraints after pre-processing. The bottleneck is the arithmetic module (theory_arith*).

其他备注:

• 问题出在无法确定的片段中:混合整数&真正的非线性算术.也就是说，不可能为该片段编写完善的求解器.当然，我们可以编写一个求解器来解决我们在实践中发现的实例.我相信可以扩展nlsat来处理to_int.

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

If you avoid to_int, you will be able to use nlsat. The problem will be in the nonlinear real arithmetic fragment. I understand that this may be hard, since the to_int seems to be a key thing in your encoding.

z3.codeplex.com上不稳定"分支中的代码比主"分支中的正式版组织得更好.我将很快将其与"master"分支合并.如果要使用源代码，可以检索不稳定"分支.

The code in the "unstable" branch at z3.codeplex.com is much better organized than the official version in the "master" branch. I will merge it with the "master" branch soon. You can retrieve the "unstable" branch if you want to play with the source code.

不稳定"分支使用新的生成系统.您可以构建具有跟踪支持的发行版本.生成Makefile时只需使用选项-t.

The "unstable" branch uses a new build system. You can build the release version with tracing support. You just have to use the option -t when generating the Makefile.

python脚本/mk_make.py -t

python scripts/mk_make.py -t

• 在调试模式下编译Z3时，默认情况下选项AUTO_CONFIG=false.因此，要重现发布"模式的行为，必须提供命令行选项AUTO_CONFIG=true.
• When Z3 is compiled in debug mode, the option AUTO_CONFIG=false by default. Thus, to reproduce the behavior of "release" mode, you must provide the command line option AUTO_CONFIG=true.

这篇关于在z3中打印内部求解器公式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！