从 Z3 字符串中的字符中提取十进制值

Question

让 s1 是 Z3Str 中的任意字符串。 我可以检查其中的第三个字符是否是小写字母：

(declare-const s1 String)
(assert (= s1 "74b\x00!!###$$"))
(assert (str.in.re (str.at s1 2) (re.range "a" "z")))
(check-sat)
(get-value (s1))

现在假设确实如此，我想替换第三个字母 大写（新字符串 s2 将包含替换的版本）。受标准编程语言的启发， 我可能想做这样的事情：

(declare-const s1 String)
(declare-const s2 String)
(declare-const b1 Bool)
(assert (= s1 "74b\x00!!###$$"))
(assert (= b1 (str.in.re (str.at s1 2) (re.range "a" "z"))))
(assert (= (str.substr s2 0 2) (str.substr s1 0 2)))
(assert (= (str.substr s2 3 8) (str.substr s1 3 8)))
(assert (= (str.len s2) (str.len s1)))
(assert (= (str.at s2 2) (ite b1 (- (str.at s1 2) 32) (str.at s1 2))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 32 = 'a'-'A'
(check-sat)
(get-value (s1 s2 b1))

但是，当然，由于类型的原因，这不起作用：

(error "line 9 column 52: Sort mismatch at argument #1 for function 
(declare-fun - (Int Int) Int) supplied sort is String")

是否有任何直接的方法来处理小数 Z3 字符串中字符的值？我的意思是除了 all 小写字母上的巨大 switch-case ... 似乎有一些希望，因为 API 确实支持 "\x61" 作为 "a" 的替代表示。非常感谢任何帮助，谢谢！

Answer 1

以下作品：

(declare-const s1 String)
(declare-const s2 String)
(declare-const b1 Bool)
(assert (= s1 "74b\x00!!###$$"))
(assert (= b1 (str.in.re (str.at s1 2) (re.range "a" "z"))))
(assert (= (str.substr s2 0 2) (str.substr s1 0 2)))
(assert (= (str.substr s2 3 8) (str.substr s1 3 8)))
(assert (= (str.len s2) (str.len s1)))

(declare-const subSecElt (_ BitVec 8))
(declare-const eltUpCase (_ BitVec 8))
(assert (= (bvsub subSecElt #x20) eltUpCase))
(assert (= (seq.unit subSecElt) (str.at s1 2)))
(assert (= (str.at s2 2) (ite b1 (seq.unit eltUpCase) (str.at s1 2))))

(check-sat)
(get-value (s1 s2 b1))

如果这可以进一步简化确实会很好，尽管我没有看到一种简单的方法来做到这一点，因为 API 似乎不允许直接从序列中访问元素。它可以让您获得子序列，但不能获得元素，这正是您在这里真正需要的：请注意，长度为 1 的子序列与该位置的基础元素不同，这解释了您得到的正确类型错误。

这是我得到的这个查询的答案：

sat
((s1 "74b\x00!!###$$")
 (s2 "74B\x00!!###$$")
 (b1 true))