0

String.Containts関数を実装しようとしています。いくつかの簡単なテストケースを作成しましたが、次のテストケース（UNSATを返す必要があります）はSATを返します。

テストでは、可能なすべてのサブ文字列を必要な文字列（Z3出力から取得したテキスト）と比較することにより、文字列'abcd'のサブ文字列'bd'を一致させようとします。

{(exists ((i Int))
  (let ((a!1 (forall ((k Int))
               (and (>= k i)
                    (<= k (+ i 1))
                    (= (select stringToScan k) (select substring (- k i)))
                    (= (select stringToScan 0) #x0061)
                    (= (select stringToScan 1) #x0062)
                    (= (select stringToScan 2) #x0063)
                    (= (select stringToScan 3) #x0064)
                    (= (select stringToSearch 0) #x0062)
                    (= (select stringToSearch 1) #x0064)))))
    (and (>= i 0)
         (< i 2)
         a!1
         (= (select substring 0) (select stringToSearch 0))
         (= (select substring 1) (select stringToSearch 1)))))}

いろいろな実装を試みましたが、うまくいきませんでした。

4

1 に答える 1

1

式をアサートすると、UNSATが返されます。

http://rise4fun.com/Z3/szN

一部：

(forall ((k Int))
           (and (>= k i)
                (<= k (+ i 1)) ...)))

kをi+2またはi-1に設定できるため、は誤りです。接続詞ではなく含意を書くことを意味している可能性があります。文字列に配列を使用することが、エンコーディングを実行するための最良の方法ではない場合があります。オートマトンツールキット（http://rise4fun.com/Rexを参照）はシーケンスを使用します。

于 2012-09-06T16:41:40.957 に答える