可以用Z3来推理子串吗？

Question

我试图使用Z3来推理子串,并且遇到了一些非直观的行为.当被要求确定'xy'是否出现在'xy'内时,Z3返回'sat',但当被询问'x'是否在'x'中时,它返回'unknown',或'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,解算器返回"坐",符合市场预期.这似乎是因为该解算器可以处理此查询"XY",它应该能够处理它的"X".此外,如果搜索findMeX='x'中'xy='xy',它返回"未知".

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

Answer 1

观察到的行为的简短答案是:Z3返回'unknown',因为您的断言包含量词.

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指南介绍的主要功能和MBQI模块的限制.它包含可以由Z3处理的可判定片段.顺便说一句,请注意,如果你有量词,那么丢弃数组理论不会是一个大问题.该指南展示了如何使用量词和函数对数组进行编码.

您可以在以下文章中找到有关MBQI如何工作的更多信息:

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

• 有效解决量化比特矢量公式