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)