Average Error: 1.1 → 1.1
Time: 11.1s
Precision: 64
\[\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)}\]
↓
\[\frac{1.0}{\frac{y.re \cdot y.re + y.im \cdot y.im}{x.im \cdot y.re - x.re \cdot y.im}}\]
\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)}
↓
\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 r1482069 = x_im;
        double r1482070 = y_re;
        double r1482071 = r1482069 * r1482070;
        double r1482072 = x_re;
        double r1482073 = y_im;
        double r1482074 = r1482072 * r1482073;
        double r1482075 = r1482071 - r1482074;
        double r1482076 = r1482070 * r1482070;
        double r1482077 = r1482073 * r1482073;
        double r1482078 = r1482076 + r1482077;
        double r1482079 = r1482075 / r1482078;
        return r1482079;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r1482080 = 1.0;
        double r1482081 = y_re;
        double r1482082 = r1482081 * r1482081;
        double r1482083 = y_im;
        double r1482084 = r1482083 * r1482083;
        double r1482085 = r1482082 + r1482084;
        double r1482086 = x_im;
        double r1482087 = r1482086 * r1482081;
        double r1482088 = x_re;
        double r1482089 = r1482088 * r1482083;
        double r1482090 = r1482087 - r1482089;
        double r1482091 = r1482085 / r1482090;
        double r1482092 = r1482080 / r1482091;
        return r1482092;
}

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

    \[\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-squares1.9

    \[\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 2019124 
(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))))