Average Error: 25.5 → 25.4
Time: 3.2s
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.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}}\]
\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}
↓
\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}}
double f(double x_re, double x_im, double y_re, double y_im) {
        double r107551 = x_re;
        double r107552 = y_re;
        double r107553 = r107551 * r107552;
        double r107554 = x_im;
        double r107555 = y_im;
        double r107556 = r107554 * r107555;
        double r107557 = r107553 + r107556;
        double r107558 = r107552 * r107552;
        double r107559 = r107555 * r107555;
        double r107560 = r107558 + r107559;
        double r107561 = r107557 / r107560;
        return r107561;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r107562 = x_re;
        double r107563 = y_re;
        double r107564 = r107562 * r107563;
        double r107565 = x_im;
        double r107566 = y_im;
        double r107567 = r107565 * r107566;
        double r107568 = r107564 + r107567;
        double r107569 = r107563 * r107563;
        double r107570 = r107566 * r107566;
        double r107571 = r107569 + r107570;
        double r107572 = sqrt(r107571);
        double r107573 = r107568 / r107572;
        double r107574 = r107573 / r107572;
        return r107574;
}

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 25.5

    \[\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 div-inv25.6

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

  5. Applied *-un-lft-identity25.6

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

  6. Applied associate-*l*25.6

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

  7. Simplified25.5

    \[\leadsto 1 \cdot \color{blue}{\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}}\]
  8. Using strategy rm

  9. Applied add-sqr-sqrt25.5

    \[\leadsto 1 \cdot \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}}}\]

  10. Applied associate-/r*25.4

    \[\leadsto 1 \cdot \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}}}\]

  11. Final simplification25.4

    \[\leadsto \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}}\]

Reproduce

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