c++ - Z3 - 浮点运算 API 函数 Z3_mk_fpa_to_ubv

Question

我是第一次玩 Z3-4.6.0 C++。对于菜鸟问题​​，我们深表歉意。

我的问题分为两部分。

如果我有一个 float ，并且我使用 Z3_mk_fpa_to_ubv(...) 函数来创建一个无符号位 vector 。

1. 损失了多少精度？
2. 如果精度没有丢失，我是否可以将这个新的无符号位 vector 用作常规位 vector 并应用为其定义的所有操作，例如 Z3_mk_bvadd(....)？

我知道我可以使用 Z3_mk_fpa_to_ieee_bv(....) 进行优雅且符合 IEEE-754 的转换。之后我可以添加、子等位 vector 。

只是好奇。

非常感谢。

Answer 1

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

mk_fpa_to_ubv

此函数对应于引用论文中的FPToUInt 函数。定义如下:

(上面的 NaN 选择具有误导性:它应该被读作“未定义”。)

请注意，这里的精度损失可能很大，具体取决于 FP 值和 vector 的位宽。想象一下将一个 double 浮点值转换为一个 8 位字:您将 ±2.23×10^−308 到 ±1.80×10^308 范围内的值粉碎为仅仅 256 个不同的值。这意味着大量转化将简单地经过大量舍入取消。

您应该将其视为 C 类语言中的“转换”:

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

这就是 double 到无符号字节转换的本质，会损失很大的精度。在另一个方向上，如果你转换为一个非常大的位 vector (比如一个有千位的位 vector )，那么你的转换仍然会根据舍入模式失去精度，尽管你将能够覆盖所有整数值恰好在范围内。因此，这实际上取决于您转换为何种 BV 类型以及您选择的舍入模式。

mk_fpa_to_ieee_bv

此功能与“保留”值无关。所以在这里问“精度损失”是无关紧要的。它的作用是根据 IEEE-754 规范为您提供浮点值的底层位 vector 表示。维基百科文章对此表示进行了很好的讨论:https://en.wikipedia.org/wiki/Double-precision_floating-point_format#IEEE_754_double-precision_binary_floating-point_format:_binary64

特别是，如果您将此函数的输出解释为二进制补码整数值，您将得到一个与 float 本身的值无关的完全不相关的值。 (此外，这种转换不是唯一的，因为 NaN 有多个对应的位 vector 模式。)

总结

长话短说，从 float 到位 vector 的转换将遭受精度损失，这不仅是因为舍入导致“小数”部分丢失，而且还因为范围有限，除非您选择非常大的位- vector 大小。 IEEE-754 表示转换不保留值，因此对通过此函数转换的值进行算术或多或少没有意义。