什麼是C++文件和DPLL算法追溯樹的方法？

Question

我想找到Z3的C++文件，如果算法無法在當前分支上找到解決方案，那麼算法會回溯。我一直在瀏覽所有的文件，並嘗試在python文件上進行調試模式，但目前爲止沒有運氣。我只是想爲該方法添加一個print語句，所以我可以知道它何時返回到前一個節點並嘗試新路徑。

謝謝！

Answer 1

這取決於哪個解算器Z3用於您的問題。它通常在src/smt中使用smt_context.cpp。相關的backjump可以在context :: pop_scope方法中進行追蹤。其他求解器也存在：src/sat/sat_solver用於位向量和布爾問題。它有一個類似的流行方法。最後，nlsat用於對實數進行非線性多項式運算。