(- (/ x0 (- 1 x1)) x0)

Average Error: 8.4 → 4.0

Time: 25.0min

Precision: binary64

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

\[x0 = 1.855 \land x1 = 2.09000000000000012 \cdot 10^{-4} \lor x0 = 2.98499999999999988 \land x1 = 0.018599999999999998\]

Math

\[\frac{x0}{1 - x1} - x0\]

↓

\[\begin{array}{l} \mathbf{if}\;x1 \le 2.12089080810546861 \cdot 10^{-4}:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\left({x0}^{6} + \frac{{x0}^{6}}{{\left(1 - x1\right)}^{6}}\right) + \frac{{x0}^{6}}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{12} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{12}}}}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}{\frac{x0}{1 - x1} + x0}\\ \mathbf{else}:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{6} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{6}} - {x0}^{3}}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}{\frac{x0}{1 - x1} + x0}\\ \end{array}\]

C

double code(double x0, double x1) {
	return ((double) ((x0 / ((double) (1.0 - x1))) - x0));
}

↓

double code(double x0, double x1) {
	double VAR;
	if ((x1 <= 0.00021208908081054686)) {
		VAR = (((double) (x0 * ((((double) (((double) pow((((double) pow(x0, 3.0)) / ((double) pow(((double) (1.0 - x1)), 6.0))), 3.0)) - ((double) pow(((double) pow(x0, 3.0)), 3.0)))) / ((double) (((double) (((double) pow(x0, 6.0)) + (((double) pow(x0, 6.0)) / ((double) pow(((double) (1.0 - x1)), 6.0))))) + (((double) pow(x0, 6.0)) / ((double) (((double) pow(((double) (((double) sqrt(1.0)) + ((double) sqrt(x1)))), 12.0)) * ((double) pow(((double) (((double) sqrt(1.0)) - ((double) sqrt(x1)))), 12.0)))))))) / ((double) (x0 * ((double) (((double) (x0 + ((x0 / ((double) (1.0 - x1))) / ((double) (1.0 - x1))))) + (x0 / ((double) pow(((double) (1.0 - x1)), 4.0)))))))))) / ((double) ((x0 / ((double) (1.0 - x1))) + x0)));
	} else {
		VAR = (((double) (x0 * (((double) ((((double) pow(x0, 3.0)) / ((double) (((double) pow(((double) (((double) sqrt(1.0)) + ((double) sqrt(x1)))), 6.0)) * ((double) pow(((double) (((double) sqrt(1.0)) - ((double) sqrt(x1)))), 6.0))))) - ((double) pow(x0, 3.0)))) / ((double) (x0 * ((double) (((double) (x0 + ((x0 / ((double) (1.0 - x1))) / ((double) (1.0 - x1))))) + (x0 / ((double) pow(((double) (1.0 - x1)), 4.0)))))))))) / ((double) ((x0 / ((double) (1.0 - x1))) + x0)));
	}
	return VAR;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	8.4
Target	0.5
Herbie	4.0

\[\frac{x0 \cdot x1}{1 - x1}\]

Derivation

1. Split input into 2 regimes

2. if x1 < 2.12089080810546861e-4

   1. Initial program 11.3

      \[\frac{x0}{1 - x1} - x0\]
   2. Using strategy rm

   3. Applied flip-- 11.4

      \[\leadsto \color{blue}{\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{\frac{x0}{1 - x1} + x0}}\]

   4. Simplified 9.1

      \[\leadsto \frac{\color{blue}{x0 \cdot \left(\frac{\frac{x0}{1 - x1}}{1 - x1} - x0\right)}}{\frac{x0}{1 - x1} + x0}\]
   5. Using strategy rm

   6. Applied flip3-- 7.8

      \[\leadsto \frac{x0 \cdot \color{blue}{\frac{{\left(\frac{\frac{x0}{1 - x1}}{1 - x1}\right)}^{3} - {x0}^{3}}{\frac{\frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1}}{1 - x1} + \left(x0 \cdot x0 + \frac{\frac{x0}{1 - x1}}{1 - x1} \cdot x0\right)}}}{\frac{x0}{1 - x1} + x0}\]

   7. Simplified 7.8

      \[\leadsto \frac{x0 \cdot \frac{\color{blue}{\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}} - {x0}^{3}}}{\frac{\frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1}}{1 - x1} + \left(x0 \cdot x0 + \frac{\frac{x0}{1 - x1}}{1 - x1} \cdot x0\right)}}{\frac{x0}{1 - x1} + x0}\]

   8. Simplified 7.8

      \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}} - {x0}^{3}}{\color{blue}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}}{\frac{x0}{1 - x1} + x0}\]
   9. Using strategy rm

   10. Applied flip3-- 6.3

       \[\leadsto \frac{x0 \cdot \frac{\color{blue}{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}} \cdot \frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}} + \left({x0}^{3} \cdot {x0}^{3} + \frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}} \cdot {x0}^{3}\right)}}}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}{\frac{x0}{1 - x1} + x0}\]

   11. Simplified 6.3

       \[\leadsto \frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\color{blue}{\left({x0}^{6} + \frac{{x0}^{6}}{{\left(1 - x1\right)}^{6}}\right) + \frac{{x0}^{6}}{{\left(1 - x1\right)}^{12}}}}}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}{\frac{x0}{1 - x1} + x0}\]
   12. Using strategy rm

   13. Applied add-sqr-sqrt 6.3

       \[\leadsto \frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\left({x0}^{6} + \frac{{x0}^{6}}{{\left(1 - x1\right)}^{6}}\right) + \frac{{x0}^{6}}{{\left(1 - \color{blue}{\sqrt{x1} \cdot \sqrt{x1}}\right)}^{12}}}}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}{\frac{x0}{1 - x1} + x0}\]

   14. Applied add-sqr-sqrt 6.3

       \[\leadsto \frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\left({x0}^{6} + \frac{{x0}^{6}}{{\left(1 - x1\right)}^{6}}\right) + \frac{{x0}^{6}}{{\left(\color{blue}{\sqrt{1} \cdot \sqrt{1}} - \sqrt{x1} \cdot \sqrt{x1}\right)}^{12}}}}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}{\frac{x0}{1 - x1} + x0}\]

   15. Applied difference-of-squares 6.2

       \[\leadsto \frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\left({x0}^{6} + \frac{{x0}^{6}}{{\left(1 - x1\right)}^{6}}\right) + \frac{{x0}^{6}}{{\color{blue}{\left(\left(\sqrt{1} + \sqrt{x1}\right) \cdot \left(\sqrt{1} - \sqrt{x1}\right)\right)}}^{12}}}}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}{\frac{x0}{1 - x1} + x0}\]

   16. Applied unpow-prod-down 6.2

       \[\leadsto \frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\left({x0}^{6} + \frac{{x0}^{6}}{{\left(1 - x1\right)}^{6}}\right) + \frac{{x0}^{6}}{\color{blue}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{12} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{12}}}}}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}{\frac{x0}{1 - x1} + x0}\]

   if 2.12089080810546861e-4 < x1

   1. Initial program 5.5

      \[\frac{x0}{1 - x1} - x0\]
   2. Using strategy rm

   3. Applied flip-- 4.0

      \[\leadsto \color{blue}{\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{\frac{x0}{1 - x1} + x0}}\]

   4. Simplified 4.7

      \[\leadsto \frac{\color{blue}{x0 \cdot \left(\frac{\frac{x0}{1 - x1}}{1 - x1} - x0\right)}}{\frac{x0}{1 - x1} + x0}\]
   5. Using strategy rm

   6. Applied flip3-- 4.4

      \[\leadsto \frac{x0 \cdot \color{blue}{\frac{{\left(\frac{\frac{x0}{1 - x1}}{1 - x1}\right)}^{3} - {x0}^{3}}{\frac{\frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1}}{1 - x1} + \left(x0 \cdot x0 + \frac{\frac{x0}{1 - x1}}{1 - x1} \cdot x0\right)}}}{\frac{x0}{1 - x1} + x0}\]

   7. Simplified 4.4

      \[\leadsto \frac{x0 \cdot \frac{\color{blue}{\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}} - {x0}^{3}}}{\frac{\frac{x0}{1 - x1}}{1 - x1} \cdot \frac{\frac{x0}{1 - x1}}{1 - x1} + \left(x0 \cdot x0 + \frac{\frac{x0}{1 - x1}}{1 - x1} \cdot x0\right)}}{\frac{x0}{1 - x1} + x0}\]

   8. Simplified 4.4

      \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}} - {x0}^{3}}{\color{blue}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}}{\frac{x0}{1 - x1} + x0}\]
   9. Using strategy rm

   10. Applied add-sqr-sqrt 4.4

       \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 - \color{blue}{\sqrt{x1} \cdot \sqrt{x1}}\right)}^{6}} - {x0}^{3}}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}{\frac{x0}{1 - x1} + x0}\]

   11. Applied add-sqr-sqrt 4.4

       \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(\color{blue}{\sqrt{1} \cdot \sqrt{1}} - \sqrt{x1} \cdot \sqrt{x1}\right)}^{6}} - {x0}^{3}}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}{\frac{x0}{1 - x1} + x0}\]

   12. Applied difference-of-squares 4.4

       \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\color{blue}{\left(\left(\sqrt{1} + \sqrt{x1}\right) \cdot \left(\sqrt{1} - \sqrt{x1}\right)\right)}}^{6}} - {x0}^{3}}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}{\frac{x0}{1 - x1} + x0}\]

   13. Applied unpow-prod-down 1.6

       \[\leadsto \frac{x0 \cdot \frac{\frac{{x0}^{3}}{\color{blue}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{6} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{6}}} - {x0}^{3}}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}{\frac{x0}{1 - x1} + x0}\]
3. Recombined 2 regimes into one program.

4. Final simplification 4.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;x1 \le 2.12089080810546861 \cdot 10^{-4}:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\left({x0}^{6} + \frac{{x0}^{6}}{{\left(1 - x1\right)}^{6}}\right) + \frac{{x0}^{6}}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{12} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{12}}}}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}{\frac{x0}{1 - x1} + x0}\\ \mathbf{else}:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{6} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{6}} - {x0}^{3}}{x0 \cdot \left(\left(x0 + \frac{\frac{x0}{1 - x1}}{1 - x1}\right) + \frac{x0}{{\left(1 - x1\right)}^{4}}\right)}}{\frac{x0}{1 - x1} + x0}\\ \end{array}\]

Reproduce

herbie shell --seed 2020181 
(FPCore (x0 x1)
  :name "(- (/ x0 (- 1 x1)) x0)"
  :precision binary64
  :pre (or (and (== x0 1.855) (== x1 0.000209)) (and (== x0 2.985) (== x1 0.0186)))

  :herbie-target
  (/ (* x0 x1) (- 1.0 x1))

  (- (/ x0 (- 1.0 x1)) x0))