四舍五入的浮点数比较问题

Question

在基于 Z3 的分析器上工作（该分析器应该在 .net 中将双精度转换为 long/ulong 时检测溢出），我遇到了一个与浮点数相关的奇怪事情。

最后，我创建了一个小示例来说明问题：

两者：

(assert (= ((_ fp.to_sbv 64) roundTowardZero (fp #b0 #b10000111110 #x0000000000000)) #x8000000000000000))
(check-sat)

和：

(assert (not (= ((_ fp.to_sbv 64) roundTowardZero (fp #b0 #b10000111110 #x0000000000000)) #x8000000000000000)))
(check-sat)

给我sat.

一个四舍五入的浮点数怎么可能等于某个值，同时又可能不相等呢？

Answer 1

我假设您将这些断言与另一个断言分开，即您问 Z3 P 是否可满足，并且（分别）如果 ¬P 是可以满足的。这不同于询问 P ∧ ¬P 是否可满足。例如，假设 P 是 n = 0，对于某个整数 n。显然，n 可以是 1，在这种情况下 ¬(n = 0) 是满足的，并且n 可以是 0，这样 n = 0 就满足了。

Answer 2

浮点数常量的计算结果为

(-1)^0 * 2^(1086 - 1023) * (1 + 0) = 2^63

大小为 e 的 有符号位向量 可以容纳 [-2^(e-1), 2^(e-1) - 1] 范围内的值。因此，大小为 64 的 带符号位向量 的范围是 [-2^63, 2^63 - 1].

因为 2^63 超出了该范围，2^63 到大小 64 的 有符号位向量 的转换是 未定义:

In addition, fp.to_ubv and fp.to_sbv are unspecified for finite number inputs that are out of range (which includes all negative numbers for fp.to_ubv).

(source: SMT-LIB docs)

由于转换未定义，下面的表达式

((_ fp.to_sbv 64) roundTowardZero (fp #b0 #b10000111110 #x0000000000000))

可能有一个任意的、不受约束的、64 位位向量值。

这就解释了为什么可以发现相等性既是真又是假。

四舍五入的浮点数比较问题

Rounded floating-point number comparison issue

z3