シンボリック実行（Klee）のコンテキストでのインクリメンタルソルビングに必要です。シンボリック実行パスの分岐のポイントでは、ソルバーコンテキストを2つの部分に分割する必要があります。真と偽の条件です。もちろん、コストのかかる回避策があります。空のコンテキストを作成し、すべての制約を再生します。
Z3_contextを分割する方法はありますか？そのような機能を追加する予定はありますか？
ノート
深さ優先のシンボリック探索を使用すると、コンテキストの分割を回避できます。つまり、現在の実行パスが「終了」に達するまで探索されるため、このパスは今後探索されなくなります。この場合、分岐点に到達するまでポップして、別の条件分岐の探索を続けるだけで十分です。ただし、Kleeの場合、多くのシンボリックパスが「同時に」探索される（真と偽の分岐の探索がインターリーブされる）ため、ソルバーコンテキストソルバーの切り替え（各メソッドにZ3_context引数があります）と分岐（このためのメソッドはありません、それが私に必要なものです）。
ありがとう！
いいえ、Z3 (3.2) の現在のバージョンはこの機能をサポートしていません。これは重要な機能であり、同等の機能が次のリリースで利用可能になることを認識しています。アイデアは、Context と Solver の概念を分離することです。次のリリースでは、ソルバーを作成 (およびコピー) するための API を用意する予定です。したがって、検索のブランチごとに異なるソルバーを使用できます。簡単に言えば、Context は Z3 式の管理/作成に使用され、Solver は充足可能性のチェックに使用されます。
私が現在この種のことに対して使用しているアプローチは、A の代わりに p => A のような式をアサートすることです。ここで、p は新しいブール値リテラルです。次に、クライアントで、各ブランチに対応するガード リテラルのリスト間の関連付けを維持し、check_assumptions() を使用します。私の状況では、たまたま、各検索中に割り当てられたすべての数式をそのままにしておくことができますが、YMMV. 深さ優先の探索でも、プッシュ/ポップを使用するよりも、この方法の方がはるかに多くの増分再利用が得られるようです。