我正在尝试使用 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
in xy
,求解器会按预期返回“sat”。看起来,由于求解器可以处理“xy”的查询,它应该能够处理“x”的查询。此外,如果搜索findMeX='x'
in 'xy='xy'
,它会返回“未知”。
任何人都可以提出解释,或者在 SMT 求解器中表达这个问题的替代模型吗?