Average Error: 45.2 → 46.0
Time: 14.0s
Precision: 64
\[\mathsf{fma}\left(x, y, z\right) - \left(1 + \left(x \cdot y + z\right)\right)\]
↓
\[\mathsf{fma}\left(x, y, z\right) - \left(1 + \left(\left(x \cdot y\right) \cdot \left(x \cdot y\right) - z \cdot z\right) \cdot \frac{1}{x \cdot y - z}\right)\]
\mathsf{fma}\left(x, y, z\right) - \left(1 + \left(x \cdot y + z\right)\right)
↓
\mathsf{fma}\left(x, y, z\right) - \left(1 + \left(\left(x \cdot y\right) \cdot \left(x \cdot y\right) - z \cdot z\right) \cdot \frac{1}{x \cdot y - z}\right)
double f(double x, double y, double z) {
        double r65449 = x;
        double r65450 = y;
        double r65451 = z;
        double r65452 = fma(r65449, r65450, r65451);
        double r65453 = 1.0;
        double r65454 = r65449 * r65450;
        double r65455 = r65454 + r65451;
        double r65456 = r65453 + r65455;
        double r65457 = r65452 - r65456;
        return r65457;
}
↓
double f(double x, double y, double z) {
        double r65458 = x;
        double r65459 = y;
        double r65460 = z;
        double r65461 = fma(r65458, r65459, r65460);
        double r65462 = 1.0;
        double r65463 = r65458 * r65459;
        double r65464 = r65463 * r65463;
        double r65465 = r65460 * r65460;
        double r65466 = r65464 - r65465;
        double r65467 = 1.0;
        double r65468 = r65463 - r65460;
        double r65469 = r65467 / r65468;
        double r65470 = r65466 * r65469;
        double r65471 = r65462 + r65470;
        double r65472 = r65461 - r65471;
        return r65472;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original45.2
Target0
Herbie46.0
\[-1\]

Derivation

  1. Initial program 45.2

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

  3. Applied flip-+45.9

    \[\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-inv46.0

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

  6. Final simplification46.0

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

Reproduce

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

  :herbie-target
  -1

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