Z3を使用して部分文字列を推論できますか？

Question

私は部分文字列について推論するために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をxyに設定すると、ソルバは期待どおりに 'sat'を返します。ソルバーは 'xy'のためにこのクエリを処理できるので、 'x'のためにそれを処理できるはずです。さらに'xy='xy'にfindMeX='x'を検索すると、「不明」が返されます。

SMTソルバー内でこの問題を表現するための説明や代替モデルは誰でも提案できますか？

Answer 1

あなたのアサーションに量子が含まれているため、Z3は 'unknown'を返します。

Z3には、量子を扱うための多くの手順とヒューリスティックがあります。 Z3では、あなたのようなクエリを満たすためのモデルを構築するためのModel-Based Quantifier Instantiation（MBQI）という手法を使用しています。 第1のステップは、量子フリーアサーションを満たす解釈に基づいて候補の解釈を作成することからなる。 残念ながら、現在の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)))) 

は、次のリンクは、第二のアプローチを使用してエンコードされたスクリプトが含まれています http://rise4fun.com/Z3/yD3

2番目のアプローチはより魅力的で、文字列に関するより複雑なプロパティを証明できます。 しかし、充分に定量化された数式を書くことは非常に簡単で、Z3はモデルを構築できません。 Z3 Guideには、MBQIモジュールの主な機能と制限事項が記載されています。 Z3で扱うことができる決定可能なフラグメントが含まれている可能性があります。 ところで、数量詞があれば配列理論を落とすことは大きな問題にはならないことに注意してください。このガイドでは、量子と関数を使用して配列をエンコードする方法を示します。

あなたはMBQIは、以下の論文にどのように機能するかについての詳細な情報を見つけることができます。

• Complete instantiation for quantified SMT formulas

• Efficiently Solving Quantified Bit-Vector Formula