Average Error: 1.1 → 1.1
Time: 1.3m
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{\left(\mathsf{qms}\left(\left(\left(x.im \cdot y.re\right)\right), x.re, y.im\right)\right)}{y.re \cdot y.re + y.im \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{\left(\mathsf{qms}\left(\left(\left(x.im \cdot y.re\right)\right), x.re, y.im\right)\right)}{y.re \cdot y.re + y.im \cdot y.im}
double f(double x_re, double x_im, double y_re, double y_im) {
        double r1095344 = x_im;
        double r1095345 = y_re;
        double r1095346 = r1095344 * r1095345;
        double r1095347 = x_re;
        double r1095348 = y_im;
        double r1095349 = r1095347 * r1095348;
        double r1095350 = r1095346 - r1095349;
        double r1095351 = r1095345 * r1095345;
        double r1095352 = r1095348 * r1095348;
        double r1095353 = r1095351 + r1095352;
        double r1095354 = r1095350 / r1095353;
        return r1095354;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r1095355 = x_im;
        double r1095356 = y_re;
        double r1095357 = r1095355 * r1095356;
        double r1095358 = /*Error: no posit support in C */;
        double r1095359 = x_re;
        double r1095360 = y_im;
        double r1095361 = /*Error: no posit support in C */;
        double r1095362 = /*Error: no posit support in C */;
        double r1095363 = r1095356 * r1095356;
        double r1095364 = r1095360 * r1095360;
        double r1095365 = r1095363 + r1095364;
        double r1095366 = r1095362 / r1095365;
        return r1095366;
}

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 introduce-quire1.1

    \[\leadsto \frac{\left(\color{blue}{\left(\left(\left(x.im \cdot y.re\right)\right)\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)}\]

  4. Applied insert-quire-fdp-sub1.1

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

  5. Final simplification1.1

    \[\leadsto \frac{\left(\mathsf{qms}\left(\left(\left(x.im \cdot y.re\right)\right), x.re, y.im\right)\right)}{y.re \cdot y.re + y.im \cdot y.im}\]

Reproduce

herbie shell --seed 2019153 
(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))))