_divideComplex, real part

Average Error: 27.0 → 25.6

Time: 6.4s

Precision: binary64

• Falling back on racket egraph because egg-herbie package not installed

Math

\[\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} = -inf.0:\\ \;\;\;\;\frac{x.re}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\\ \mathbf{elif}\;\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im} \le 3.7505355971518835 \cdot 10^{302}:\\ \;\;\;\;\frac{1}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} \cdot \frac{y.re \cdot x.re + x.im \cdot y.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\\ \end{array}\]

C

double code(double x_46_re, double x_46_im, double y_46_re, double y_46_im) {
	return (((double) (((double) (x_46_re * y_46_re)) + ((double) (x_46_im * y_46_im)))) / ((double) (((double) (y_46_re * y_46_re)) + ((double) (y_46_im * y_46_im)))));
}

↓

double code(double x_46_re, double x_46_im, double y_46_re, double y_46_im) {
	double VAR;
	if (((((double) (((double) (x_46_re * y_46_re)) + ((double) (x_46_im * y_46_im)))) / ((double) (((double) (y_46_re * y_46_re)) + ((double) (y_46_im * y_46_im))))) <= -inf.0)) {
		VAR = (x_46_re / ((double) sqrt(((double) (((double) (y_46_re * y_46_re)) + ((double) (y_46_im * y_46_im)))))));
	} else {
		double VAR_1;
		if (((((double) (((double) (x_46_re * y_46_re)) + ((double) (x_46_im * y_46_im)))) / ((double) (((double) (y_46_re * y_46_re)) + ((double) (y_46_im * y_46_im))))) <= 3.7505355971518835e+302)) {
			VAR_1 = ((double) ((1.0 / ((double) sqrt(((double) (((double) (y_46_re * y_46_re)) + ((double) (y_46_im * y_46_im))))))) * (((double) (((double) (y_46_re * x_46_re)) + ((double) (x_46_im * y_46_im)))) / ((double) sqrt(((double) (((double) (y_46_re * y_46_re)) + ((double) (y_46_im * y_46_im)))))))));
		} else {
			VAR_1 = (x_46_im / ((double) sqrt(((double) (((double) (y_46_re * y_46_re)) + ((double) (y_46_im * y_46_im)))))));
		}
		VAR = VAR_1;
	}
	return VAR;
}

Error

Bits error versus x.re

Bits error versus x.im

Bits error versus y.re

Bits error versus y.im

Derivation

1. Split input into 3 regimes

2. if (/ (+ (* x.re y.re) (* x.im y.im)) (+ (* y.re y.re) (* y.im y.im))) < -inf.0

   1. Initial program 64.0

      \[\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-sqrt 64.0

      \[\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 associate-/r* 64.0

      \[\leadsto \color{blue}{\frac{\frac{x.re \cdot y.re + x.im \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. Simplified 64.0

      \[\leadsto \frac{\color{blue}{\frac{y.re \cdot x.re + x.im \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}}\]

   6. Taylor expanded around inf 51.9

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

   if -inf.0 < (/ (+ (* x.re y.re) (* x.im y.im)) (+ (* y.re y.re) (* y.im y.im))) < 3.7505355971518835e302

   1. Initial program 12.0

      \[\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-sqrt 12.0

      \[\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-identity 12.0

      \[\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-frac 12.0

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

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

   if 3.7505355971518835e302 < (/ (+ (* x.re y.re) (* x.im y.im)) (+ (* y.re y.re) (* y.im y.im)))

   1. Initial program 63.8

      \[\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-sqrt 63.8

      \[\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 associate-/r* 63.8

      \[\leadsto \color{blue}{\frac{\frac{x.re \cdot y.re + x.im \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. Simplified 63.8

      \[\leadsto \frac{\color{blue}{\frac{y.re \cdot x.re + x.im \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}}\]

   6. Taylor expanded around 0 60.2

      \[\leadsto \frac{\color{blue}{x.im}}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\]
3. Recombined 3 regimes into one program.

4. Final simplification 25.6

   \[\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} = -inf.0:\\ \;\;\;\;\frac{x.re}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\\ \mathbf{elif}\;\frac{x.re \cdot y.re + x.im \cdot y.im}{y.re \cdot y.re + y.im \cdot y.im} \le 3.7505355971518835 \cdot 10^{302}:\\ \;\;\;\;\frac{1}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}} \cdot \frac{y.re \cdot x.re + x.im \cdot y.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x.im}{\sqrt{y.re \cdot y.re + y.im \cdot y.im}}\\ \end{array}\]

Reproduce

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