恐怕您误解了这些功能的作用。在使用SMTLib浮子时保持打开的一个很好的参考是：http ://smtlib.cs.uiowa.edu/papers/BTRW15.pdf

mk_fpa_to_ubv

此功能与FPToUInt引用的论文中的功能相对应。它的定义如下：

（上面的NaN选项具有误导性：应将其读取为“ undefined”。）

请注意，根据FP值和向量的位宽，此处的精度损失可能很大。想象一下将双精度浮点值转换为8位字：您正在将±2.23×10 ^ −308到±1.80×10 ^ 308的范围内的值粉碎为仅256个不同的值。这意味着大量转换将直接进行大量舍入取消。

您应该将其视为类似C的语言中的“广播”：

unsigned char c;
double f;
c = (char) f;

这是从双精度到无符号字节的转换的本质，这将导致严重的精度损失。在另一个方向上，如果您转换为一个很大的位向量（例如具有一千个位的位向量），则尽管四舍五入的方式可以覆盖所有整数值，但转换仍将失去舍入精度。恰好在范围内。因此，这实际上取决于您要转换为哪种BV类型以及您选择的舍入模式。

mk_fpa_to_ieee_bv

此功能与“保留”值无关。因此，在这里询问“精度损失”是无关紧要的。它的作用是按照IEEE-754规范为您提供浮点值的基础位向量表示。维基百科文章对此表示形式进行了很好的讨论：https : //en.wikipedia.org/wiki/Double-precision_floating-point_format#IEEE_754_double-precision_binary_floating-point_format : _binary64

特别是，如果将此函数的输出解释为二进制补码整数值，则会得到一个完全无关的值，该值与浮点数本身的值无关。（此外，此转换不是唯一的，因为NaN具有多个对应的位向量模式。）

概要

长话短说，从浮点数到位向量的转换不仅会因为舍入而损失“小数”部分，还会由于范围有限而遭受精度损失，除非您选择非常大的位向量大小。的IEEE-754表示转换并不保留值，并因此这样做算术上的值转换从这个功能是或多或少毫无意义。