Average Error: 1.1 → 1.1
Time: 11.2s
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 r1064176 = x_im;
        double r1064177 = y_re;
        double r1064178 = r1064176 * r1064177;
        double r1064179 = x_re;
        double r1064180 = y_im;
        double r1064181 = r1064179 * r1064180;
        double r1064182 = r1064178 - r1064181;
        double r1064183 = r1064177 * r1064177;
        double r1064184 = r1064180 * r1064180;
        double r1064185 = r1064183 + r1064184;
        double r1064186 = r1064182 / r1064185;
        return r1064186;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r1064187 = 1.0;
        double r1064188 = y_re;
        double r1064189 = r1064188 * r1064188;
        double r1064190 = y_im;
        double r1064191 = r1064190 * r1064190;
        double r1064192 = r1064189 + r1064191;
        double r1064193 = x_im;
        double r1064194 = r1064193 * r1064188;
        double r1064195 = x_re;
        double r1064196 = r1064195 * r1064190;
        double r1064197 = r1064194 - r1064196;
        double r1064198 = r1064192 / r1064197;
        double r1064199 = r1064187 / r1064198;
        return r1064199;
}

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 2019104 
(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))))