Z3: Convert between FP and BitVector?

问题:

Is there any way to convert between BitVector and FP in SMTLIB2, something like the int2bv and bv2int functions?

To clarify, I am looking for a raw representation of the bits, not e.g., a rounded integer in BitVec form.

回答1:

To be precise, there is no standard for floating point arithmetic in SMTLIB yet. There is a draft for this which will be finalized at a later point in time; this draft does not contain such functions at the moment. However, Z3 does support such conversion functions when the QF_FPABV logic is enabled.

These functions are called

asIEEEBV (takes a float and returns a BV in IEEE764 format of appropriate size)

and

fromIEEEBV (takes a BV in IEEE764 format and returns a float of appropriate size)