Average Error: 26.5 → 26.3
Time: 3.5s
Precision: 64
\[\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
↓
\[\begin{array}{l} \mathbf{if}\;\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im} \le 5.1588593744494812 \cdot 10^{245}:\\ \;\;\;\;\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} \cdot \left(-1 \cdot x.re\right)\\ \end{array}\]
\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}
↓
\begin{array}{l}
\mathbf{if}\;\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im} \le 5.1588593744494812 \cdot 10^{245}:\\
\;\;\;\;\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\\

\mathbf{else}:\\
\;\;\;\;\frac{1}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} \cdot \left(-1 \cdot x.re\right)\\

\end{array}
double f(double x_re, double x_im, double y_re, double y_im) {
        double r113932 = x_re;
        double r113933 = y_re;
        double r113934 = r113932 * r113933;
        double r113935 = x_im;
        double r113936 = y_im;
        double r113937 = r113935 * r113936;
        double r113938 = r113934 + r113937;
        double r113939 = r113933 * r113933;
        double r113940 = r113936 * r113936;
        double r113941 = r113939 + r113940;
        double r113942 = r113938 / r113941;
        return r113942;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r113943 = x_re;
        double r113944 = y_re;
        double r113945 = r113943 * r113944;
        double r113946 = x_im;
        double r113947 = y_im;
        double r113948 = r113946 * r113947;
        double r113949 = r113945 + r113948;
        double r113950 = r113944 * r113944;
        double r113951 = r113947 * r113947;
        double r113952 = r113950 + r113951;
        double r113953 = r113949 / r113952;
        double r113954 = 5.158859374449481e+245;
        bool r113955 = r113953 <= r113954;
        double r113956 = 1.0;
        double r113957 = sqrt(r113952);
        double r113958 = r113956 / r113957;
        double r113959 = -1.0;
        double r113960 = r113959 * r113943;
        double r113961 = r113958 * r113960;
        double r113962 = r113955 ? r113953 : r113961;
        return r113962;
}

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. Split input into 2 regimes

  2. if (/ (+ (* x.re y.re) (* x.im y.im)) (+ (* y.re y.re) (* y.im y.im))) < 5.158859374449481e+245

    1. Initial program 14.6

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

    if 5.158859374449481e+245 < (/ (+ (* x.re y.re) (* x.im y.im)) (+ (* y.re y.re) (* y.im y.im)))

    1. Initial program 60.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-sqrt60.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 *-un-lft-identity60.6

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

      \[\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. Taylor expanded around -inf 60.1

      \[\leadsto \frac{1}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} \cdot \color{blue}{\left(-1 \cdot x.re\right)}\]
  3. Recombined 2 regimes into one program.

  4. Final simplification26.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im} \le 5.1588593744494812 \cdot 10^{245}:\\ \;\;\;\;\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} \cdot \left(-1 \cdot x.re\right)\\ \end{array}\]

Reproduce

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