Average Error: 26.9 → 26.9
Time: 2.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 \cdot \left(x.re \cdot y.re + x.im \cdot y.im\right)}{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 \cdot \left(x.re \cdot y.re + x.im \cdot y.im\right)}{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 r109376 = x_re;
        double r109377 = y_re;
        double r109378 = r109376 * r109377;
        double r109379 = x_im;
        double r109380 = y_im;
        double r109381 = r109379 * r109380;
        double r109382 = r109378 + r109381;
        double r109383 = r109377 * r109377;
        double r109384 = r109380 * r109380;
        double r109385 = r109383 + r109384;
        double r109386 = r109382 / r109385;
        return r109386;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r109387 = 1.0;
        double r109388 = x_re;
        double r109389 = y_re;
        double r109390 = r109388 * r109389;
        double r109391 = x_im;
        double r109392 = y_im;
        double r109393 = r109391 * r109392;
        double r109394 = r109390 + r109393;
        double r109395 = r109387 * r109394;
        double r109396 = r109389 * r109389;
        double r109397 = r109392 * r109392;
        double r109398 = r109396 + r109397;
        double r109399 = r109395 / r109398;
        return r109399;
}

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

    \[\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 *-un-lft-identity26.9

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

  4. Final simplification26.9

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

Reproduce

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