解釈されていない並べ替えと関数で遊んでいて、定量化された数式が空のモデルとどのように相互作用するかを完全に理解できません。ここ(ここでもhttp://rise4fun.com/Z3Py/6ets)は、私をやや混乱させるいくつかの簡単な例です:
[∀v : False]
は未飽和ですが、「直感的に」空のモデルに当てはまります。- チェック
[∃v : v = v]
すると空のモデルが生成されますが、それには満足のいく割り当てがありません。 - と一見同等のいくつかの式は
[∃v : v = v]
、どういうわけか z3 が空のモデルを生成するのを防ぎます。[∃v, v1 : v = v1]
はその一例です。たとえば、そのような式をソルバーに追加してから、allsat プロシージャに似たものを作成しようとすると (より多くのモデルを除外するために、より多くの制約を追加する)、空のモデルを取得する前に unsat に遭遇します。
では、z3 が量指定子と空のモデルをどのように処理するかを説明しているドキュメント/論文を参照していただけますか? また、空でないモデルのみに注意を向けることを選択した場合、z3 にそれを求める正しい方法は何ですか? のような[∃v, v1 : v = v1]
ことがうまくいくように見えますが、より良い方法はありますか?