什么是C++文件和DPLL算法追溯树的方法？

Question

我想找到Z3的C++文件，如果算法无法在当前分支上找到解决方案，那么算法会回溯。我一直在浏览所有的文件，并尝试在python文件上进行调试模式，但目前为止没有运气。我只是想为该方法添加一个print语句，所以我可以知道它何时返回到前一个节点并尝试新路径。

谢谢！

Answer 1

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