小编Kat*_*tie的帖子

我试图使用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 = …