z3 - Z3：FP和BitVector之间的转换？

Question

有没有办法在 SMTLIB2 中的 BitVector 和 FP 之间进行转换，比如 int2bv 和 bv2int 函数？

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

score 8 · Accepted Answer

准确地说，在 SMTLIB 中还没有浮点运算的标准。有一个草案将在稍后的时间点完成；本草案目前不包含此类功能。但是，Z3 在QF_FPABV启用逻辑时确实支持此类转换功能。

这些函数被称为

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)

1 回答 1