是（x – x）对于双打总是正的零，或者有时是负的零？
当x是double +0.0 ， (x - x)保证为+0.0 ，或者有时可能为-0.0 （取决于x的符号）？
x - x可以是+0.0或NaN 。 在IEEE 754algorithm中没有其他值可以在最近（在Java中，舍入模式总是舍入到最近 ） 算出 。 两个相同有限值的减法定义为在该舍入模式下产生+0.0 。 马克·迪金森 （ Mark Dickinson ）在下面的评论中引用了IEEE 754标准，如第6.3节所述：
当两个符号相反的操作数之和（或者两个操作数与相同符号的差值）恰好为零时，除了roundToward负数之外，所有圆angular方向属性的和（或差）的符号应为+0。 。
此页面显示特别是0.0 - 0.0和-0.0 - (-0.0) 0.0 - 0.0 -0.0 - (-0.0)都是+0.0 。
Infinities和NaN都从NaN中减去NaN。
SMT解算器Z3支持IEEE浮点运算。 让我们问Z3findx - x != 0 。 它立即发现NaN以及+-infinity 。 不包括那些，没有x满足那个等式。
(set-logic QF_FPA) (declare-const x (_ FP 11 53)) (declare-const r (_ FP 11 53)) (assert (and (not (= x (as NaN (_ FP 11 53)))) (not (= x (as plusInfinity (_ FP 11 53)))) (not (= x (as minusInfinity (_ FP 11 53)))) (= r (- roundTowardZero xx)) (not (= r ((_ asFloat 11 53) roundTowardZero 0.0 0))) )) (check-sat) (get-model)
Z3通过将所有操作转换为布尔逻辑电路并使用标准的SAT求解器来find一个模型来实现IEEE浮点运算。 除了在翻译或SAT求解器中的任何错误，结果都是非常精确的。
certificate…
- …
roundTowardZero： http：roundTowardZero - …
roundNearestTiesToEven： http:roundNearestTiesToEven
请注意舍入模式roundTowardNegative的反例： http: roundTowardNegative 。 对于某个x ， x - x x的结果是负的零。 这种情况很难被人发现。 然而，用SMT解算器很容易find。 我们可以将=改为==以便Z3使用IEEE相等比较语义而不是精确的相等。 在这个变化之后，再没有反例，因为根据IEEE的-0 == +0 。
我试图把舍入模式变成一个variables。 这将理论上工作，但Z3有一个错误在这里。 现在我们必须手动指定一个硬编码的舍入模式。 如果我们可以把它作为一个variables，我们可以要求Z3在一个查询中certificate所有舍入模式的声明。
