Average Error: 25.6 → 25.7
Time: 16.1s
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}{y.re \cdot y.re + y.im \cdot y.im} \cdot \left(x.re \cdot y.re + x.im \cdot y.im\right)\]
\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}
↓
\frac{1}{y.re \cdot y.re + y.im \cdot y.im} \cdot \left(x.re \cdot y.re + x.im \cdot y.im\right)
double f(double x_re, double x_im, double y_re, double y_im) {
        double r2351501 = x_re;
        double r2351502 = y_re;
        double r2351503 = r2351501 * r2351502;
        double r2351504 = x_im;
        double r2351505 = y_im;
        double r2351506 = r2351504 * r2351505;
        double r2351507 = r2351503 + r2351506;
        double r2351508 = r2351502 * r2351502;
        double r2351509 = r2351505 * r2351505;
        double r2351510 = r2351508 + r2351509;
        double r2351511 = r2351507 / r2351510;
        return r2351511;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r2351512 = 1.0;
        double r2351513 = y_re;
        double r2351514 = r2351513 * r2351513;
        double r2351515 = y_im;
        double r2351516 = r2351515 * r2351515;
        double r2351517 = r2351514 + r2351516;
        double r2351518 = r2351512 / r2351517;
        double r2351519 = x_re;
        double r2351520 = r2351519 * r2351513;
        double r2351521 = x_im;
        double r2351522 = r2351521 * r2351515;
        double r2351523 = r2351520 + r2351522;
        double r2351524 = r2351518 * r2351523;
        return r2351524;
}

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

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

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

    \[\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 *-un-lft-identity25.5

    \[\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{\color{blue}{1 \cdot \left(y.re \cdot y.re + y.im \cdot y.im\right)}}}\]

  7. Applied sqrt-prod25.5

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

  8. Applied div-inv25.6

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

  9. Applied times-frac25.7

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

  10. Simplified25.7

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

  11. Simplified25.7

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

  12. Final simplification25.7

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

Reproduce

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