Z3: семантика FMA с плавающей точкой

Z3 возвращает удовлетворительную модель для этого бенчмарка: http://rise4fun.com/Z3/Bnv5m

Однако запрос по существу утверждает, что a*b+0 эквивалентно a*b с использованием инструкции FMA, которая, как я полагаю, выполняется для чисел с плавающей запятой IEEE. Обратите внимание, что бенчмарк явно гарантирует, что ни a, ни b не являются NaN.

Есть ли проблема в моем кодировании FMA?

2 4
floating-point ieee-754

2 ответа:

Да, FMA в настоящее время глючит. Я сделал несколько исправлений для других инструкций в прошлую пятницу, но еще не удосужился исправить FMA. Спасибо за отчет и особенно за тестовый кейс, особенно в случае с FMA это неоценимая помощь!

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.

3