Average Error: 45.7 → 46.1
Time: 4.7s
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 + \left(x \cdot y\right) \cdot \frac{x \cdot y}{x \cdot y - z}\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 + \left(x \cdot y\right) \cdot \frac{x \cdot y}{x \cdot y - z}\right)\right) + \frac{z \cdot z}{x \cdot y - z}
double f(double x, double y, double z) {
        double r64550 = x;
        double r64551 = y;
        double r64552 = z;
        double r64553 = fma(r64550, r64551, r64552);
        double r64554 = 1.0;
        double r64555 = r64550 * r64551;
        double r64556 = r64555 + r64552;
        double r64557 = r64554 + r64556;
        double r64558 = r64553 - r64557;
        return r64558;
}
↓
double f(double x, double y, double z) {
        double r64559 = x;
        double r64560 = y;
        double r64561 = z;
        double r64562 = fma(r64559, r64560, r64561);
        double r64563 = 1.0;
        double r64564 = r64559 * r64560;
        double r64565 = r64564 - r64561;
        double r64566 = r64564 / r64565;
        double r64567 = r64564 * r64566;
        double r64568 = r64563 + r64567;
        double r64569 = r64562 - r64568;
        double r64570 = r64561 * r64561;
        double r64571 = r64570 / r64565;
        double r64572 = r64569 + r64571;
        return r64572;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original45.7
Target0
Herbie46.1
\[-1\]

Derivation

  1. Initial program 45.7

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

  3. Applied flip-+46.4

    \[\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-sub46.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-46.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-46.4

    \[\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 *-un-lft-identity46.4

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

  10. Applied times-frac46.1

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

  11. Simplified46.1

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

  12. Final simplification46.1

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

Reproduce

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

  :herbie-target
  -1

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