Z3 排序转换：（一个字符）字符串到（长度 8）位向量答案

【问题标题】：Z3 sort conversion: (one character) String to (length 8) bitvectorZ3 排序转换：（一个字符）字符串到（长度 8）位向量
【发布时间】：2017-10-26 09:34:39
【问题描述】：

参考之前提出的关于 extracting the decimal value from a Z3 string 的 SO 问题，我知道 将 BitVec8 转换为一个字符串是可能的。例如，运行这个查询：

(declare-const s String)
(declare-const someBV8 (_ BitVec 8))
(assert (= (str.len s) 6))

(assert (= someBV8 #x62))
(assert (= (seq.unit someBV8) (str.at s 2)))
(assert (= (seq.unit someBV8) (str.at s 3)))
(assert (= (seq.unit someBV8) (str.at s 4)))

(check-sat)
(get-value (s))

给出以下输出：

sat
((s "\x00\x00bbb\x00"))

我想知道相反的转换是否也存在？ 是否可以将一个字符串转换为 BitVec8？ 类似 str2bv 的东西：

(declare-const s String)
(declare-const someBV8 (_ BitVec 8))
(assert (= (str.len s) 6))

(assert (= someBV8 #x62))
(assert (= someBV8 (str2bv (str.at s 2))))
(assert (= someBV8 (str2bv (str.at s 3))))
(assert (= someBV8 (str2bv (str.at s 4))))

(check-sat)
(get-value (s))

【问题讨论】：

标签： string z3

【解决方案1】：

简短的回答是肯定的，但这既不容易也不是很有效。请参阅此处的讨论：https://github.com/Z3Prover/z3/issues/1302

如果这对您来说是个大问题，我建议您重新打开该票并提供一些反馈。这样，z3 人员可能会将所需的功能直接添加到 z3。

【讨论】：