實現一個模擬字符串的公式包含方法

Question

我試圖實現String.Containts函數。 我寫了一些簡單的測試用例，但是下面的一個（應該返回UNSAT）返回SAT。

試驗試圖通過comparig所有可能的子到子在字符串「ABCD」「BD」匹配字符串想（從Z3輸出取文本）：

{(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)))))} 

我曾嘗試過各種實施，但沒有任何成功。

Answer 1

如果您聲明公式，它將返回UNSAT。

http://rise4fun.com/Z3/szN

的部分：

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

是假的監守，您可以設置k以我+ 2或I - 1 你大概的意思寫的含義，而不是結合。 有時使用數組作爲字符串不是執行編碼的最佳方式。 自動機工具包（請參閱：http://rise4fun.com/Rex）使用序列。