Average Error: 26.1 → 26.1
Time: 25.9s
Precision: 64
\[\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
↓
\[\frac{\frac{x.im \cdot y.im + x.re \cdot y.re}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}}{\sqrt{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 r5239654 = x_re;
        double r5239655 = y_re;
        double r5239656 = r5239654 * r5239655;
        double r5239657 = x_im;
        double r5239658 = y_im;
        double r5239659 = r5239657 * r5239658;
        double r5239660 = r5239656 + r5239659;
        double r5239661 = r5239655 * r5239655;
        double r5239662 = r5239658 * r5239658;
        double r5239663 = r5239661 + r5239662;
        double r5239664 = r5239660 / r5239663;
        return r5239664;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r5239665 = x_im;
        double r5239666 = y_im;
        double r5239667 = r5239665 * r5239666;
        double r5239668 = x_re;
        double r5239669 = y_re;
        double r5239670 = r5239668 * r5239669;
        double r5239671 = r5239667 + r5239670;
        double r5239672 = r5239669 * r5239669;
        double r5239673 = r5239666 * r5239666;
        double r5239674 = r5239672 + r5239673;
        double r5239675 = sqrt(r5239674);
        double r5239676 = r5239671 / r5239675;
        double r5239677 = r5239676 / r5239675;
        return r5239677;
}


\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}
↓
\frac{\frac{x.im \cdot y.im + x.re \cdot y.re}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}

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 26.1

    \[\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
  2. Using strategy rm

  3. Applied add-sqr-sqrt26.1

    \[\leadsto \frac{x.re \cdot y.re + x.im \cdot y.im}{\color{blue}{\sqrt{y.re \cdot y.re + y.im \cdot y.im} \cdot \sqrt{y.re \cdot y.re + y.im \cdot y.im}}}\]

  4. Applied associate-/r*26.1

    \[\leadsto \color{blue}{\frac{\frac{x.re \cdot y.re + x.im \cdot y.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}}\]

  5. Final simplification26.1

    \[\leadsto \frac{\frac{x.im \cdot y.im + x.re \cdot y.re}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\]

Reproduce

herbie shell --seed 2019102 
(FPCore (x.re x.im y.re y.im)
  :name "_divideComplex, real part"
  (/ (+ (* x.re y.re) (* x.im y.im)) (+ (* y.re y.re) (* y.im y.im))))