一般的な問題
push-popすでにポップされcheck-satたスコープが、後続のスコープで必要な時間に影響を与えているように見えることに何度か気付きました。
つまり、それぞれが check-sat コマンドを含む複数の (場合によっては任意にネストされた) push-pop スコープを持つプログラムを想定します。さらに、2 番目のチェック サットには 10 秒かかり、最初のチェック サットには 0.1 秒しかかからないと仮定します。
...
(push)
(assert (not P))
(check-sat) ; Could be sat, unsat or unknown
(pop)
...
(push)
(assert (not Q))
(check-sat) ; Could be sat, unsat or unknown
(pop)
最初の push-pop スコープにコメントした後、2 番目の check-sat は 1 しかかかりません。何故ですか？
私の知る限り、プッシュポップスコープが使用されている場合、Z3はインクリメンタルソルバーに切り替わります。なぜ彼らがこのように振る舞うのか（概念的な）理由はありますか？
Z3 は重要度によってシンボルを属性付けすると聞いたことがあるが、これはプルーフ サーチに影響を与える (シンボルの重要度はプルーフ サーチ中にも変化する可能性がある)。それが理由でしょうか？(スコープ間で) 重要度をリセットすることは可能ですか?
バグでしょうか？Leonardo が関連していると思われるバグについて言及しているこの投稿を見つけました (ただし、彼の回答は 2012 年のものです)。
特定のインスタンス
残念ながら、動作を説明するかなり長い (自動生成された) SMTLibファイルしかありません。量指定子と解釈されない関数を使用しますが、mbqi配列やビット ベクトルも使用しません。この例は、148 個のネストされたプッシュ/ポップ スコープと 89 個のチェック サットで構成されており、Z3 4.3.2 では処理に約 8 秒かかります。最後のチェックサット (接頭辞echo) は、はるかに長くかかります。
ランダムにいくつかのプッシュ/ポップ スコープにコメントを付けました (一度に 1 つずつ、最後のものではなく、シンボル宣言にコメントしないように注意してください)。ほとんどの場合、全体の実行時間は 1 秒未満に短縮されました。つまり、最後のチェックサットは大幅に高速化されました。
詳細を提供するために、Z3 のすべてのスコープ (低速、8 秒) の実行と、 でマークされたスコープ[XXX]がコメントされた Z3 の実行 (高速、0.3 秒) を比較しました。結果はこの差分で確認できます(左が遅い、右が速い)。
diff は、すべての check-sats が同じように動作することを示しています (「unsat」を echo することでコメント付きのものを偽造しました)。このことから、コメント付きのスコープは証明検索に影響しますが、最終的な結果には影響しないと結論付けています。
また、得られた統計の違いをある程度理解しようとしましたが、統計を正しく解釈する方法についてはほとんど知りません。ここに私が理解できるいくつかの統計があります：
grobner(383 対 36) およびnonlinear-horner(342 対 25) であるため、実行が遅いほど算術関連の操作が多く実行されるようです。コメントされたスコープは確かに非線形算術に近づきます（そして他の多くの場合もそうです）が、コメントされたスコープの特定の証明は「自明」である必要がx != 0ありxます0 < x。memory(40 対 7)、これは、Z3 が低速バージョンのプログラムでより大きな探索空間を探索していることを示していると解釈します。quant-instantiations(43k 対 51k)、これは私を驚かせました。実行が大幅に高速であるにも関わらず、より多くの量指定子のインスタンス化がトリガーされたからです。