印刷在Z3内部求解公式(printing internal solver formulas in z

该定理证明工具Z3是服用大量的时间来解决一个公式，我相信它应该能够应付自如。为了更好地理解和可能优化我输入到Z3，我想看到Z3产生作为其求解过程的一部分，内部约束。如何打印，即Z3产生其后端求解使用命令行Z3当公式？

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部件用于预处理和解决这个问题。然后，我们可以选择“标签”，我们应该启用跟踪。

编辑（在后的约束被张贴）：您的例子是在混合整数＆真正的非线性运算。新的非线性算法求解（ nlsat在Z3）不支持to_int 。因此，Z3通用求解器用于解决您的问题。虽然这个求解接受几乎所有的东西，它不是真正的非线性算法甚至是完整的。在此求解非线性支持是基于：区间分析和Grobner基计算。该解算器是在文件夹中实现src/smt （在不稳定的分支）。该运算模块是在文件中实现theory_arith* 。一个良好的跟踪命令行选项-tr:after_reduce 。这将显示设定预处理之后约束。瓶颈是运算模块（ theory_arith* ）。

补充说明：

问题是在一个不可判定片段：混合整数＆真正的非线性运算。也就是说，它是不可能写这个片段的声音和完整的解决者。当然，我们可以写，解决了我们在实践中发现实例解算器。我相信这是可能延长nlsat处理to_int 。
如果你避免to_int ，你将能够使用nlsat 。这个问题将是非线性的真实算术片段。我明白，这可能很难，因为to_int似乎是在您的编码一个关键的事情。
在z3.codeplex.com的“不稳定”分支的代码是比“master”分支的正式版要好得多组织。我将与“主”分支很快合并。如果你想用源代码播放，您可以检索“不稳定”分支。
在“不稳定”分支采用了全新的构建系统。你可以建立跟踪支持发行版本。你只需要使用的选项-t生成的Makefile的时候。