Average Error: 26.0 → 26.0
Time: 19.8s
Precision: 64
\[\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
↓
\[\frac{1}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} \cdot \frac{x.im \cdot y.im + x.re \cdot y.re}{\sqrt{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{1}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} \cdot \frac{x.im \cdot y.im + x.re \cdot y.re}{\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 r2058477 = x_re;
        double r2058478 = y_re;
        double r2058479 = r2058477 * r2058478;
        double r2058480 = x_im;
        double r2058481 = y_im;
        double r2058482 = r2058480 * r2058481;
        double r2058483 = r2058479 + r2058482;
        double r2058484 = r2058478 * r2058478;
        double r2058485 = r2058481 * r2058481;
        double r2058486 = r2058484 + r2058485;
        double r2058487 = r2058483 / r2058486;
        return r2058487;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r2058488 = 1.0;
        double r2058489 = y_re;
        double r2058490 = r2058489 * r2058489;
        double r2058491 = y_im;
        double r2058492 = r2058491 * r2058491;
        double r2058493 = r2058490 + r2058492;
        double r2058494 = sqrt(r2058493);
        double r2058495 = r2058488 / r2058494;
        double r2058496 = x_im;
        double r2058497 = r2058496 * r2058491;
        double r2058498 = x_re;
        double r2058499 = r2058498 * r2058489;
        double r2058500 = r2058497 + r2058499;
        double r2058501 = r2058500 / r2058494;
        double r2058502 = r2058495 * r2058501;
        return r2058502;
}

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 *-un-lft-identity26.0

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

  5. Applied times-frac26.0

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

  6. Final simplification26.0

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

Reproduce

herbie shell --seed 2019142 
(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))))