Average Error: 1.1 → 1.1
Time: 17.8s
Precision: 64
\[\frac{\left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)}{\left(\frac{\left(y.re \cdot y.re\right)}{\left(y.im \cdot y.im\right)}\right)}\]
↓
\[\left(\left(\frac{y.re \cdot x.im - x.re \cdot y.im}{\left(\mathsf{qma}\left(\left(\left(y.re \cdot y.re\right)\right), y.im, y.im\right)\right)}\right)\right)\]
\frac{\left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)}{\left(\frac{\left(y.re \cdot y.re\right)}{\left(y.im \cdot y.im\right)}\right)}
↓
\left(\left(\frac{y.re \cdot x.im - x.re \cdot y.im}{\left(\mathsf{qma}\left(\left(\left(y.re \cdot y.re\right)\right), y.im, y.im\right)\right)}\right)\right)
double f(double x_re, double x_im, double y_re, double y_im) {
        double r408266 = x_im;
        double r408267 = y_re;
        double r408268 = r408266 * r408267;
        double r408269 = x_re;
        double r408270 = y_im;
        double r408271 = r408269 * r408270;
        double r408272 = r408268 - r408271;
        double r408273 = r408267 * r408267;
        double r408274 = r408270 * r408270;
        double r408275 = r408273 + r408274;
        double r408276 = r408272 / r408275;
        return r408276;
}
↓
double f(double x_re, double x_im, double y_re, double y_im) {
        double r408277 = y_re;
        double r408278 = x_im;
        double r408279 = r408277 * r408278;
        double r408280 = x_re;
        double r408281 = y_im;
        double r408282 = r408280 * r408281;
        double r408283 = r408279 - r408282;
        double r408284 = r408277 * r408277;
        double r408285 = /*Error: no posit support in C */;
        double r408286 = /*Error: no posit support in C */;
        double r408287 = /*Error: no posit support in C */;
        double r408288 = r408283 / r408287;
        double r408289 = /*Error: no posit support in C */;
        double r408290 = /*Error: no posit support in C */;
        return r408290;
}

Error

Bits error versus x.re

Bits error versus x.im

Bits error versus y.re

Bits error versus y.im

Derivation

  1. Initial program 1.1

    \[\frac{\left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)}{\left(\frac{\left(y.re \cdot y.re\right)}{\left(y.im \cdot y.im\right)}\right)}\]
  2. Using strategy rm

  3. Applied introduce-quire1.1

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

  4. Applied insert-quire-fdp-add1.1

    \[\leadsto \frac{\left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)}{\color{blue}{\left(\left(\mathsf{qma}\left(\left(\left(y.re \cdot y.re\right)\right), y.im, y.im\right)\right)\right)}}\]
  5. Using strategy rm

  6. Applied p16-*-un-lft-identity1.1

    \[\leadsto \frac{\color{blue}{\left(\left(1.0\right) \cdot \left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)\right)}}{\left(\left(\mathsf{qma}\left(\left(\left(y.re \cdot y.re\right)\right), y.im, y.im\right)\right)\right)}\]

  7. Applied associate-/l*1.1

    \[\leadsto \color{blue}{\frac{\left(1.0\right)}{\left(\frac{\left(\left(\mathsf{qma}\left(\left(\left(y.re \cdot y.re\right)\right), y.im, y.im\right)\right)\right)}{\left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)}\right)}}\]
  8. Using strategy rm

  9. Applied introduce-quire1.1

    \[\leadsto \color{blue}{\left(\left(\frac{\left(1.0\right)}{\left(\frac{\left(\left(\mathsf{qma}\left(\left(\left(y.re \cdot y.re\right)\right), y.im, y.im\right)\right)\right)}{\left(\left(x.im \cdot y.re\right) - \left(x.re \cdot y.im\right)\right)}\right)}\right)\right)}\]

  10. Simplified1.1

    \[\leadsto \color{blue}{\left(\left(\frac{\left(\left(y.re \cdot x.im\right) - \left(x.re \cdot y.im\right)\right)}{\left(\left(\mathsf{qma}\left(\left(\left(y.re \cdot y.re\right)\right), y.im, y.im\right)\right)\right)}\right)\right)}\]

  11. Final simplification1.1

    \[\leadsto \left(\left(\frac{y.re \cdot x.im - x.re \cdot y.im}{\left(\mathsf{qma}\left(\left(\left(y.re \cdot y.re\right)\right), y.im, y.im\right)\right)}\right)\right)\]

Reproduce

herbie shell --seed 2019156 +o rules:numerics
(FPCore (x.re x.im y.re y.im)
  :name "_divideComplex, imaginary part"
  (/.p16 (-.p16 (*.p16 x.im y.re) (*.p16 x.re y.im)) (+.p16 (*.p16 y.re y.re) (*.p16 y.im y.im))))