Average Error: 45.1 → 8.5
Time: 13.2s
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(z + y \cdot x\right)\right) - 1\]
\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(z + y \cdot x\right)\right) - 1
double f(double x, double y, double z) {
        double r3513075 = x;
        double r3513076 = y;
        double r3513077 = z;
        double r3513078 = fma(r3513075, r3513076, r3513077);
        double r3513079 = 1.0;
        double r3513080 = r3513075 * r3513076;
        double r3513081 = r3513080 + r3513077;
        double r3513082 = r3513079 + r3513081;
        double r3513083 = r3513078 - r3513082;
        return r3513083;
}
↓
double f(double x, double y, double z) {
        double r3513084 = x;
        double r3513085 = y;
        double r3513086 = z;
        double r3513087 = fma(r3513084, r3513085, r3513086);
        double r3513088 = r3513085 * r3513084;
        double r3513089 = r3513086 + r3513088;
        double r3513090 = r3513087 - r3513089;
        double r3513091 = 1.0;
        double r3513092 = r3513090 - r3513091;
        return r3513092;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original45.1
Target0
Herbie8.5
\[-1\]

Derivation

  1. Initial program 45.1

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

  3. Applied add-cube-cbrt45.6

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

  5. Applied *-un-lft-identity45.6

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

  6. Applied *-un-lft-identity45.6

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

  7. Applied distribute-lft-out--45.6

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

  8. Simplified8.5

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

  9. Final simplification8.5

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

Reproduce

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

  :herbie-target
  -1.0

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