9

Z3 を使用して部分文字列について推論しようとしていますが、直感的でない動作に遭遇しました。Z3 は、「xy」が「xy」内にあるかどうかを判断するように求められると「sat」を返しますが、「x」が「x」にあるか、「x」が「xy」にあるかを尋ねられると「unknown」を返します。

この動作を説明するために、次のコードにコメントを付けました。

(set-logic AUFLIA)
(declare-sort Char 0)

;characters to build strings are _x_ and _y_
(declare-fun _x_ () Char)
(declare-fun _y_ () Char)
(assert (distinct _x_ _y_))

;string literals
(declare-fun findMeX () (Array Int Char))  
(declare-fun findMeXY () (Array Int Char))  
(declare-fun x () (Array Int Char))
(declare-fun xy () (Array Int Char))
(declare-fun length ( (Array Int Char) ) Int )

;set findMeX = 'x'
(assert (= (select findMeX 0) _x_))
(assert (= (length findMeX) 1))

;set findMeXY = 'xy'
(assert (= (select findMeXY 0) _x_))
(assert (= (select findMeXY 1) _y_))
(assert (= (length findMeXY) 2))

;set x = 'x'
(assert (= (select x 0) _x_))
(assert (= (length x) 1))

;set xy = 'xy'
(assert (= (select xy 0) _x_))
(assert (= (select xy 1) _y_))
(assert (= (length xy) 2))

問題が設定されたので、部分文字列を見つけようとします。

;search for findMeX='x' in x='x' 

(push 1)
(assert 
  (exists 
    ((offset Int)) 
    (and 
      (<= offset (- (length x) (length findMeX))) 
      (>= offset 0) 
      (forall 
        ((index Int)) 
        (=> 
          (and 
            (< index (length findMeX)) 
            (>= index 0)) 
          (= 
            (select x (+ index offset)) 
            (select findMeX index)))))))

(check-sat) ;'sat' expected, 'unknown' returned
(pop 1)

findMeXY代わりにinを検索するとxy、ソルバーは予想どおり 'sat' を返します。ソルバーは「xy」についてこのクエリを処理できるため、「x」についても処理できるはずです。さらに、 で検索するfindMeX='x'と'xy='xy'、「不明」が返されます。

SMTソルバー内でこの問題を表現するための説明、またはおそらく代替モデルを提案できる人はいますか?

4

1 に答える 1

6

観察された動作に対する短い答えは次のとおりです。アサーションに量指定子が含まれているため、Z3 は「不明」を返します。

Z3 には、量指定子を処理するための多くの手順とヒューリスティックが含まれています。Z3 は、Model-Based Quantifier Instantiation (MBQI) と呼ばれる手法を使用して、ユーザーのようなクエリを満たすモデルを構築します。この手順の最初のステップは、量指定子のないアサーションを満たす解釈に基づいて候補解釈を作成することです。残念ながら、現在の Z3 では、このステップはアレイ理論とスムーズに相互作用しません。基本的な問題は、配列理論によって構築された解釈がこのモジュールによって変更できないことです。

公正な質問: プッシュ/ポップ コマンドを削除すると、なぜ機能するのでしょうか? これが機能するのは、Z3 が増分解決コマンド (push コマンドや pop コマンドなど) を使用しない場合に、より積極的な単純化 (前処理) ステップを使用するためです。

あなたの問題に対して 2 つの回避策が考えられます。

  • 量指定子を避けて、配列理論を使い続けることができます。すべての「文字列」の長さがわかっているため、これはあなたの例では実現可能です。したがって、量指定子を拡張できます。このアプローチは厄介に思えるかもしれませんが、実際には多くの検証ツールやテスト ツールで使用されています。

  • 配列理論を回避できます。Char の場合と同様に、文字列を解釈されない並べ替えとして宣言します。次に、文字列の i 番目の文字を返す関数 char-of を宣言します。この操作を公理化できます。たとえば、同じ長さで同じ文字を含む 2 つの文字列は等しいと言えます。


(assert (forall ((s1 String) (s2 String))
                (=> (and 
                     (= (length s1) (length s2))
                     (forall ((i Int))
                             (=> (and (<= 0 i) (< i (length s1)))
                                 (= (char-of s1 i) (char-of s2 i)))))
                    (= s1 s2))))

次のリンクには、2 番目の方法を使用してエンコードされたスクリプトが含まれています: http://rise4fun.com/Z3/yD3

2 番目のアプローチはより魅力的で、文字列に関するより複雑なプロパティを証明できます。ただし、Z3 がモデルを構築できないという満足できる定量化された数式を記述するのは非常に簡単です。Z3 ガイドでは、MBQI モジュールの主な機能と制限について説明しています。これには、Z3 で処理できる多くの決定可能なフラグメントが含まれています。ところで、量指定子がある場合、配列理論を削除しても大きな問題にはならないことに注意してください。このガイドでは、量指定子と関数を使用して配列をエンコードする方法を示します。

MBQI のしくみについて詳しくは、次の論文を参照してください。

于 2011-08-22T21:54:23.027 に答える