Average Error: 26.0 → 26.0
Time: 11.7s
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 r44510 = x_re;
        double r44511 = y_re;
        double r44512 = r44510 * r44511;
        double r44513 = x_im;
        double r44514 = y_im;
        double r44515 = r44513 * r44514;
        double r44516 = r44512 + r44515;
        double r44517 = r44511 * r44511;
        double r44518 = r44514 * r44514;
        double r44519 = r44517 + r44518;
        double r44520 = r44516 / r44519;
        return r44520;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r44521 = x_re;
        double r44522 = y_re;
        double r44523 = r44521 * r44522;
        double r44524 = x_im;
        double r44525 = y_im;
        double r44526 = r44524 * r44525;
        double r44527 = r44523 + r44526;
        double r44528 = r44522 * r44522;
        double r44529 = r44525 * r44525;
        double r44530 = r44528 + r44529;
        double r44531 = r44527 / r44530;
        return r44531;
}

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*25.9

    \[\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. Using strategy rm

  6. Applied clear-num26.0

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

  7. 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 2019291 
(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))))