Average Error: 44.8 → 45.2
Time: 15.5s
Precision: 64
\[\mathsf{fma}\left(x, y, z\right) - \left(1 + \left(x \cdot y + z\right)\right)\]
↓
\[\left(\mathsf{fma}\left(x, y, z\right) - \left(1 + \frac{1}{\frac{1 - \frac{z}{x \cdot y}}{x \cdot y}}\right)\right) + \frac{z \cdot z}{x \cdot y - z}\]
\mathsf{fma}\left(x, y, z\right) - \left(1 + \left(x \cdot y + z\right)\right)
↓
\left(\mathsf{fma}\left(x, y, z\right) - \left(1 + \frac{1}{\frac{1 - \frac{z}{x \cdot y}}{x \cdot y}}\right)\right) + \frac{z \cdot z}{x \cdot y - z}
double f(double x, double y, double z) {
        double r82372 = x;
        double r82373 = y;
        double r82374 = z;
        double r82375 = fma(r82372, r82373, r82374);
        double r82376 = 1.0;
        double r82377 = r82372 * r82373;
        double r82378 = r82377 + r82374;
        double r82379 = r82376 + r82378;
        double r82380 = r82375 - r82379;
        return r82380;
}
↓
double f(double x, double y, double z) {
        double r82381 = x;
        double r82382 = y;
        double r82383 = z;
        double r82384 = fma(r82381, r82382, r82383);
        double r82385 = 1.0;
        double r82386 = 1.0;
        double r82387 = r82381 * r82382;
        double r82388 = r82383 / r82387;
        double r82389 = r82386 - r82388;
        double r82390 = r82389 / r82387;
        double r82391 = r82386 / r82390;
        double r82392 = r82385 + r82391;
        double r82393 = r82384 - r82392;
        double r82394 = r82383 * r82383;
        double r82395 = r82387 - r82383;
        double r82396 = r82394 / r82395;
        double r82397 = r82393 + r82396;
        return r82397;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original44.8
Target0
Herbie45.2
\[-1\]

Derivation

  1. Initial program 44.8

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

  3. Applied flip-+45.5

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

  5. Applied div-sub45.5

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

  6. Applied associate-+r-45.5

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

  7. Applied associate--r-45.5

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

  9. Applied clear-num45.5

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

  10. Simplified45.2

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

  11. Final simplification45.2

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

Reproduce

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

  :herbie-target
  -1

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