Average Error: 64.0 → 0.3
Time: 2.3s
Precision: binary64
\[1.9 \leq t \land t \leq 2.1\]
\[1.7 \cdot 10^{+308} \cdot t - 1.7 \cdot 10^{+308} \]
↓
\[\mathsf{fma}\left(1.7 \cdot 10^{+308}, t, -1.7 \cdot 10^{+308}\right) \]
1.7 \cdot 10^{+308} \cdot t - 1.7 \cdot 10^{+308}
↓
\mathsf{fma}\left(1.7 \cdot 10^{+308}, t, -1.7 \cdot 10^{+308}\right)

(FPCore (t) :precision binary64 (- (* 1.7e+308 t) 1.7e+308))
↓
(FPCore (t) :precision binary64 (fma 1.7e+308 t -1.7e+308))
double code(double t) {
	return (1.7e+308 * t) - 1.7e+308;
}
↓
double code(double t) {
	return fma(1.7e+308, t, -1.7e+308);
}

Error

Bits error versus t

Target

Original64.0
Target0.3
Herbie0.3
\[\mathsf{fma}\left(1.7 \cdot 10^{+308}, t, -1.7 \cdot 10^{+308}\right) \]

Derivation

  1. Initial program 64.0

    \[1.7 \cdot 10^{+308} \cdot t - 1.7 \cdot 10^{+308} \]

  2. Simplified0.3

    \[\leadsto \color{blue}{\mathsf{fma}\left(1.7 \cdot 10^{+308}, t, -1.7 \cdot 10^{+308}\right)} \]

  3. Final simplification0.3

    \[\leadsto \mathsf{fma}\left(1.7 \cdot 10^{+308}, t, -1.7 \cdot 10^{+308}\right) \]

Reproduce

herbie shell --seed 2022125 
(FPCore (t)
  :name "fma_test2"
  :precision binary64
  :pre (and (<= 1.9 t) (<= t 2.1))

  :herbie-target
  (fma 1.7e+308 t (- 1.7e+308))

  (- (* 1.7e+308 t) 1.7e+308))