Z3可以用來推斷子串嗎？

我正在嘗試使用Z3來推理子串，並且遇到了一些非直觀的行爲。當詢問確定'xy'是否出現在'xy'內時，Z3返回'sat'，但當詢問'x'是'x'還是'x'是'xy'時，返回'未知'。Z3可以用來推斷子串嗎？

我的評論下面的代碼來說明這個問題：

(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解決方案中表達這個問題的替代模型？

來源

2011-08-19 Katie

我試圖重現您沒有成功所描述的問題。您使用的是哪個版本的Z3？我嘗試使用Z3 2.19（Windows和Linux）以及Z3 3.0（可在SMT-COMP網站上獲得），並且所有人都返回上面的查詢。謝謝，獅子座。 –

謝謝你的評論，Leo，你讓我意識到我留下了一些不可能的東西。看起來，我所經歷的行爲只發生在最後的斷言和check-sat出現在'push'和'pop'命令之間，我一直用這些命令在同一組斷言中嘗試各種實驗。我已經相應地修改了這個問題，但現在看來問題在於範圍界定。如果'push'和'pop'被遺漏了，那麼你是對的，'sat'會在所有情況下返回。 – Katie

您是否可能正在尋找：https://www.cs.purdue.edu/homes/zheng16/str/ – user

觀察到的行爲的簡短答案是：Z3返回「未知」，因爲您的斷言包含量詞。

Z3包含許多處理量詞的程序和啓發式。 Z3使用稱爲基於模型的量化器實例（MBQI）的技術來構建模型以滿足像您這樣的查詢。第一步是這個過程包括基於滿足量詞自由斷言的解釋創建候選解釋。不幸的是，在目前的Z3中，這一步與陣列理論不能很好地相互作用。基本問題是由數組理論構建的解釋不能被這個模塊修改。

一個公平的問題是：爲什麼當我們刪除push/pop命令時它會工作？它起作用是因爲當不使用增量求解命令（如push和pop命令）時，Z3使用更積極的簡化（預處理）步驟。

我看到您的問題的兩種可能的解決方法。

你可以避免量詞，並繼續使用數組理論。在你的例子中這是可行的，因爲你知道所有「字符串」的長度。因此，您可以擴展量詞。儘管這種方法看起來很尷尬，但它在實踐中以及許多驗證和測試工具中都有使用。
你可以避免數組理論。您將字符串聲明爲未解釋的類型，就像您爲Char所做的那樣。然後，你聲明一個函數char-of應該返回字符串的第i個字符。你可以公理化這個操作。例如，你可能會說，兩個字符串相等如果他們有相同的長度和包含相同字符：


(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

第二種方法更具吸引力，並且可以讓您證明有關字符串的更復雜的屬性。但是，編寫滿意的量化公式很容易，Z3無法構建模型。 Z3 Guide描述了MBQI模塊的主要功能和限制。它包含可以由Z3處理的可判定的片段。順便說一句，請注意，如果你有量詞，那麼刪除數組理論不會是一個大問題。該指南介紹瞭如何使用量詞和函數對數組進行編碼。

您可以找到有關MBQI如何在以下文章瞭解更多信息：

來源

2011-08-22 21:54:23

Z3可以用來推斷子串嗎？

回答

相關問題