Average Error: 25.3 → 22.1
Time: 27.3s
Precision: 64
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
↓
\[\frac{x.im \cdot \frac{y.re}{\sqrt{\mathsf{fma}\left(y.im, y.im, y.re \cdot y.re\right)}} - \frac{x.re}{\frac{\sqrt{\mathsf{fma}\left(y.im, y.im, y.re \cdot y.re\right)}}{y.im}}}{\sqrt{\mathsf{fma}\left(y.im, y.im, y.re \cdot y.re\right)}}\]
\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}
↓
\frac{x.im \cdot \frac{y.re}{\sqrt{\mathsf{fma}\left(y.im, y.im, y.re \cdot y.re\right)}} - \frac{x.re}{\frac{\sqrt{\mathsf{fma}\left(y.im, y.im, y.re \cdot y.re\right)}}{y.im}}}{\sqrt{\mathsf{fma}\left(y.im, y.im, y.re \cdot y.re\right)}}
double f(double x_re, double x_im, double y_re, double y_im) {
        double r1703592 = x_im;
        double r1703593 = y_re;
        double r1703594 = r1703592 * r1703593;
        double r1703595 = x_re;
        double r1703596 = y_im;
        double r1703597 = r1703595 * r1703596;
        double r1703598 = r1703594 - r1703597;
        double r1703599 = r1703593 * r1703593;
        double r1703600 = r1703596 * r1703596;
        double r1703601 = r1703599 + r1703600;
        double r1703602 = r1703598 / r1703601;
        return r1703602;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r1703603 = x_im;
        double r1703604 = y_re;
        double r1703605 = y_im;
        double r1703606 = r1703604 * r1703604;
        double r1703607 = fma(r1703605, r1703605, r1703606);
        double r1703608 = sqrt(r1703607);
        double r1703609 = r1703604 / r1703608;
        double r1703610 = r1703603 * r1703609;
        double r1703611 = x_re;
        double r1703612 = r1703608 / r1703605;
        double r1703613 = r1703611 / r1703612;
        double r1703614 = r1703610 - r1703613;
        double r1703615 = r1703614 / r1703608;
        return r1703615;
}

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 25.3

    \[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]

  2. Simplified25.3

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

  4. Applied add-sqr-sqrt25.3

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

  5. Applied associate-/r*25.3

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

  7. Applied div-sub25.3

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

  9. Applied *-un-lft-identity25.3

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

  10. Applied times-frac23.8

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

  11. Simplified23.8

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

  13. Applied associate-/l*22.1

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

  14. Final simplification22.1

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

Reproduce

herbie shell --seed 2019144 +o rules:numerics
(FPCore (x.re x.im y.re y.im)
  :name "_divideComplex, imaginary part"
  (/ (- (* x.im y.re) (* x.re y.im)) (+ (* y.re y.re) (* y.im y.im))))