Average Error: 1.1 → 1.1
Time: 34.9s
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 r2711908 = x_im;
        double r2711909 = y_re;
        double r2711910 = r2711908 * r2711909;
        double r2711911 = x_re;
        double r2711912 = y_im;
        double r2711913 = r2711911 * r2711912;
        double r2711914 = r2711910 - r2711913;
        double r2711915 = r2711909 * r2711909;
        double r2711916 = r2711912 * r2711912;
        double r2711917 = r2711915 + r2711916;
        double r2711918 = r2711914 / r2711917;
        return r2711918;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r2711919 = x_im;
        double r2711920 = y_re;
        double r2711921 = r2711919 * r2711920;
        double r2711922 = /*Error: no posit support in C */;
        double r2711923 = x_re;
        double r2711924 = y_im;
        double r2711925 = /*Error: no posit support in C */;
        double r2711926 = /*Error: no posit support in C */;
        double r2711927 = r2711920 * r2711920;
        double r2711928 = r2711924 * r2711924;
        double r2711929 = r2711927 + r2711928;
        double r2711930 = r2711926 / r2711929;
        return r2711930;
}

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