4

Z3 为该基准返回了一个令人满意的模型：http ://rise4fun.com/Z3/Bnv5m

但是，该查询本质上是断言a*b+0等同于a*b使用 FMA 指令，我相信它适用于 IEEE 浮点数。请注意，基准明确确保既不是a也不b是NaN。

我的 FMA 编码有问题吗？

4

2 回答 2

3

看起来他们的(fusedMA <mode> foo bar baz)回报foo*bar/2 + baz。当参数或结果不正常时，无论是在定理证明器中还是在实际的融合乘加中，似乎都会发生一些奇怪的事情。

我运行它以查看它认为有问题的产品和 FMA 是什么：

(set-logic QF_FPA)
; s7 is equivalent to single-precision +0
(define-fun s7 () (_ FP  8 24) ((_ asFloat 8 24) roundNearestTiesToEven (/ 0 1)))
(declare-fun s0 () (_ FP  8 24))
(declare-fun s1 () (_ FP  8 24))
(declare-fun prod () (_ FP  8 24))
(declare-fun fma () (_ FP  8 24))
(assert
   (let ((s2 (== s0 s0)))     ; make sure s0 is not NaN
   (let ((s3 (== s1 s1)))     ; make sure s1 is not NaN
   (let ((s4 (and s2 s3)))
   (let ((s5 (not s4)))       ; s5 is True when either argument is NaN
   (let ((s6 (* roundNearestTiesToEven s0 s1)))            ; s6 = s0*s1
   (let ((s8 (fusedMA roundNearestTiesToEven s0 s1 s7)))   ; s8 = s0*s1 + s7 = s0*s1 since s7 is 0
   (let ((s9 (== s6 s8)))     ; s9 should always be true provided arguments are not NaN  
   (let ((s10 (or s5 s9)))    ; thus; s10 is true always
   (and (== fma s8) (== prod s6) (not s10)))))))))))         ; hence, the whole expression is unsatisfiable
(check-sat)
(get-model)

得到了这个：

sat
(model
  (define-fun prod () (_ FP 8 24) (as -1.0572719573974609375p-9 (_ FP 8 24)))
  (define-fun fma () (_ FP 8 24) (as -1.0572719573974609375p-10 (_ FP 8 24)))
  (define-fun s1 () (_ FP 8 24) (as +1.62525212764739990234375p118 (_ FP 8 24)))
  (define-fun s0 () (_ FP 8 24) (as -0.0101644992828369140625p-126 (_ FP 8 24)))
)

产品和 FMA 都没有真正符合 -2 -14的内容，这令人讨厌。

如果你限制prod和fma低于 2 -125，你可以得到这样的东西：

sat
(model
  (define-fun prod () (_ FP 8 24) (as +1.52807605266571044921875p-3 (_ FP 8 24))) 
  (define-fun fma () (_ FP 8 24) (as +1.528076171875p-3 (_ FP 8 24)))
  (define-fun s1 () (_ FP 8 24) (as -0.0002593994140625p-126 (_ FP 8 24)))
  (define-fun s0 () (_ FP 8 24) (as -1.4381892681121826171875p125 (_ FP 8 24)))
)

如果您还限制s0和s1低于 2 -125，它会返回unsat。

于 2013-04-08T04:53:11.353 回答
3

是的，FMA 目前有问题。上周五，我对其他指令进行了一些修复，但还没有着手修复 FMA。感谢报告，尤其是测试用例，尤其是在 FMA 的情况下，这是非常宝贵的帮助！

于 2013-04-08T10:14:24.153 回答