z3 - DPLL算法回溯树的c ++文件和方法是什么？

Question

我正在尝试找到 Z3 的 c++ 文件，如果在当前分支上找不到解决方案，算法会在该文件中回溯。我一直在查看所有文件并在 python 文件上尝试了调试模式，但到目前为止还没有运气。我只想在方法中添加一个打印语句，这样我就可以知道它何时返回到前一个节点并尝试新路径。

谢谢！

Answer 1

这取决于 Z3 使用哪个求解器来解决您的问题。它通常使用 src/smt 中的 smt_context.cpp。可以在 context::pop_scope 方法中跟踪相关的回跳。也存在其他求解器：src/sat/sat_solver 用于位向量和布尔问题。它有一个类似的弹出方法。最后，nlsat 用于实数上的非线性多项式算术。