Average Error: 45.0 → 45.1
Time: 6.6s
Precision: binary64
\[\mathsf{fma}\left(x, y, z\right) - \left(1 + \left(x \cdot y + z\right)\right)\]
↓
\[\mathsf{fma}\left(x, y, z\right) + \frac{-1}{\frac{1}{1 + \left(z + x \cdot y\right)}}\]
\mathsf{fma}\left(x, y, z\right) - \left(1 + \left(x \cdot y + z\right)\right)
↓
\mathsf{fma}\left(x, y, z\right) + \frac{-1}{\frac{1}{1 + \left(z + x \cdot y\right)}}
(FPCore (x y z) :precision binary64 (- (fma x y z) (+ 1.0 (+ (* x y) z))))
↓
(FPCore (x y z)
 :precision binary64
 (+ (fma x y z) (/ -1.0 (/ 1.0 (+ 1.0 (+ z (* x y)))))))
double code(double x, double y, double z) {
	return ((double) (((double) fma(x, y, z)) - ((double) (1.0 + ((double) (((double) (x * y)) + z))))));
}
↓
double code(double x, double y, double z) {
	return ((double) (((double) fma(x, y, z)) + (-1.0 / (1.0 / ((double) (1.0 + ((double) (z + ((double) (x * y))))))))));
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original45.0
Target0
Herbie45.1
\[-1\]

Derivation

  1. Initial program 45.0

    \[\mathsf{fma}\left(x, y, z\right) - \left(1 + \left(x \cdot y + z\right)\right)\]
  2. Using strategy rm

  3. Applied flip-+45.7

    \[\leadsto \mathsf{fma}\left(x, y, z\right) - \color{blue}{\frac{1 \cdot 1 - \left(x \cdot y + z\right) \cdot \left(x \cdot y + z\right)}{1 - \left(x \cdot y + z\right)}}\]

  4. Simplified45.7

    \[\leadsto \mathsf{fma}\left(x, y, z\right) - \frac{\color{blue}{1 \cdot 1 - \left(z + x \cdot y\right) \cdot \left(z + x \cdot y\right)}}{1 - \left(x \cdot y + z\right)}\]

  5. Simplified45.7

    \[\leadsto \mathsf{fma}\left(x, y, z\right) - \frac{1 \cdot 1 - \left(z + x \cdot y\right) \cdot \left(z + x \cdot y\right)}{\color{blue}{1 - \left(z + x \cdot y\right)}}\]
  6. Using strategy rm

  7. Applied clear-num45.8

    \[\leadsto \mathsf{fma}\left(x, y, z\right) - \color{blue}{\frac{1}{\frac{1 - \left(z + x \cdot y\right)}{1 \cdot 1 - \left(z + x \cdot y\right) \cdot \left(z + x \cdot y\right)}}}\]

  8. Simplified45.1

    \[\leadsto \mathsf{fma}\left(x, y, z\right) - \frac{1}{\color{blue}{\frac{1}{1 + \left(z + x \cdot y\right)}}}\]

  9. Final simplification45.1

    \[\leadsto \mathsf{fma}\left(x, y, z\right) + \frac{-1}{\frac{1}{1 + \left(z + x \cdot y\right)}}\]

Reproduce

herbie shell --seed 2020198 
(FPCore (x y z)
  :name "simple fma test"
  :precision binary64

  :herbie-target
  -1.0

  (- (fma x y z) (+ 1.0 (+ (* x y) z))))