FMA:证明性能

Question

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

下面就是一个这样的例子，我试图证明x*y+0等于fma(x,y,0)。它做了一些额外的事情，以确保x和y不是NaNs，等等，所以这个等式确实有效。为什么这个基准会给z3带来这么多麻烦？

我的z3版本：Z3 [version 4.3.2 - 64 bit - build hashcode 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通过将浮点公式转换成位向量公式(然后再转换成位向量公式)来解决浮点公式.在某些公式(例如，基于ACDCL或某些形式的近似精化)上，有些方法比这更快，但对于这个特定的公式，我希望它们都表现出较差的性能。对于底层引擎来说，乘法(和类似的)约束通常是很难的，而证明乘法保留了一些属性甚至更难。