Average Error: 26.3 → 26.3
Time: 3.6s
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.re \cdot y.re + x.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{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}}
double f(double x_re, double x_im, double y_re, double y_im) {
        double r53016 = x_re;
        double r53017 = y_re;
        double r53018 = r53016 * r53017;
        double r53019 = x_im;
        double r53020 = y_im;
        double r53021 = r53019 * r53020;
        double r53022 = r53018 + r53021;
        double r53023 = r53017 * r53017;
        double r53024 = r53020 * r53020;
        double r53025 = r53023 + r53024;
        double r53026 = r53022 / r53025;
        return r53026;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r53027 = 1.0;
        double r53028 = y_re;
        double r53029 = r53028 * r53028;
        double r53030 = y_im;
        double r53031 = r53030 * r53030;
        double r53032 = r53029 + r53031;
        double r53033 = sqrt(r53032);
        double r53034 = r53027 / r53033;
        double r53035 = x_re;
        double r53036 = r53035 * r53028;
        double r53037 = x_im;
        double r53038 = r53037 * r53030;
        double r53039 = r53036 + r53038;
        double r53040 = r53039 / r53033;
        double r53041 = r53034 * r53040;
        return r53041;
}

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

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

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

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

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

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

Reproduce

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