z3 - Z3 将“小”位向量转换为整数

Question

我知道bv2int和int2bv在 Z3 中都作为未解释的函数处理。尽管如此，我仍在寻找解决以下问题的最佳实践：给定一个“小”（< 10 位）位向量索引，如何有效地将其转换为 Int，并在这样的查询中使用：

(declare-const s String)
(declare-const someInt                Int)
(declare-const someBitVec10 (_ BitVec 10))

(assert (= s "74g\x00!!#2#$$"))

;(assert (str.in.re (str.at s someBitVec10) (re.range "a" "z")))
( assert (str.in.re (str.at s someInt     ) (re.range "1" "3")))

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

输出：

sat
((s "74g\x00!!#2#$$")
 (someInt 7))

谢谢！