z3 - Z3: FP と BitVector の間で変換しますか?

Question

int2bv 関数と bv2int 関数のような、SMTLIB2 で BitVector と FP の間で変換する方法はありますか?

明確にするために、BitVec形式の丸められた整数などではなく、ビットの生の表現を探しています。