Average Error: 45.4 → 45.4
Time: 13.6s
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) - 1\right) - \left(x \cdot y + z\right)\]
\mathsf{fma}\left(x, y, z\right) - \left(1 + \left(x \cdot y + z\right)\right)
↓
\left(\mathsf{fma}\left(x, y, z\right) - 1\right) - \left(x \cdot y + z\right)
double f(double x, double y, double z) {
        double r45030 = x;
        double r45031 = y;
        double r45032 = z;
        double r45033 = fma(r45030, r45031, r45032);
        double r45034 = 1.0;
        double r45035 = r45030 * r45031;
        double r45036 = r45035 + r45032;
        double r45037 = r45034 + r45036;
        double r45038 = r45033 - r45037;
        return r45038;
}
↓
double f(double x, double y, double z) {
        double r45039 = x;
        double r45040 = y;
        double r45041 = z;
        double r45042 = fma(r45039, r45040, r45041);
        double r45043 = 1.0;
        double r45044 = r45042 - r45043;
        double r45045 = r45039 * r45040;
        double r45046 = r45045 + r45041;
        double r45047 = r45044 - r45046;
        return r45047;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

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

Derivation

  1. Initial program 45.4

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

  3. Applied associate--r+45.4

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

  4. Final simplification45.4

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

Reproduce

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

  :herbie-target
  -1

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