Average Error: 45.4 → 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 r4260056 = x;
        double r4260057 = y;
        double r4260058 = z;
        double r4260059 = fma(r4260056, r4260057, r4260058);
        double r4260060 = 1.0;
        double r4260061 = r4260056 * r4260057;
        double r4260062 = r4260061 + r4260058;
        double r4260063 = r4260060 + r4260062;
        double r4260064 = r4260059 - r4260063;
        return r4260064;
}
↓
double f(double x, double y, double z) {
        double r4260065 = x;
        double r4260066 = y;
        double r4260067 = z;
        double r4260068 = fma(r4260065, r4260066, r4260067);
        double r4260069 = r4260066 * r4260065;
        double r4260070 = r4260067 + r4260069;
        double r4260071 = r4260068 - r4260070;
        double r4260072 = 1.0;
        double r4260073 = r4260071 - r4260072;
        return r4260073;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original45.4
Target0
Herbie8.5
\[-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 add-cube-cbrt45.9

    \[\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.9

    \[\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.9

    \[\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.9

    \[\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 2019174 
(FPCore (x y z)
  :name "simple fma test"

  :herbie-target
  -1.0

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