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)