1

リスト（Rise4Fun）のcontains-operationをAxiomatisingとして

(declare-fun Seq.in ((List Int) Int) Bool)

(assert (forall ((e Int))
  (not (Seq.in nil e))))

(assert (forall ((xs (List Int)) (e Int))
  (iff
    (not (= xs nil))
    (=
      (Seq.in xs e)
      (or
        (= e (head xs))
        (Seq.in (tail xs) e))))))

Z34.0がアサーションに反論できるようにします

(declare-const x Int)
(assert (Seq.in nil x))
(check-sat) ; UNSAT, as expected

私の目には同等の公理化

(assert (forall ((xs (List Int)) (e Int))
  (ite (= xs nil)
    (= (Seq.in xs e) false)
    (=
      (Seq.in xs e)
      (or
        (= e (head xs))
        (Seq.in (tail xs) e))))))

結果はunknown。

これはトリガーの問題でしょうか、それとも動作の違いを説明できるListドメインに固有の何かがありますか？

4

1 に答える 1

2

rise4funのスクリプトは、:mbqiエンジンを無効にします。したがって、Z3はEマッチングのみを使用して問題を解決しようとします。パターン（別名トリガー）が提供されていない場合、Z3はトリガーを推測します。Z3は、パターン/トリガーを推測するために多くのヒューリスティックを使用します。それらの1つはスクリプトに関連しており、何が起こっているかを説明します。Z3は、「マッチングループ」を生成するパターン/トリガーを選択することはありません。パターン/トリガーPは、QのインスタンスがPの新しいマッチングを生成するときに、数量詞Qのマッチングループを生成すると言います。数量詞を考えてみましょう。

(assert (forall ((xs (List Int)) (e Int))
  (ite (= xs nil)
    (= (Seq.in xs e) false)
    (=
      (Seq.in xs e)
      (or
        (= e (head xs))
        (Seq.in (tail xs) e))))))

Z3は、一致するループを生成するため、この数量詞のパターン/トリガーとして選択しません。(Seq.in xs e)地上項があるとし(Seq.in a b)ます。この用語はパターンと一致します(Seq.in xs e)。数量詞をawillでインスタンス化すると、パターンにも一致するb項が生成されます。とを使用して数量詞をインスタンス化すると、パターンにも一致する項が生成されます。(Seq.in (tail a) b)(Seq.in xs e)(tail a)b(Seq.in (tail (tail a)) b)(Seq.in xs e)

検索中、Z3はいくつかのしきい値を使用して一致するループをブロックします。ただし、通常はパフォーマンスに影響します。したがって、デフォルトでは、Z3は(Seq.in xs e)パターンとして選択されません。代わりに、を選択します(Seq.in (tail xs) e)。このパターンは一致するループを生成しませんが、Z3が2番目と3番目のクエリが満たされないことを証明することも防ぎます。E-matchingエンジンの制限は、通常、:mbqiエンジンによって処理されます。ただし、:mbqiスクリプトでは無効になっています。

スクリプトで2番目と3番目のクエリのパターンを指定する場合。Z3は、すべての例がであることを証明しますunsat。明示的なパターン/トリガーを使用した例を次に示します。

http://rise4fun.com/Z3/DkZd

最初の例は、パターンを使用しなくても通過します。これは、例がであることを証明するために最初の数量詞のみが必要なためですunsat。

(assert (forall ((e Int))
  (not (Seq.in nil e))))

(Seq.in nil e)これはこの数量詞に最適なパターンであり、Z3によって選択されたものであることに注意してください。

于 2012-06-20T19:52:45.597 に答える