Average Error: 26.0 → 26.0
Time: 13.3s
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 r66364 = x_re;
        double r66365 = y_re;
        double r66366 = r66364 * r66365;
        double r66367 = x_im;
        double r66368 = y_im;
        double r66369 = r66367 * r66368;
        double r66370 = r66366 + r66369;
        double r66371 = r66365 * r66365;
        double r66372 = r66368 * r66368;
        double r66373 = r66371 + r66372;
        double r66374 = r66370 / r66373;
        return r66374;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r66375 = x_re;
        double r66376 = y_re;
        double r66377 = r66375 * r66376;
        double r66378 = x_im;
        double r66379 = y_im;
        double r66380 = r66378 * r66379;
        double r66381 = r66377 + r66380;
        double r66382 = r66376 * r66376;
        double r66383 = r66379 * r66379;
        double r66384 = r66382 + r66383;
        double r66385 = r66381 / r66384;
        return r66385;
}

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.0

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

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

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

    \[\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 2019298 
(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))))