Average Error: 1.1 → 1.1
Time: 11.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{1.0}{\frac{y.re \cdot y.re + y.im \cdot y.im}{x.im \cdot y.re - x.re \cdot y.im}}\]
double f(double x_re, double x_im, double y_re, double y_im) {
        double r1526608 = x_im;
        double r1526609 = y_re;
        double r1526610 = r1526608 * r1526609;
        double r1526611 = x_re;
        double r1526612 = y_im;
        double r1526613 = r1526611 * r1526612;
        double r1526614 = r1526610 - r1526613;
        double r1526615 = r1526609 * r1526609;
        double r1526616 = r1526612 * r1526612;
        double r1526617 = r1526615 + r1526616;
        double r1526618 = r1526614 / r1526617;
        return r1526618;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r1526619 = 1.0;
        double r1526620 = y_re;
        double r1526621 = r1526620 * r1526620;
        double r1526622 = y_im;
        double r1526623 = r1526622 * r1526622;
        double r1526624 = r1526621 + r1526623;
        double r1526625 = x_im;
        double r1526626 = r1526625 * r1526620;
        double r1526627 = x_re;
        double r1526628 = r1526627 * r1526622;
        double r1526629 = r1526626 - r1526628;
        double r1526630 = r1526624 / r1526629;
        double r1526631 = r1526619 / r1526630;
        return r1526631;
}


\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}
↓
\frac{1.0}{\frac{y.re \cdot y.re + y.im \cdot y.im}{x.im \cdot y.re - x.re \cdot y.im}}

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 1.1

    \[\frac{\left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)}{\left(\frac{\left(y.re \cdot y.re\right)}{\left(y.im \cdot y.im\right)}\right)}\]
  2. Using strategy rm

  3. Applied p16-flip--2.1

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

  5. Applied difference-of-squares2.0

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

  6. Applied associate-/l*1.1

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

  8. Applied associate-/r/1.1

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

  9. Applied associate-/l*1.1

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

  10. Simplified1.1

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

  11. Final simplification1.1

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

Reproduce

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