Rosa's DopplerBench

Average Error: 18.5 → 0.7

Time: 23.3s

Precision: 64

Math

\[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]

↓

\[\begin{array}{l} \mathbf{if}\;u \le -2.2057910742292809 \cdot 10^{72}:\\ \;\;\;\;\left(\frac{v}{t1 + u} \cdot \left(-\sqrt[3]{t1} \cdot \sqrt[3]{t1}\right)\right) \cdot \frac{\sqrt[3]{t1}}{t1 + u}\\ \mathbf{elif}\;u \le 2.5797567822584585 \cdot 10^{-16}:\\ \;\;\;\;\frac{-\frac{v}{1}}{\frac{t1 + u}{t1} \cdot \left(t1 + u\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{v}{t1 + u} \cdot \left(-\frac{t1}{t1 + u}\right)\\ \end{array}\]

C

double code(double u, double v, double t1) {
	return ((double) (((double) (((double) -(t1)) * v)) / ((double) (((double) (t1 + u)) * ((double) (t1 + u))))));
}

↓

double code(double u, double v, double t1) {
	double VAR;
	if ((u <= -2.205791074229281e+72)) {
		VAR = ((double) (((double) (((double) (v / ((double) (t1 + u)))) * ((double) -(((double) (((double) cbrt(t1)) * ((double) cbrt(t1)))))))) * ((double) (((double) cbrt(t1)) / ((double) (t1 + u))))));
	} else {
		double VAR_1;
		if ((u <= 2.5797567822584585e-16)) {
			VAR_1 = ((double) (((double) -(((double) (v / 1.0)))) / ((double) (((double) (((double) (t1 + u)) / t1)) * ((double) (t1 + u))))));
		} else {
			VAR_1 = ((double) (((double) (v / ((double) (t1 + u)))) * ((double) -(((double) (t1 / ((double) (t1 + u))))))));
		}
		VAR = VAR_1;
	}
	return VAR;
}

Error

Bits error versus u

Bits error versus v

Bits error versus t1

Derivation

1. Split input into 3 regimes

2. if u < -2.205791074229281e+72

   1. Initial program 16.3

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]
   2. Using strategy rm

   3. Applied *-commutative 16.3

      \[\leadsto \frac{\color{blue}{v \cdot \left(-t1\right)}}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]

   4. Applied times-frac 1.4

      \[\leadsto \color{blue}{\frac{v}{t1 + u} \cdot \frac{-t1}{t1 + u}}\]

   5. Simplified 1.4

      \[\leadsto \frac{v}{t1 + u} \cdot \color{blue}{\left(-\frac{t1}{t1 + u}\right)}\]
   6. Using strategy rm

   7. Applied *-un-lft-identity 1.4

      \[\leadsto \frac{v}{t1 + u} \cdot \left(-\frac{t1}{\color{blue}{1 \cdot \left(t1 + u\right)}}\right)\]

   8. Applied add-cube-cbrt 1.8

      \[\leadsto \frac{v}{t1 + u} \cdot \left(-\frac{\color{blue}{\left(\sqrt[3]{t1} \cdot \sqrt[3]{t1}\right) \cdot \sqrt[3]{t1}}}{1 \cdot \left(t1 + u\right)}\right)\]

   9. Applied times-frac 1.8

      \[\leadsto \frac{v}{t1 + u} \cdot \left(-\color{blue}{\frac{\sqrt[3]{t1} \cdot \sqrt[3]{t1}}{1} \cdot \frac{\sqrt[3]{t1}}{t1 + u}}\right)\]

   10. Applied distribute-lft-neg-in 1.8

       \[\leadsto \frac{v}{t1 + u} \cdot \color{blue}{\left(\left(-\frac{\sqrt[3]{t1} \cdot \sqrt[3]{t1}}{1}\right) \cdot \frac{\sqrt[3]{t1}}{t1 + u}\right)}\]

   11. Applied associate-*r* 0.5

       \[\leadsto \color{blue}{\left(\frac{v}{t1 + u} \cdot \left(-\frac{\sqrt[3]{t1} \cdot \sqrt[3]{t1}}{1}\right)\right) \cdot \frac{\sqrt[3]{t1}}{t1 + u}}\]

   12. Simplified 0.5

       \[\leadsto \color{blue}{\left(\frac{v}{t1 + u} \cdot \left(-\sqrt[3]{t1} \cdot \sqrt[3]{t1}\right)\right)} \cdot \frac{\sqrt[3]{t1}}{t1 + u}\]

   if -2.205791074229281e+72 < u < 2.5797567822584585e-16

   1. Initial program 21.5

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]
   2. Using strategy rm

   3. Applied *-commutative 21.5

      \[\leadsto \frac{\color{blue}{v \cdot \left(-t1\right)}}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]

   4. Applied times-frac 1.7

      \[\leadsto \color{blue}{\frac{v}{t1 + u} \cdot \frac{-t1}{t1 + u}}\]

   5. Simplified 1.7

      \[\leadsto \frac{v}{t1 + u} \cdot \color{blue}{\left(-\frac{t1}{t1 + u}\right)}\]
   6. Using strategy rm

   7. Applied clear-num 1.7

      \[\leadsto \frac{v}{t1 + u} \cdot \left(-\color{blue}{\frac{1}{\frac{t1 + u}{t1}}}\right)\]

   8. Applied distribute-neg-frac 1.7

      \[\leadsto \frac{v}{t1 + u} \cdot \color{blue}{\frac{-1}{\frac{t1 + u}{t1}}}\]

   9. Applied associate-*r/ 1.7

      \[\leadsto \color{blue}{\frac{\frac{v}{t1 + u} \cdot \left(-1\right)}{\frac{t1 + u}{t1}}}\]

   10. Simplified 1.7

       \[\leadsto \frac{\color{blue}{-\frac{v}{t1 + u}}}{\frac{t1 + u}{t1}}\]
   11. Using strategy rm

   12. Applied *-un-lft-identity 1.7

       \[\leadsto \frac{-\frac{v}{\color{blue}{1 \cdot \left(t1 + u\right)}}}{\frac{t1 + u}{t1}}\]

   13. Applied associate-/r* 1.7

       \[\leadsto \frac{-\color{blue}{\frac{\frac{v}{1}}{t1 + u}}}{\frac{t1 + u}{t1}}\]

   14. Applied distribute-neg-frac 1.7

       \[\leadsto \frac{\color{blue}{\frac{-\frac{v}{1}}{t1 + u}}}{\frac{t1 + u}{t1}}\]

   15. Applied associate-/l/ 0.5

       \[\leadsto \color{blue}{\frac{-\frac{v}{1}}{\frac{t1 + u}{t1} \cdot \left(t1 + u\right)}}\]

   if 2.5797567822584585e-16 < u

   1. Initial program 14.0

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]
   2. Using strategy rm

   3. Applied *-commutative 14.0

      \[\leadsto \frac{\color{blue}{v \cdot \left(-t1\right)}}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]

   4. Applied times-frac 1.3

      \[\leadsto \color{blue}{\frac{v}{t1 + u} \cdot \frac{-t1}{t1 + u}}\]

   5. Simplified 1.3

      \[\leadsto \frac{v}{t1 + u} \cdot \color{blue}{\left(-\frac{t1}{t1 + u}\right)}\]
3. Recombined 3 regimes into one program.

4. Final simplification 0.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;u \le -2.2057910742292809 \cdot 10^{72}:\\ \;\;\;\;\left(\frac{v}{t1 + u} \cdot \left(-\sqrt[3]{t1} \cdot \sqrt[3]{t1}\right)\right) \cdot \frac{\sqrt[3]{t1}}{t1 + u}\\ \mathbf{elif}\;u \le 2.5797567822584585 \cdot 10^{-16}:\\ \;\;\;\;\frac{-\frac{v}{1}}{\frac{t1 + u}{t1} \cdot \left(t1 + u\right)}\\ \mathbf{else}:\\ \;\;\;\;\frac{v}{t1 + u} \cdot \left(-\frac{t1}{t1 + u}\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2020113 +o rules:numerics
(FPCore (u v t1)
  :name "Rosa's DopplerBench"
  :precision binary64
  (/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))