simple fma test

Average Error: 45.0 → 44.2

Time: 17.8s

Precision: 64

Math

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

↓

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

C

double f(double x, double y, double z) {
        double r3747251 = x;
        double r3747252 = y;
        double r3747253 = z;
        double r3747254 = fma(r3747251, r3747252, r3747253);
        double r3747255 = 1.0;
        double r3747256 = r3747251 * r3747252;
        double r3747257 = r3747256 + r3747253;
        double r3747258 = r3747255 + r3747257;
        double r3747259 = r3747254 - r3747258;
        return r3747259;
}

↓

double f(double x, double y, double z) {
        double r3747260 = x;
        double r3747261 = y;
        double r3747262 = z;
        double r3747263 = fma(r3747260, r3747261, r3747262);
        double r3747264 = r3747260 * r3747261;
        double r3747265 = r3747264 + r3747262;
        double r3747266 = 1.0;
        double r3747267 = r3747265 + r3747266;
        double r3747268 = cbrt(r3747267);
        double r3747269 = cbrt(r3747268);
        double r3747270 = r3747269 * r3747269;
        double r3747271 = r3747269 * r3747270;
        double r3747272 = r3747271 * r3747268;
        double r3747273 = r3747271 * r3747272;
        double r3747274 = r3747263 - r3747273;
        double r3747275 = /* ERROR: no posit support in C */;
        double r3747276 = /* ERROR: no posit support in C */;
        return r3747276;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	45.0
Target	0
Herbie	44.2

\[-1\]

Derivation

1. Initial program 45.0

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

3. Applied insert-posit16 45.0

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

5. Applied add-cube-cbrt 44.2

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

7. Applied add-cube-cbrt 44.2

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

9. Applied add-cube-cbrt 44.2

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

10. Final simplification 44.2

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

Reproduce

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

  :herbie-target
  -1

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