simple fma test

Average Error: 45.2 → 45.1

Time: 19.2s

Precision: 64

Math

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

↓

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

C

double f(double x, double y, double z) {
        double r3076897 = x;
        double r3076898 = y;
        double r3076899 = z;
        double r3076900 = fma(r3076897, r3076898, r3076899);
        double r3076901 = 1.0;
        double r3076902 = r3076897 * r3076898;
        double r3076903 = r3076902 + r3076899;
        double r3076904 = r3076901 + r3076903;
        double r3076905 = r3076900 - r3076904;
        return r3076905;
}

↓

double f(double x, double y, double z) {
        double r3076906 = -1.0;
        double r3076907 = y;
        double r3076908 = x;
        double r3076909 = r3076907 * r3076908;
        double r3076910 = r3076906 - r3076909;
        double r3076911 = z;
        double r3076912 = fma(r3076908, r3076907, r3076911);
        double r3076913 = r3076910 + r3076912;
        double r3076914 = r3076913 - r3076911;
        double r3076915 = cbrt(r3076914);
        double r3076916 = r3076915 * r3076915;
        double r3076917 = r3076915 * r3076916;
        return r3076917;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Target

Original	45.2
Target	0
Herbie	45.1

\[-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 flip-+ 45.6

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

4. Simplified 45.5

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

6. Applied clear-num 45.6

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

7. Simplified 45.3

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

9. Applied *-un-lft-identity 45.3

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

10. Applied *-un-lft-identity 45.3

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

11. Applied distribute-lft-out 45.3

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

12. Applied *-un-lft-identity 45.3

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

13. Applied distribute-lft-out-- 45.3

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

14. Simplified 45.1

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

16. Applied add-cube-cbrt 45.1

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

17. Final simplification 45.1

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

Reproduce

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

  :herbie-target
  -1

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