从 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 小写字母上的巨大开关盒之外......似乎有一些希望，因为 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))

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

extracting decimal value from a character in a Z3 string

string

smt

z3