2

Microsoft が開発した SMT ソルバーである Z3 に 1 次理論を入れたいと考えています。この理論には、オブジェクトobj1とobj2の 2 つのオブジェクトがあり、オブジェクトを受け取りアクションを返す関数moveと、アクションを引数として取る1 位の述語が発生します。理論には数式occurs(move(obj1)) が含まれており、これが発生述語が真になる唯一の方法であることを確認したいと思います。私は発生の定義を与えることによってこれを行います:

forall (A) (occurs(A) <-> (A = move(obj1)))

これは、ocens(move(obj1))は理論から推論できますが、ocens(move(obj2))は推論できないことを意味します。これを証明するために、私はこれを次のように Z3 に翻訳しました。

(declare-datatypes () (( Obj obj1 obj2 )))
(declare-sort Action 0)

(declare-fun occurs (Action) Bool)
(declare-fun move (Obj) Action)

(assert (forall ((A Action)) (
    = (occurs A) (= A (move obj1))
)))

(check-sat)
(get-value ((occurs (move obj1))))
(get-value ((occurs (move obj2))))

問題は、これにより次の出力が得られることです。

sat
(((occurs (move obj1)) true))
(((occurs (move obj2)) true))

私には理解できません。発生の定義は、述語が真になるための必要かつ十分な条件をすべて提供するため、どのモデルでも発生(move(obj2))が真になることはできないと思います。私は何を間違っていますか？

更新 de Moura のおかげで、問題の解決策を見つけることができました。私がする必要があるのは、アクション (私の場合は関数) に固有の名前の公理を提供することです。2 つの異なる引数がある場合、 sort の同じ要素を決して返さないことmoveを述べる必要があります。これはいくつかの方法で実行できますが、これが最も簡潔なバージョンであることがわかりました。moveAction

(assert (forall ((o1 Obj) (o2 Obj)) 
    (=> (not (= o1 o2)) (not (= (move o1) (move o2))))))
4

1 に答える 1

3

アサートしなかった制約を想定しています。たとえばmove、定数関数であることを妨げるものは何もありません。Z3が製作したモデルが正解です。(get-model)の後にコマンドを追加すると、モデルを取得できます(check-sat)。コマンド(declare-sort Action 0)は、解釈されない並べ替えを宣言しています。Z3 によって作成されたモデルでは、sort の解釈はAction1 つの要素のみを含み、occurs定数move関数です。これは、スクリプト内のすべてのアサーションがモデルによって満たされるため、モデルです。

于 2012-10-29T21:58:13.703 に答える