Average Error: 1.1 → 1.0
Time: 47.0s
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)}{\left(\mathsf{qma}\left(\left(\left(y.re \cdot y.re\right)\right), y.im, 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{\left(\mathsf{qms}\left(\left(\left(x.im \cdot y.re\right)\right), x.re, y.im\right)\right)}{\left(\mathsf{qma}\left(\left(\left(y.re \cdot y.re\right)\right), y.im, y.im\right)\right)}
double f(double x_re, double x_im, double y_re, double y_im) {
        double r3185760 = x_im;
        double r3185761 = y_re;
        double r3185762 = r3185760 * r3185761;
        double r3185763 = x_re;
        double r3185764 = y_im;
        double r3185765 = r3185763 * r3185764;
        double r3185766 = r3185762 - r3185765;
        double r3185767 = r3185761 * r3185761;
        double r3185768 = r3185764 * r3185764;
        double r3185769 = r3185767 + r3185768;
        double r3185770 = r3185766 / r3185769;
        return r3185770;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r3185771 = x_im;
        double r3185772 = y_re;
        double r3185773 = r3185771 * r3185772;
        double r3185774 = /*Error: no posit support in C */;
        double r3185775 = x_re;
        double r3185776 = y_im;
        double r3185777 = /*Error: no posit support in C */;
        double r3185778 = /*Error: no posit support in C */;
        double r3185779 = r3185772 * r3185772;
        double r3185780 = /*Error: no posit support in C */;
        double r3185781 = /*Error: no posit support in C */;
        double r3185782 = /*Error: no posit support in C */;
        double r3185783 = r3185778 / r3185782;
        return r3185783;
}

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

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

  7. Applied insert-quire-fdp-add1.0

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

  8. Final simplification1.0

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

Reproduce

herbie shell --seed 2019142 +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))))