z3 - Z3运行时间分析

Question

我正在使用通过 python 实现的 Z3 SMT 求解器。我有源代码，我希望有一些任何迹象表明该进程正在运行。是否可以使用一些详细的命令或任何东西来了解进程当前正在做什么？我知道它背后的算法，但我想可视化，即使使用 printf，代码中发生了什么。

谢谢！

Answer 1

您可以使用：

      set_option(verbose=10)

获得标准错误的详细输出。

求解器完成后，您可以使用

     statistics()

方法。

在调试模式下，您可以使用

     enable_trace("arith")  

获取低级跟踪（此处以“arith”作为示例标签给出）。这仅用于调试。