舍入浮点数比较问题

Question

在一个基于Z3的分析器上工作(这个分析器应该在.net中将doubles转换为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)

给我CCD_ 1。

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

Answer 1

浮点常量的求值结果为

(-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的有符号位向量的转换是未定义：

此外，对于超出范围的有限数输入(包括sat1的所有负数(，未指定fp.to_ubv和fp.to_sbv。

(来源：SMT-LIB文档(

由于转换未定义，因此以下表达式

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

可以具有任意的、不受约束的64位位矢量值。

这就解释了为什么等式可以被发现是真的和假的。

Answer 2

我假设你分别做出了另一个断言，即你问Z3p是否可满足，以及(分别(-p何时可满足。这与询问P∧-P是否可满足不同。例如，假设P是n=0，对于某个整数n。显然，n可以是1，在这种情况下满足-(n=0(；n可能是0。