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

Average Error: 8.3 → 5.1

Time: 9.0s

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\]

↓

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

C

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

↓

double code(double x0, double x1) {
	return (((double) (x0 * ((((double) (((double) pow(((double) pow(((x0 / ((double) (1.0 - x1))) / ((double) (1.0 - x1))), 3.0)), 3.0)) - ((double) pow(((double) pow(x0, 3.0)), 3.0)))) / ((double) (((double) ((((double) pow(x0, 6.0)) / ((double) pow(((double) (((double) (1.0 - x1)) * ((double) (1.0 - x1)))), 3.0))) + ((double) pow(x0, 6.0)))) + ((double) (((double) pow(((double) (((double) cbrt((x0 / ((double) (1.0 - x1))))) * ((double) cbrt((x0 / ((double) (1.0 - x1))))))), 6.0)) * ((double) pow((((double) cbrt((x0 / ((double) (1.0 - x1))))) / ((double) (1.0 - x1))), 6.0))))))) / ((double) (((double) (x0 * ((double) (((x0 / ((double) (1.0 - x1))) / ((double) (1.0 - x1))) + x0)))) + (((double) ((x0 / ((double) (1.0 - x1))) * x0)) / ((double) pow(((double) (1.0 - x1)), 3.0)))))))) / ((double) (x0 + (x0 / ((double) (1.0 - x1))))));
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	8.3
Target	0.5
Herbie	5.1

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

Derivation

1. Initial program 8.3

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

3. Applied flip-- 7.7

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

4. Simplified 6.9

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

5. Simplified 6.9

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

7. Applied flip3-- 6.1

   \[\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)}}}{x0 + \frac{x0}{1 - x1}}\]

8. Simplified 6.1

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

10. Applied flip3-- 5.3

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

11. Simplified 5.2

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

13. Applied *-un-lft-identity 5.2

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

14. Applied add-cube-cbrt 5.2

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

15. Applied times-frac 5.1

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

16. Applied unpow-prod-down 5.1

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

17. Simplified 5.1

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

18. Final simplification 5.1

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

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))