Average Error: 26.1 → 26.1
Time: 12.7s
Precision: 64
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
↓
\[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}
↓
\frac{x.im \cdot y.re - x.re \cdot y.im}{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 r61906 = x_im;
        double r61907 = y_re;
        double r61908 = r61906 * r61907;
        double r61909 = x_re;
        double r61910 = y_im;
        double r61911 = r61909 * r61910;
        double r61912 = r61908 - r61911;
        double r61913 = r61907 * r61907;
        double r61914 = r61910 * r61910;
        double r61915 = r61913 + r61914;
        double r61916 = r61912 / r61915;
        return r61916;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r61917 = x_im;
        double r61918 = y_re;
        double r61919 = r61917 * r61918;
        double r61920 = x_re;
        double r61921 = y_im;
        double r61922 = r61920 * r61921;
        double r61923 = r61919 - r61922;
        double r61924 = r61918 * r61918;
        double r61925 = r61921 * r61921;
        double r61926 = r61924 + r61925;
        double r61927 = r61923 / r61926;
        return r61927;
}

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

    \[\frac{x.im \cdot y.re - x.re \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im}\]
  2. Using strategy rm

  3. Applied add-sqr-sqrt26.1

    \[\leadsto \frac{x.im \cdot y.re - x.re \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 associate-/r*26.0

    \[\leadsto \color{blue}{\frac{\frac{x.im \cdot y.re - x.re \cdot y.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}}\]

  5. Final simplification26.1

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

Reproduce

herbie shell --seed 2019291 
(FPCore (x.re x.im y.re y.im)
  :name "_divideComplex, imaginary part"
  :precision binary64
  (/ (- (* x.im y.re) (* x.re y.im)) (+ (* y.re y.re) (* y.im y.im))))