Z3：在FP和BitVector之間轉換？

Question

有沒有什麼辦法可以在SMTLIB2中的BitVector和FP之間進行轉換，比如int2bv和bv2int函數？

爲了澄清，我正在尋找位的原始表示，而不是BitVec形式的舍入整數。

Answer 1

準確地說，SMTLIB中沒有浮點運算的標準。有一份草案將在稍後時間完成;該草案目前不包含這些職能。但是，當啓用QF_FPABV邏輯時，Z3確實支持這種轉換功能。

這些函數被稱爲

asIEEEBV (takes a float and returns a BV in IEEE764 format of appropriate size) 

和

fromIEEEBV (takes a BV in IEEE764 format and returns a float of appropriate size)