Average Error: 26.2 → 26.2
Time: 5.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{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}
↓
\frac{x.re \cdot y.re + x.im \cdot y.im}{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 r50612 = x_re;
        double r50613 = y_re;
        double r50614 = r50612 * r50613;
        double r50615 = x_im;
        double r50616 = y_im;
        double r50617 = r50615 * r50616;
        double r50618 = r50614 + r50617;
        double r50619 = r50613 * r50613;
        double r50620 = r50616 * r50616;
        double r50621 = r50619 + r50620;
        double r50622 = r50618 / r50621;
        return r50622;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r50623 = x_re;
        double r50624 = y_re;
        double r50625 = r50623 * r50624;
        double r50626 = x_im;
        double r50627 = y_im;
        double r50628 = r50626 * r50627;
        double r50629 = r50625 + r50628;
        double r50630 = r50624 * r50624;
        double r50631 = r50627 * r50627;
        double r50632 = r50630 + r50631;
        double r50633 = r50629 / r50632;
        return r50633;
}

Error

Bits error versus x.re

Bits error versus x.im

Bits error versus y.re

Bits error versus y.im

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 26.2

    \[\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.2

    \[\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.2

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

Reproduce

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