Z3 -浮点算术API函数Z3_mk_fpa_to_ubv

Question

我是第一次玩Z3-4.6.0 C++。抱歉让我问你这些问题。

我的问题有两部分。

如果我有一个浮点数，并使用Z3_mk_fpa_to_ubv(...)函数创建一个无符号位向量。

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

我知道我可以使用Z3_mk_fpa_to_ieee_bv(....)进行优雅的和IEEE-754兼容的转换。之后，我可以添加，子等位向量。

只是好奇而已。

非常感谢。

Answer 1

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

mk_fpa_to_ubv

这个函数对应于引用文献中的FPToUInt函数。它的定义如下：

​

​

(上面的NaN选项具有误导性:应该将其理解为“未定义”)。

请注意，这里的精度损失可能很大，取决于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规范给出浮点值的基本位向量表示。维基百科的文章很好地讨论了这种表示形式：binary64

特别是，如果将此函数的输出解释为2的补整数值，您将得到一个与浮点数本身的值无关的完全无关的值。(而且，这种转换并不是唯一的，因为NaN有多个对应的位向量模式。)

摘要

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