1

解釈されていない並べ替えと関数で遊んでいて、定量化された数式が空のモデルとどのように相互作用するかを完全に理解できません。ここ（ここでもhttp://rise4fun.com/Z3Py/6ets）は、私をやや混乱させるいくつかの簡単な例です：

  1. [∀v : False]は未飽和ですが、「直感的に」空のモデルに当てはまります。
  2. チェック[∃v : v = v]すると空のモデルが生成されますが、それには満足のいく割り当てがありません。
  3. と一見同等のいくつかの式は[∃v : v = v]、どういうわけか z3 が空のモデルを生成するのを防ぎます。[∃v, v1 : v = v1]はその一例です。たとえば、そのような式をソルバーに追加してから、allsat プロシージャに似たものを作成しようとすると (より多くのモデルを除外するために、より多くの制約を追加する)、空のモデルを取得する前に unsat に遭遇します。

では、z3 が量指定子と空のモデルをどのように処理するかを説明しているドキュメント/論文を参照していただけますか? また、空でないモデルのみに注意を向けることを選択した場合、z3 にそれを求める正しい方法は何ですか? のような[∃v, v1 : v = v1]ことがうまくいくように見えますが、より良い方法はありますか?

4

1 に答える 1

3

Z3 は空のモデルを考慮しません。これは一次論理の標準的な仮定です。詳細については、「一次論理の空のモデル」を検索してください。この規則の動機を説明する多くのリンクが表示されます。一次論理のウィキペディア ページには、簡単な説明があります (セクション「空のドメイン」)。

[]さらに、空のモデルと混同しないでください。入力式を満たすために、Z3 は入力式の未解釈の記号に解釈を割り当てる必要がないことを言っているだけです。Z3 は、式を満たすために必要な記号の解釈のみを表示します。たとえば、数式に[∃v : v = v]未解釈の記号が含まれていない場合、Z3 は空の割り当て []を表示するだけです。

于 2013-03-01T03:02:23.070 に答える