4

Z3 で SMTLIBv2 入力形式とパターンを使用すると、問題が発生します。次の入力で「不明」という結果が返され続けます。

(declare-datatypes () ((L L0 L1)))
(declare-fun path () (List L))
(declare-fun checkTransition ((List L)) Bool)

(define-fun isCons ((p (List L))) Bool
    (not (= p nil))
)

; configuration options for :pattern, taken from the Z3 tutorial
(set-option :auto-config false) ; disable automatic self configuration
(set-option :smt.mbqi false)    ; disable model-based quantifier instantiation

(assert (isCons path))
(assert (isCons (tail path)))
(assert (= nil (tail (tail path))))
(assert (= L0 (head path)))             ; initial state constraint

(assert
    (forall ((p (List L)))
    (!
        (implies
            (and    (isCons p)
                    (isCons (tail p)))
            (and    (=  L0  (head p))           ; transition from L0
                    (=  L1  (head (tail p)))))  ; to L1
    :pattern ((checkTransition p))
    )
    )
)
(assert (checkTransition path))

(check-sat)
(get-model)

リストを使用して、遷移システムを介して可能なパスを表します。この場合の遷移システムは、L0 から L1 への遷移によってリンクされた状態 L0 と L1 のみで構成されます。assert ステートメントによって、パスを L0 で始まり、長さが 2 になるように制限します。パス (L0 (cons (L1 (cons nil)))) をモデルとして取得することを期待しています。

私はすでに問題を示す最小限の例に要約しようとしましたが、上記のコードが得られました。パターンを使用して「パス」に再帰チェックを実装し、リスト内の 2 つの連続するノードがそれぞれ (遷移) 制約に準拠していることを確認します。連続するコンスのチェックは、この再帰チェックの停止条件として使用されます。上記の例では、checkTransition を使用して再帰チェックを削除しましたが、それでも機能しません。全体のアイデアは、Z3 2.0 と .net API を使用してこのような方法でモデル チェックの問題を表す Milicevic と Kugler による記事にまでさかのぼります。

パターンのインスタンス化によって結果が「不明」になる可能性があることは承知していますが、なぜこのような単純な (?) 例で既に発生しているのか疑問に思っていました。量指定子のサポートを実現するために間違った方法でパターンを使用していますか?

この問題に関するアイデアは大歓迎です!

よろしくカルステン

PS: MacOS X (10.8.3) で Z3 バージョン 4.3.2 を使用しています。前述の記事: Milicevic, A. & Kugler, H., 2011. SMT とリスト理論を使用したモデル チェック。NASA Formal Methods、pp.282–297。

mhs のコメントに基づく編集:

バージョン4.3.2(不安定)からモデルが取得できない問題が発生するようです。さまざまなバージョンでいくつかのトラブルシューティングを行いました。

  • Z3 4.3.0 32 ビット、WinXP 32 ビット、インストーラーから
    • 結果: 不明ですが、モデルを提供します
  • Z3 バージョン 4.3.1、git checkout 89c1785b73225a1b363c0e485f854613121b70a7、MacOS X、自己コンパイル、これは master ブランチの最新バージョンです....
    • 結果: 不明ですが、モデルを提供します
  • master ブランチの他のさまざまなチェックアウト、すべて <= 4.3.1 は同じ結果をもたらします。
  • Z3 バージョン 4.3.2、夜間ビルド z3-4.3.2.197b2e8ddb91-x64-osx-10.8.2、MacOS X...
    • 結果: 不明、モデルなし
  • Z3 バージョン 4.3.2、夜間ビルド z3-4.3.2.96f4606a7f2d-x64-osx-10.8.2、MacOS X...
    • 結果: 不明、モデルなし

面白い？

4

2 に答える 2

0

Win 7 x64のZ3 4.3.0であなたの例を試したところ、結果が得られました

unknown

(model 
  (define-fun path () (List L)
    (insert L0 (insert L1 nil)))

  (define-fun checkTransition ((x!1 (List L))) Bool
    (ite (= x!1 (insert L0 (insert L1 nil))) true
      true))
)

pathそれはあなたが期待するモデルではありませんか？

unknown具体的な問題を特定することはできませんが、問題が特定されていないため、問題が解決したと思います。たとえば、追加することにより、Z3に反論する何かを与える場合

(assert (not (= L1 (head (tail path)))))
(check-sat)

コードに追加するunsatと、期待どおりになります。

于 2013-04-04T08:43:31.483 に答える