Z3：FP和BitVector之间的转换？答案

【问题标题】：Z3: Convert between FP and BitVector?Z3：FP和BitVector之间的转换？
【发布时间】：2013-05-30 16:20:15
【问题描述】：

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

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

【问题讨论】：

标签： z3

【解决方案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)

【讨论】：

本次更新：浮点SMT理论已定稿：smtlib.cs.uiowa.edu/theories/FloatingPoint.smt2 Z3 完全支持标准中的这些功能，并且所有以前的运算符都已删除。
链接已更改，这里是更新位置smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml