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)