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

Average Error: 8.3 → 3.5

Time: 4.8s

Precision: binary64

\[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 0.0023027651367187492:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(1 - x1\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\frac{{x0}^{6}}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{12} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{\frac{x0}{\frac{{\left(1 - x1\right)}^{4}}{x0}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{6} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{6}}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{\left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right) + \frac{{x0}^{6}}{{\left(1 - x1\right)}^{12}}}}{\frac{x0}{\frac{{\left(1 - x1\right)}^{4}}{x0}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \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.002302765136718749)) {
		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) 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) (((double) pow(x0, 6.0)) + ((double) pow((x0 / ((double) (1.0 - x1))), 6.0))))))) / ((double) ((x0 / (((double) pow(((double) (1.0 - x1)), 4.0)) / x0)) + ((double) (x0 * ((double) (x0 + (x0 / ((double) (((double) (1.0 - x1)) * ((double) (1.0 - x1)))))))))))))) / ((double) (x0 + (x0 / ((double) (1.0 - x1))))));
	} else {
		VAR = (((double) (x0 * ((((double) (((double) pow((((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))))), 3.0)) - ((double) pow(((double) pow(x0, 3.0)), 3.0)))) / ((double) (((double) (((double) pow(x0, 6.0)) + ((double) pow((x0 / ((double) (1.0 - x1))), 6.0)))) + (((double) pow(x0, 6.0)) / ((double) pow(((double) (1.0 - x1)), 12.0)))))) / ((double) ((x0 / (((double) pow(((double) (1.0 - x1)), 4.0)) / x0)) + ((double) (x0 * ((double) (x0 + (x0 / ((double) (((double) (1.0 - x1)) * ((double) (1.0 - x1)))))))))))))) / ((double) (x0 + (x0 / ((double) (1.0 - x1))))));
	}
	return VAR;
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	8.3
Target	0.5
Herbie	3.5

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

Derivation

1. Split input into 2 regimes

2. if x1 < 0.0023027651367187492

   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{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} - x0\right)}}{\frac{x0}{1 - x1} + x0}\]

   5. Simplified 9.1

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

   7. Applied flip3-- 7.8

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

   8. Simplified 7.8

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

   9. Simplified 7.8

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

   11. 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)}}}{\frac{x0}{\frac{{\left(1 - x1\right)}^{4}}{x0}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\]

   12. 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}{\frac{{x0}^{6}}{{\left(1 - x1\right)}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}}{\frac{x0}{\frac{{\left(1 - x1\right)}^{4}}{x0}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\]
   13. Using strategy rm

   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}}{\frac{{x0}^{6}}{{\left(1 - \color{blue}{\sqrt{x1} \cdot \sqrt{x1}}\right)}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{\frac{x0}{\frac{{\left(1 - x1\right)}^{4}}{x0}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\]

   15. 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}}{\frac{{x0}^{6}}{{\left(\color{blue}{\sqrt{1} \cdot \sqrt{1}} - \sqrt{x1} \cdot \sqrt{x1}\right)}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{\frac{x0}{\frac{{\left(1 - x1\right)}^{4}}{x0}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\]

   16. 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}}{\frac{{x0}^{6}}{{\color{blue}{\left(\left(\sqrt{1} + \sqrt{x1}\right) \cdot \left(\sqrt{1} - \sqrt{x1}\right)\right)}}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{\frac{x0}{\frac{{\left(1 - x1\right)}^{4}}{x0}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\]

   17. 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}}{\frac{{x0}^{6}}{\color{blue}{{\left(\sqrt{1} + \sqrt{x1}\right)}^{12} \cdot {\left(\sqrt{1} - \sqrt{x1}\right)}^{12}}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{\frac{x0}{\frac{{\left(1 - x1\right)}^{4}}{x0}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\]

   if 0.0023027651367187492 < 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{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} - x0\right)}}{\frac{x0}{1 - x1} + x0}\]

   5. Simplified 4.7

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

   7. Applied flip3-- 4.4

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

   8. Simplified 4.4

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

   9. Simplified 4.5

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

   11. Applied flip3-- 4.4

       \[\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)}}}{\frac{x0}{\frac{{\left(1 - x1\right)}^{4}}{x0}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\]

   12. Simplified 4.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}{\frac{{x0}^{6}}{{\left(1 - x1\right)}^{12}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}}{\frac{x0}{\frac{{\left(1 - x1\right)}^{4}}{x0}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\]
   13. Using strategy rm

   14. Applied add-sqr-sqrt 4.3

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

   15. Applied add-sqr-sqrt 4.3

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

   16. Applied difference-of-squares 4.3

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

   17. Applied unpow-prod-down 1.0

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

4. Final simplification 3.5

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

Reproduce

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