1

いくつかの仮説に関して、ステートメントの妥当性を証明することに興味があります。ただし、デフォルトでは Z3 は「オープン」モデルを想定しているようです。たとえば、次のように仮定します。

フー(4)

そして、このステートメントに関して、foo の「in」は偶数であることを示したいと思います。だから私は foo を宣言することから始めます

(declare-fun foo (Int) Bool)

次に、仮説に興味があるので。私は含意を構築します：

(implies (foo 4) (not (exists ((x Int)) (and (foo x) (not (= (mod x 2) 0))))))

最後に、充足可能性よりも妥当性に関心があるので、このステートメントの否定の充足可能性を確認したいと思います。 

(assert (not (implies (foo 4) (not (exists ((x Int)) (and (foo x) (not (= (mod x 2) 0))))))))
(check-sat)

ただし、Z3 は、このステートメントが実際に満足できるものであると報告しています。

sat
(model 
  (define-fun x!0 () Int
    (- 1))
  (define-fun foo ((x!1 Int)) Bool
    (ite (= x!1 4) true
    (ite (= x!1 (- 1)) true
      true)))
)

私はここで何が起こっているかを大まかに理解していますが、私の仮定のステートメントの下で foo を「閉じる」必要があることを最もよく表現する方法がわかりません。この非常に単純な例では、Z3 に foo の他のメンバーが存在しないことを伝えることでこれを行うことができます。

(assert (not (implies (and (foo 4) (not (exists ((x Int)) (and (not (= x 4)) (foo x))))) (not (exists ((x Int)) (and (foo x) (not (= (mod x 2) 0))))))))

しかし、より複雑な仮説に移ると、foo にないものを定義するための数式を自動的に生成することが難しくなるようです。

私が見逃しているばかげたことはありますか？

4

1 に答える 1

1

x = 4 の場合にのみ (foo x) と述べないのはなぜですか? 最初のステートメントは次のように述べています(否定を逆コンパイルした後):

(assert (foo 4))
(assert (exists ((x Int)) (and (foo x) (not (= (mod x 2) 0))))

これは、すべてを「true」にマップする関数 foo によって満たされ、x = -1 を使用して存在論的アサーションを満たすことができます。これは標準的な一次セマンティクスです。

foo が最大で 4 で満足していると言う 1 つの方法は、次のとおりです。

(assert (forall ((x Int)) (=> (foo x) (= x 4))))

また、foo は 4 でのみ成り立つとも言えます。

(assert (forall ((x Int)) (= (foo x) (= x 4))))
于 2013-11-04T03:45:00.727 に答える