Average Error: 1.1 → 1.1
Time: 1.4m
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 r976399 = x_im;
        double r976400 = y_re;
        double r976401 = r976399 * r976400;
        double r976402 = x_re;
        double r976403 = y_im;
        double r976404 = r976402 * r976403;
        double r976405 = r976401 - r976404;
        double r976406 = r976400 * r976400;
        double r976407 = r976403 * r976403;
        double r976408 = r976406 + r976407;
        double r976409 = r976405 / r976408;
        return r976409;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r976410 = x_im;
        double r976411 = y_re;
        double r976412 = r976410 * r976411;
        double r976413 = /*Error: no posit support in C */;
        double r976414 = x_re;
        double r976415 = y_im;
        double r976416 = /*Error: no posit support in C */;
        double r976417 = /*Error: no posit support in C */;
        double r976418 = r976411 * r976411;
        double r976419 = r976415 * r976415;
        double r976420 = r976418 + r976419;
        double r976421 = r976417 / r976420;
        return r976421;
}

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 +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))))