Z3可以用来推理子串吗？

Question

我正在尝试使用 Z3 来推理子字符串，并且遇到了一些不直观的行为。当询问“xy”是否出现在“xy”中时，Z3 返回“sat”，但当询问“x”是否在“x”中或“x”是否在“xy”中时，它返回“未知”。

我注释了以下代码来说明此行为：

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

如果我们改为在 xy 中搜索 findMeXY，正如预期的那样，求解器返回“sat”。看起来既然求解器可以处理“xy”的查询，它应该能够处理“x”的查询。此外，如果在 'xy='xy' 中搜索 findMeX='x'，则会返回“unknown”。

任何人都可以建议一个解释，或者可能是在 SMT 求解器中表达此问题的替代模型吗？

Answer 1

观察到的行为的简短答案是：Z3 返回“未知”，因为您的断言包含量词。

Z3 包含许多处理量词的过程和启发式方法。
Z3 使用一种称为基于模型的量词实例化 (MBQI) 的技术来构建模型来满足像您这样的查询。
第一步是该过程包括基于满足无量词断言的解释创建候选解释。
不幸的是，在当前的Z3中，这一步与阵列理论的交互并不顺利。
基本问题是该模块无法修改由数组理论构建的解释。

一个合理的问题是：为什么当我们删除推送/弹出命令时它会起作用？
它之所以有效，是因为当不使用增量求解命令（例如push和pop命令）时，Z3使用更积极的简化（预处理）步骤。

我看到您的问题有两种可能的解决方法。

• 您可以避免使用量词，并继续使用数组理论。这在您的示例中是可行的，因为您知道所有“字符串”的长度。因此，您可以扩展量词。
  尽管这种方法可能看起来很尴尬，但它在实践中以及许多验证和测试工具中都有使用。

• 你可以避免数组理论。您将 string 声明为未解释的排序，就像您对 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 指南描述了 MBQI 模块的主要功能和限制。
它包含可能由 Z3 处理的可判定片段。
顺便说一句，请注意，如果你有量词，放弃数组理论不会是一个大问题。该指南展示了如何使用量词和函数对数组进行编码。

您可以在以下论文中找到有关 MBQI 工作原理的更多信息：

• 量化 SMT 公式的完整实例化

• 高效求解量化位向量公式