Z3ソート変換：（1文字）文字列から（長さ8）ビットベクトル

Question

extracting the decimal value from a Z3 stringについては、以前の質問から、は、BitVec8を1文字列に変換することが可能です。たとえば、次のクエリ実行中：

(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")) 

私は逆の変換があまりにも存在するかどうかを知りたいと思いましたか？ 1つの文字列を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)) 

Answer 1

短い答えはイエスですが、それは簡単でも非常に効果的でもないのです。 https://github.com/Z3Prover/z3/issues/1302

これはショーストッパーであれば、そのチケットを再度開いてフィードバックをお伝えください。そうすれば、z3の人々は必要な機能をz3に直接追加することができます。