simple fma test

Average Error: 44.9 → 8.3

Time: 6.5s

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

C

double f(double x, double y, double z) {
        double r107559 = x;
        double r107560 = y;
        double r107561 = z;
        double r107562 = fma(r107559, r107560, r107561);
        double r107563 = 1.0;
        double r107564 = r107559 * r107560;
        double r107565 = r107564 + r107561;
        double r107566 = r107563 + r107565;
        double r107567 = r107562 - r107566;
        return r107567;
}

↓

double f(double x, double y, double z) {
        double r107568 = x;
        double r107569 = y;
        double r107570 = z;
        double r107571 = fma(r107568, r107569, r107570);
        double r107572 = r107568 * r107569;
        double r107573 = r107572 + r107570;
        double r107574 = r107571 - r107573;
        double r107575 = 1.0;
        double r107576 = r107574 - r107575;
        return r107576;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	44.9
Target	0
Herbie	8.3

\[-1\]

Derivation

1. Initial program 44.9

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

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

   \[\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 *-un-lft-identity 45.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 \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. Applied *-un-lft-identity 45.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 \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. 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 \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)}\]

10. Simplified 8.3

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

11. Final simplification 8.3

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

Reproduce

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

  :herbie-target
  -1

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