FMA: proof of performance
I am experimenting with new FP logic. Alas, even the simplest FMA queries seem to cause a lot of problems for the z3.
Below is one such example where I was trying to prove that x*y+0
is equal fma(x,y,0)
. It does a few additional things to make sure that x
and y
are not NaN
s and so on, so the equality will indeed be satisfied. Is there a reason this criterion is causing so many problems for z3
?
My version 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)
source to share
Z3 solves floating point formulas by translating them into bit vector formulas (and then SAT). There are some methods that are faster than this in some formulas (like ACDCL or some form of approximation), but on this particular formula, I would expect them all to perform poorly. Multiplication (and similar) constraints are usually difficult for the underlying engine, and proving that multiplication preserves a property is even more difficult.
source to share