DPLLアルゴリズムがツリーをバックトレースするC++ファイルと方法は何ですか？

Question

現在のブランチで解決策が見つからない場合、アルゴリズムのバックトレースを行うZ3用のC++ファイルを探しています。私はすべてのファイルを調べていて、pythonファイルでデバッグモードを試しましたが、これまでのところ運がありません。私はちょうどメソッドにprintステートメントを追加したいので、前のノードに戻ってきたときに新しいパスを試してみることができます。

ありがとうございます！

Answer 1

どのソルバーZ3が問題に使用するかによって異なります。通常、src/smtにはsmt_context.cppが使用されます。関連するバックジャンプは、context :: pop_scopeメソッドで追跡できます。他のソルバーも存在します。src/sat/sat_solverはビットベクトルとブールの問題に使用されます。それにも同様のpopメソッドがあります。最後に、nlsatは実数に対する非線形多項式演算に使用されます。