simple fma test

Average Error: 45.2 → 31.4

Time: 8.8s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

Math

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

↓

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

C

double f(double x, double y, double z) {
        double r125686 = x;
        double r125687 = y;
        double r125688 = z;
        double r125689 = fma(r125686, r125687, r125688);
        double r125690 = 1.0;
        double r125691 = r125686 * r125687;
        double r125692 = r125691 + r125688;
        double r125693 = r125690 + r125692;
        double r125694 = r125689 - r125693;
        return r125694;
}

↓

double f(double x, double y, double z) {
        double r125695 = x;
        double r125696 = y;
        double r125697 = z;
        double r125698 = fma(r125695, r125696, r125697);
        double r125699 = r125698 - r125697;
        double r125700 = r125695 * r125696;
        double r125701 = 1.0;
        double r125702 = r125700 + r125701;
        double r125703 = r125699 - r125702;
        double r125704 = cbrt(r125703);
        double r125705 = r125704 * r125704;
        double r125706 = r125705 * r125704;
        return r125706;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	45.2
Target	0
Herbie	31.4

\[-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 add-cube-cbrt 45.8

   \[\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 add-cube-cbrt 45.8

   \[\leadsto \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 \color{blue}{\left(\left(\sqrt[3]{\sqrt[3]{x \cdot y + z}} \cdot \sqrt[3]{\sqrt[3]{x \cdot y + z}}\right) \cdot \sqrt[3]{\sqrt[3]{x \cdot y + z}}\right)}\right)\]
6. Using strategy rm

7. Applied add-cube-cbrt 45.8

   \[\leadsto \color{blue}{\left(\sqrt[3]{\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 \left(\left(\sqrt[3]{\sqrt[3]{x \cdot y + z}} \cdot \sqrt[3]{\sqrt[3]{x \cdot y + z}}\right) \cdot \sqrt[3]{\sqrt[3]{x \cdot y + z}}\right)\right)} \cdot \sqrt[3]{\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 \left(\left(\sqrt[3]{\sqrt[3]{x \cdot y + z}} \cdot \sqrt[3]{\sqrt[3]{x \cdot y + z}}\right) \cdot \sqrt[3]{\sqrt[3]{x \cdot y + z}}\right)\right)}\right) \cdot \sqrt[3]{\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 \left(\left(\sqrt[3]{\sqrt[3]{x \cdot y + z}} \cdot \sqrt[3]{\sqrt[3]{x \cdot y + z}}\right) \cdot \sqrt[3]{\sqrt[3]{x \cdot y + z}}\right)\right)}}\]

8. Simplified 45.6

   \[\leadsto \color{blue}{\left(\sqrt[3]{\left(\mathsf{fma}\left(x, y, z\right) - z\right) - \left(x \cdot y + 1\right)} \cdot \sqrt[3]{\left(\mathsf{fma}\left(x, y, z\right) - z\right) - \left(x \cdot y + 1\right)}\right)} \cdot \sqrt[3]{\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 \left(\left(\sqrt[3]{\sqrt[3]{x \cdot y + z}} \cdot \sqrt[3]{\sqrt[3]{x \cdot y + z}}\right) \cdot \sqrt[3]{\sqrt[3]{x \cdot y + z}}\right)\right)}\]

9. Simplified 31.4

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

10. Final simplification 31.4

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

Reproduce

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

  :herbie-target
  -1

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