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

Average Error: 8.4 → 5.2

Time: 2.6s

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

C

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

↓

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

Error

Bits error versus x0

Bits error versus x1

Target

Original	8.4
Target	0.5
Herbie	5.2

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

Derivation

1. Initial program 8.4

   \[\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. Using strategy rm

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

7. Simplified 6.1

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

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

10. Simplified 5.3

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

12. Applied flip3-- 5.3

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

13. Applied associate-/r/ 5.3

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

14. Applied unpow-prod-down 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(\color{blue}{{\left(\frac{\frac{x0}{1 - x1}}{{1}^{3} - {x1}^{3}}\right)}^{6} \cdot {\left(1 \cdot 1 + \left(x1 \cdot x1 + 1 \cdot x1\right)\right)}^{6}} + {x0}^{6}\right) + {\left(\frac{\frac{x0}{1 - x1}}{1 - x1}\right)}^{3} \cdot {x0}^{3}}}{x0 \cdot x0 + \frac{\frac{x0}{1 - x1}}{1 - x1} \cdot \left(\frac{\frac{x0}{1 - x1}}{1 - x1} + x0\right)}}{\frac{x0}{1 - x1} + x0}\]

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

16. Final simplification 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({\left(\frac{\frac{x0}{1 - x1}}{{1}^{3} - {x1}^{3}}\right)}^{6} \cdot {\left(x1 \cdot \left(x1 + 1\right) + 1 \cdot 1\right)}^{6} + {x0}^{6}\right) + {\left(\frac{\frac{x0}{1 - x1}}{1 - x1}\right)}^{3} \cdot {x0}^{3}}}{x0 \cdot x0 + \frac{\frac{x0}{1 - x1}}{1 - x1} \cdot \left(\frac{\frac{x0}{1 - x1}}{1 - x1} + x0\right)}}{\frac{x0}{1 - x1} + x0}\]

Reproduce

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