Average Error: 0.0 → 0.0
Time: 10.5s
Precision: 64
\[x.re \cdot y.re - x.im \cdot y.im\]
↓
\[\mathsf{fma}\left(x.im, -y.im, x.re \cdot y.re\right)\]
x.re \cdot y.re - x.im \cdot y.im
↓
\mathsf{fma}\left(x.im, -y.im, x.re \cdot y.re\right)
double f(double x_re, double x_im, double y_re, double y_im) {
        double r59862 = x_re;
        double r59863 = y_re;
        double r59864 = r59862 * r59863;
        double r59865 = x_im;
        double r59866 = y_im;
        double r59867 = r59865 * r59866;
        double r59868 = r59864 - r59867;
        return r59868;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r59869 = x_im;
        double r59870 = y_im;
        double r59871 = -r59870;
        double r59872 = x_re;
        double r59873 = y_re;
        double r59874 = r59872 * r59873;
        double r59875 = fma(r59869, r59871, r59874);
        return r59875;
}

Error

Bits error versus x.re

Bits error versus x.im

Bits error versus y.re

Bits error versus y.im

Derivation

  1. Initial program 0.0

    \[x.re \cdot y.re - x.im \cdot y.im\]
  2. Using strategy rm

  3. Applied add-sqr-sqrt31.1

    \[\leadsto \color{blue}{\sqrt{x.re \cdot y.re - x.im \cdot y.im} \cdot \sqrt{x.re \cdot y.re - x.im \cdot y.im}}\]
  4. Using strategy rm

  5. Applied add-sqr-sqrt31.1

    \[\leadsto \sqrt{x.re \cdot y.re - x.im \cdot y.im} \cdot \sqrt{\color{blue}{\sqrt{x.re \cdot y.re - x.im \cdot y.im} \cdot \sqrt{x.re \cdot y.re - x.im \cdot y.im}}}\]

  6. Applied sqrt-prod31.2

    \[\leadsto \sqrt{x.re \cdot y.re - x.im \cdot y.im} \cdot \color{blue}{\left(\sqrt{\sqrt{x.re \cdot y.re - x.im \cdot y.im}} \cdot \sqrt{\sqrt{x.re \cdot y.re - x.im \cdot y.im}}\right)}\]

  7. Simplified31.2

    \[\leadsto \sqrt{x.re \cdot y.re - x.im \cdot y.im} \cdot \left(\color{blue}{\sqrt{\sqrt{\mathsf{fma}\left(y.re, x.re, -x.im \cdot y.im\right)}}} \cdot \sqrt{\sqrt{x.re \cdot y.re - x.im \cdot y.im}}\right)\]

  8. Simplified31.2

    \[\leadsto \sqrt{x.re \cdot y.re - x.im \cdot y.im} \cdot \left(\sqrt{\sqrt{\mathsf{fma}\left(y.re, x.re, -x.im \cdot y.im\right)}} \cdot \color{blue}{\sqrt{\sqrt{\mathsf{fma}\left(y.re, x.re, -x.im \cdot y.im\right)}}}\right)\]
  9. Using strategy rm

  10. Applied *-un-lft-identity31.2

    \[\leadsto \sqrt{\color{blue}{1 \cdot \left(x.re \cdot y.re - x.im \cdot y.im\right)}} \cdot \left(\sqrt{\sqrt{\mathsf{fma}\left(y.re, x.re, -x.im \cdot y.im\right)}} \cdot \sqrt{\sqrt{\mathsf{fma}\left(y.re, x.re, -x.im \cdot y.im\right)}}\right)\]

  11. Applied sqrt-prod31.2

    \[\leadsto \color{blue}{\left(\sqrt{1} \cdot \sqrt{x.re \cdot y.re - x.im \cdot y.im}\right)} \cdot \left(\sqrt{\sqrt{\mathsf{fma}\left(y.re, x.re, -x.im \cdot y.im\right)}} \cdot \sqrt{\sqrt{\mathsf{fma}\left(y.re, x.re, -x.im \cdot y.im\right)}}\right)\]

  12. Applied associate-*l*31.2

    \[\leadsto \color{blue}{\sqrt{1} \cdot \left(\sqrt{x.re \cdot y.re - x.im \cdot y.im} \cdot \left(\sqrt{\sqrt{\mathsf{fma}\left(y.re, x.re, -x.im \cdot y.im\right)}} \cdot \sqrt{\sqrt{\mathsf{fma}\left(y.re, x.re, -x.im \cdot y.im\right)}}\right)\right)}\]

  13. Simplified0.0

    \[\leadsto \sqrt{1} \cdot \color{blue}{\mathsf{fma}\left(x.im, -y.im, x.re \cdot y.re\right)}\]

  14. Final simplification0.0

    \[\leadsto \mathsf{fma}\left(x.im, -y.im, x.re \cdot y.re\right)\]

Reproduce

herbie shell --seed 2019208 +o rules:numerics
(FPCore (x.re x.im y.re y.im)
  :name "_multiplyComplex, real part"
  :precision binary64
  (- (* x.re y.re) (* x.im y.im)))