ある式Pをアサートしたと仮定し、充足可能性を確認した後、 Z3 からその部分モデルを取得し、それをMと呼びましょう。
ここで、必要に応じて現在のモデルMを拡張することで、別の式Qを満たすことができるかどうかをテストできます。つまり、式P と Qが満足できるかどうかを確認したいのですが、現在の部分モデルによって割り当てられた値を修正します。
あるいは、Z3 に特定の部分モデルを「完成」させることは可能ですか? (つまり、まだ部分モデルを取得したいのですが、場合によっては、部分モデルを拡張して、関数によって割り当てられていない定数/関数を含む可能性のある任意の式Qを評価できるようにしたいと考えています。現行モデル）