私は Z3 を使用して、CUTE、DART、または (おそらく) SAGE と非常によく似た、深さ優先の順序で状態空間を探索するシンボリック エグゼキューターによって生成されたパス条件を解決しています。Z3 のさまざまな使用方法を実験しています。極端な場合、すべてのクエリを Z3 に送信し、その直後に (リセット) します。もう 1 つは、すべての追加の分岐制約を (プッシュ) し、パス条件を正しく弱めるために必要な最小限のバックトラックを (ポップ) (ポップ) します。問題は、すべての状況で他の戦略よりもうまく機能する戦略がないように見えることです。プッシュは最高の利点を提供するようですが、すべてのクエリの後に Z3 をリセットすると、プッシュ/ポップを実行するよりも 1 桁以上高速になるいくつかのケースに遭遇しました。通信のオーバーヘッドはごくわずかであることに注意してください。ほとんどすべての時間が check-sat 内で費やされます。
共有する経験がある人、または Z3 によって内部的に保持されている状態 (レンマなど) に関する何らかの兆候があり、その動作を明確にするのに役立ちますか? また、他の SMT ソルバーの動作はどうですか?