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

Average Error: 8.4 → 5.5

Time: 3.9s

Precision: 64

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

Math

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

↓

\[\frac{\left(\left({\left(\sqrt{\frac{x0}{1 - x1}}\right)}^{\frac{3}{2}} + {\left(\sqrt{x0}\right)}^{\frac{3}{2}}\right) \cdot \left({\left(\sqrt{\frac{x0}{1 - x1}}\right)}^{\frac{3}{2}} - {\left(\sqrt{x0}\right)}^{\frac{3}{2}}\right)\right) \cdot \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{x0 + \frac{x0}{1 - x1}}}{\left(\left(\frac{x0}{1 - x1} + x0\right) + \sqrt{\frac{x0}{1 - x1}} \cdot \sqrt{x0}\right) \cdot \left(\sqrt{\frac{x0}{1 - x1}} - \sqrt{x0}\right)}\]

C

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

↓

double code(double x0, double x1) {
	return ((((pow(sqrt((x0 / (1.0 - x1))), 1.5) + pow(sqrt(x0), 1.5)) * (pow(sqrt((x0 / (1.0 - x1))), 1.5) - pow(sqrt(x0), 1.5))) * ((((x0 / (1.0 - x1)) * (x0 / (1.0 - x1))) - (x0 * x0)) / (x0 + (x0 / (1.0 - x1))))) / ((((x0 / (1.0 - x1)) + x0) + (sqrt((x0 / (1.0 - x1))) * sqrt(x0))) * (sqrt((x0 / (1.0 - x1))) - sqrt(x0))));
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	8.4
Target	0.5
Herbie	5.5

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

Derivation

1. Initial program 8.4

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

3. Applied add-sqr-sqrt 8.4

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

4. Applied add-sqr-sqrt 7.6

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

5. Applied difference-of-squares 7.7

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

7. Applied flip3-- 7.8

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

8. Applied flip-+ 8.0

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

9. Applied frac-times 8.0

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

10. Simplified 7.5

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

11. Simplified 7.5

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

13. Applied flip-+ 6.0

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

14. Simplified 6.0

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

15. Simplified 6.0

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

17. Applied sqr-pow 6.0

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

18. Applied sqr-pow 4.0

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

19. Applied difference-of-squares 5.5

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

20. Simplified 5.5

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

21. Simplified 5.5

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

22. Final simplification 5.5

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

Reproduce

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

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