Average Error: 26.5 → 26.5
Time: 14.9s
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 r55836 = x_re;
        double r55837 = y_re;
        double r55838 = r55836 * r55837;
        double r55839 = x_im;
        double r55840 = y_im;
        double r55841 = r55839 * r55840;
        double r55842 = r55838 + r55841;
        double r55843 = r55837 * r55837;
        double r55844 = r55840 * r55840;
        double r55845 = r55843 + r55844;
        double r55846 = r55842 / r55845;
        return r55846;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r55847 = 1.0;
        double r55848 = y_re;
        double r55849 = r55848 * r55848;
        double r55850 = y_im;
        double r55851 = r55850 * r55850;
        double r55852 = r55849 + r55851;
        double r55853 = sqrt(r55852);
        double r55854 = r55847 / r55853;
        double r55855 = x_re;
        double r55856 = r55855 * r55848;
        double r55857 = x_im;
        double r55858 = r55857 * r55850;
        double r55859 = r55856 + r55858;
        double r55860 = r55859 / r55853;
        double r55861 = r55854 * r55860;
        return r55861;
}

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.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 add-sqr-sqrt26.5

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

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

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

    \[\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 2019306 
(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))))