floating-point - FMA : proof performance

Question

我正在试验新的 FP 逻辑。唉，即使是与 FMA 相关的最简单的查询似乎也会给 z3 带来不少麻烦。

下面是一个这样的例子，我试图证明 x*y+0 等于 fma(x,y,0)。它做了一些额外的事情来确保 x 和 y 不是 NaN 等，所以相等性确实成立。这个基准测试给 z3 带来这么多麻烦是有原因的吗？

我的 z3 版本:Z3 [版本 4.3.2 - 64 位 - 构建哈希码 728835357594]。

(set-option :produce-models true)
(set-logic QF_FPA)
(define-fun s3 () (_ FP  8 24) (as plusInfinity (_ FP 8 24)))
(define-fun s5 () (_ FP  8 24) (as minusInfinity (_ FP 8 24)))
(define-fun s17 () (_ FP  8 24) ((_ asFloat 8 24) roundNearestTiesToEven (/ 0 1)))
(declare-fun s0 () (_ FP  8 24))
(declare-fun s1 () (_ FP  8 24))
(assert
   (let ((s2 (== s0 s0)))
   (let ((s4 (< s0 s3)))
   (let ((s6 (> s0 s5)))
   (let ((s7 (and s4 s6)))
   (let ((s8 (and s2 s7)))
   (let ((s9 (== s1 s1)))
   (let ((s10 (< s1 s3)))
   (let ((s11 (> s1 s5)))
   (let ((s12 (and s10 s11)))
   (let ((s13 (and s9 s12)))
   (let ((s14 (and s8 s13)))
   (let ((s15 (not s14)))
   (let ((s16 (* roundNearestTiesToEven s0 s1)))
   (let ((s18 (+ roundNearestTiesToEven s16 s17)))
   (let ((s19 (fusedMA roundNearestTiesToEven s0 s1 s17)))
   (let ((s20 (== s18 s19)))
   (let ((s21 (or s15 s20)))
   (not s21)))))))))))))))))))
(check-sat)

Answer 1

Z3 通过将浮点公式转换为位向量公式(然后是 SAT)来求解浮点公式。有些方法在某些公式上比这更快(例如，基于 ACDCL 或某些形式的近似细化)，但在这个特定的公式上，我希望它们都表现出较差的性能。乘法(和类似的)约束对于底层引擎来说通常很难，证明乘法保留某些属性更难。