Average Error: 1.1 → 1.1
Time: 24.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}{\left(\mathsf{qms}\left(\left(\left(x.im \cdot y.re\right)\right), x.re, y.im\right)\right)}}\]
\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}{\left(\mathsf{qms}\left(\left(\left(x.im \cdot y.re\right)\right), x.re, y.im\right)\right)}}
double f(double x_re, double x_im, double y_re, double y_im) {
        double r583365 = x_im;
        double r583366 = y_re;
        double r583367 = r583365 * r583366;
        double r583368 = x_re;
        double r583369 = y_im;
        double r583370 = r583368 * r583369;
        double r583371 = r583367 - r583370;
        double r583372 = r583366 * r583366;
        double r583373 = r583369 * r583369;
        double r583374 = r583372 + r583373;
        double r583375 = r583371 / r583374;
        return r583375;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r583376 = 1.0;
        double r583377 = y_re;
        double r583378 = r583377 * r583377;
        double r583379 = y_im;
        double r583380 = r583379 * r583379;
        double r583381 = r583378 + r583380;
        double r583382 = x_im;
        double r583383 = r583382 * r583377;
        double r583384 = /*Error: no posit support in C */;
        double r583385 = x_re;
        double r583386 = /*Error: no posit support in C */;
        double r583387 = /*Error: no posit support in C */;
        double r583388 = r583381 / r583387;
        double r583389 = r583376 / r583388;
        return r583389;
}

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. Using strategy rm

  6. Applied p16-*-un-lft-identity1.1

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

  7. Applied associate-/l*1.1

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

  8. Final simplification1.1

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

Reproduce

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