DPLL算法备份树的c++文件和方法是什么

Question

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

谢谢！

Answer 1

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