Average Error: 25.7 → 25.7
Time: 15.0s
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.im \cdot y.im + x.re \cdot y.re}{\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.im \cdot y.im + x.re \cdot y.re}{\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 r1988485 = x_re;
        double r1988486 = y_re;
        double r1988487 = r1988485 * r1988486;
        double r1988488 = x_im;
        double r1988489 = y_im;
        double r1988490 = r1988488 * r1988489;
        double r1988491 = r1988487 + r1988490;
        double r1988492 = r1988486 * r1988486;
        double r1988493 = r1988489 * r1988489;
        double r1988494 = r1988492 + r1988493;
        double r1988495 = r1988491 / r1988494;
        return r1988495;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r1988496 = 1.0;
        double r1988497 = y_re;
        double r1988498 = r1988497 * r1988497;
        double r1988499 = y_im;
        double r1988500 = r1988499 * r1988499;
        double r1988501 = r1988498 + r1988500;
        double r1988502 = sqrt(r1988501);
        double r1988503 = r1988496 / r1988502;
        double r1988504 = x_im;
        double r1988505 = r1988504 * r1988499;
        double r1988506 = x_re;
        double r1988507 = r1988506 * r1988497;
        double r1988508 = r1988505 + r1988507;
        double r1988509 = r1988508 / r1988502;
        double r1988510 = r1988503 * r1988509;
        return r1988510;
}

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

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

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

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

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

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

Reproduce

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