Average Error: 25.5 → 24.1
Time: 20.4s
Precision: 64
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
↓
\[\frac{\frac{y.re \cdot x.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}} - y.im \cdot \frac{x.re}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
double f(double x_re, double x_im, double y_re, double y_im) {
        double r3298510 = x_im;
        double r3298511 = y_re;
        double r3298512 = r3298510 * r3298511;
        double r3298513 = x_re;
        double r3298514 = y_im;
        double r3298515 = r3298513 * r3298514;
        double r3298516 = r3298512 - r3298515;
        double r3298517 = r3298511 * r3298511;
        double r3298518 = r3298514 * r3298514;
        double r3298519 = r3298517 + r3298518;
        double r3298520 = r3298516 / r3298519;
        return r3298520;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r3298521 = y_re;
        double r3298522 = x_im;
        double r3298523 = r3298521 * r3298522;
        double r3298524 = y_im;
        double r3298525 = r3298521 * r3298521;
        double r3298526 = fma(r3298524, r3298524, r3298525);
        double r3298527 = sqrt(r3298526);
        double r3298528 = r3298523 / r3298527;
        double r3298529 = x_re;
        double r3298530 = r3298529 / r3298527;
        double r3298531 = r3298524 * r3298530;
        double r3298532 = r3298528 - r3298531;
        double r3298533 = r3298532 / r3298527;
        return r3298533;
}


\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}
↓
\frac{\frac{y.re \cdot x.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}} - y.im \cdot \frac{x.re}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}

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

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

  2. Simplified25.5

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

  4. Applied add-sqr-sqrt25.5

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

  5. Applied associate-/r*25.5

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

  6. Taylor expanded around inf 25.5

    \[\leadsto \frac{\frac{\color{blue}{y.re \cdot x.im - y.im \cdot x.re}}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
  7. Using strategy rm

  8. Applied div-sub25.5

    \[\leadsto \frac{\color{blue}{\frac{y.re \cdot x.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}} - \frac{y.im \cdot x.re}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]
  9. Using strategy rm

  10. Applied *-un-lft-identity25.5

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

  11. Applied sqrt-prod25.5

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

  12. Applied times-frac24.1

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

  13. Simplified24.1

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

  14. Final simplification24.1

    \[\leadsto \frac{\frac{y.re \cdot x.im}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}} - y.im \cdot \frac{x.re}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}}{\sqrt{(y.im \cdot y.im + \left(y.re \cdot y.re\right))_*}}\]

Reproduce

herbie shell --seed 2019102 +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))))