プロファイラー gprof を使用して (疑似非線形) 整数実数フラグメント (呼び出しグラフを含む統計) にある問題をプロファイリングし、2 つのクラスにかかった時間を分離しようとしました。
I) SAT 解決部分 ([純粋に] ブール伝搬と [純粋に] ブール競合節の検出、バックジャンプ、その他の命題操作を含む)
II) 理論解決部分 (理論の一貫性チェック、理論の矛盾節の生成、理論の伝播を含む)。
smt_context.cpp の3280 ～ 3346行目bounded_search()はトップレベルの DPLL(X) ループを構成していますか?
SATソルバー関数の時間を合計する方が簡単だと思います（数が少ないため）。残りは理論ソルバーの時間と見なすことができます。上記のクラス I に該当すると見なすべき関数を見つけようとしています。彼らsmt::context::decide()は、smt::context::bcp()内にいますsmt::context::propagate()か？他のもの？
smt::context: resolve_conflict()理論ソルバーへの呼び出しと混在しているようですか?
smt::context::propagate()機能以外はほとんど理論伝播（クラスII）のように見えるのは正しいbcp()ですか？また、smt::context::final_check()純粋にクラス II にあるようです。
どんなヒントでも大歓迎です。ありがとう。