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

如果我们改为搜索 findMeXY在 xy ，求解器按预期返回“sat”。看起来，由于求解器可以处理“xy”的查询，它应该能够处理“x”的查询。此外，如果搜索 findMeX='x'在 'xy='xy' ，它返回“未知”。

任何人都可以提出解释，或者在 SMT 求解器中表达这个问题的替代模型吗？

Answer 1

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

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

一个公平的问题是:为什么当我们删除 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 工作原理的更多信息:

Complete instantiation for quantified SMT formulas

Efficiently Solving Quantified Bit-Vector Formula