はい、基本的に 2 つのインクリメンタル モードがあります。
スタックベース: push()、pop() を使用して、スタック規律に従うローカル コンテキストを作成します。push() の下に追加されたアサーションは、対応する pop() の後に削除されます。さらに、プッシュの下で導出された補題はすべて削除されます。push()/pop() を使用して状態の凍結をエミュレートし、凍結状態に制約を追加してから、凍結状態に戻ります。これには、push() のスコープ内で蓄積された追加のメモリ オーバーヘッド (学習した補題など) が解放されるという利点があります。作業の仮定は、プッシュで学習した補題はもはや役に立たないということです。
仮定ベース: check()/check_sat() に渡された追加の仮定リテラルを使用して、(1) 仮定リテラルに対して満足できないコアを抽出し、(2) 仮定とは無関係に導出されるガベージ コレクション レンマを使用せずにローカルのインクリメンタル性を得ることができます。言い換えれば、Z3 が仮定リテラルをまったく含まないレンマを学習した場合、それらをガベージ コレクションしないことが期待されます。仮定リテラルを効果的に使用するには、それらを数式にも追加する必要があります。したがって、トレードオフは、仮定で使用される句にはある程度の肥大化が含まれることです。たとえば、式 (<= xy) を局所的に想定したい場合は、節 (=> p (<= xy)) を追加し、check_sat() を呼び出すときに p を想定します。元の仮定は単位であることに注意してください。Z3 はユニットを効率的に増殖させます。仮定リテラルを使用する定式化では、検索のベース レベルの単位ではなくなります。これにより、追加のオーバーヘッドが発生します。単位は二項句になり、二項項は三項句になります。
プッシュ/ポップ機能の違いは、Z3 のデフォルト SMT エンジンにも当てはまります。これは、ほとんどの数式で使用されるエンジンです。Z3 には、いくつかのエンジンのポートフォリオが含まれています。たとえば、純粋なビット ベクトルの問題の場合、Z3 は sat ベースのエンジンを使用することになります。sat ベースのエンジンの増分は、デフォルトのエンジンとは異なる方法で実装されます。ここでは、仮定リテラルを使用してインクリメンタル性が実装されています。プッシュのスコープ内に追加したアサーションは、含意 (=> scope_literals 式) としてアサートされます。そのようなスコープ内の check_sat() は、仮定リテラルを処理する必要があります。反対に、現在のスコープに依存しない結果 (レンマ) はpop() でガベージ コレクションされません。
最適化モードでは、最適化目標をアサートするとき、または API を介して最適化オブジェクトを使用するときに、プッシュ/ポップを呼び出すこともできます。固定小数点も同様です。これら 2 つの機能の場合、プッシュ/ポップは基本的にユーザーの利便性のためのものです。内部増分はありません。その理由は、これらの 2 つのモードが、非常に非増分的な実質的な前処理を使用するためです。