理論ソルバーの実行時間をトリガー

Question

理論ソルバーの実行時間をトリガーして、各理論チェックにどれくらいの時間がかかるかを見たいと思います。誰がどのファイルとどの変数を調べる必要があるか分かっていますか？統計メソッドにこのオプションがあるかどうかわかりません。

Answer 1

this answerによると、Christoph Wintersteigerは「正確に何をカウントするべきか、カウントすべきではないかが明確ではないため、これは重要ではないと考えています。 Z3のSATソルバの特殊なケースについて

、Leonardo de Mouraによってthis answerは、この特定のサブソルバに属するZ3のソースの特定のC++ファイル（smt_context.cpp）に（例えばbcp()とdecide()など）いくつかの方法に言及しています。