Average Error: 8.4 → 4.5
Time: 1.8min
Precision: binary64
Cost: 4800
\[x0 = 1.855 \land x1 = 0.000209 \lor x0 = 2.985 \land x1 = 0.0186\]
\[\frac{x0}{1 - x1} - x0\]
↓
\[\frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{\log \left(e^{{\left(1 - x1\right)}^{6}}\right)}\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)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]
\frac{x0}{1 - x1} - x0
↓
\frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{\log \left(e^{{\left(1 - x1\right)}^{6}}\right)}\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)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}
(FPCore (x0 x1) :precision binary64 (- (/ x0 (- 1.0 x1)) x0))
↓
(FPCore (x0 x1)
 :precision binary64
 (/
  (*
   x0
   (/
    (/
     (-
      (pow (/ (pow x0 3.0) (log (exp (pow (- 1.0 x1) 6.0)))) 3.0)
      (pow (pow x0 3.0) 3.0))
     (+
      (/ (pow x0 6.0) (pow (- 1.0 x1) 12.0))
      (+ (pow x0 6.0) (pow (/ x0 (- 1.0 x1)) 6.0))))
    (+
     (* x0 x0)
     (* (/ x0 (- 1.0 x1)) (+ (/ x0 (- 1.0 x1)) (/ x0 (pow (- 1.0 x1) 3.0)))))))
  (+ x0 (/ x0 (- 1.0 x1)))))
double code(double x0, double x1) {
	return (x0 / (1.0 - x1)) - x0;
}
↓
double code(double x0, double x1) {
	return (x0 * (((pow((pow(x0, 3.0) / log(exp(pow((1.0 - x1), 6.0)))), 3.0) - pow(pow(x0, 3.0), 3.0)) / ((pow(x0, 6.0) / pow((1.0 - x1), 12.0)) + (pow(x0, 6.0) + pow((x0 / (1.0 - x1)), 6.0)))) / ((x0 * x0) + ((x0 / (1.0 - x1)) * ((x0 / (1.0 - x1)) + (x0 / pow((1.0 - x1), 3.0))))))) / (x0 + (x0 / (1.0 - x1)));
}

Error

Bits error versus x0

Bits error versus x1

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original8.4
Target0.5
Herbie4.5
\[\frac{x0 \cdot x1}{1 - x1}\]
Alternative 1
Accuracy4.9
Cost5120
\[\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 - x1\right)}^{12}} + \left({x0}^{6} + {\left({\left(\frac{x0}{1 - x1}\right)}^{\left(\sqrt[3]{6} \cdot \sqrt[3]{6}\right)}\right)}^{\left(\sqrt[3]{6}\right)}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]
Alternative 2
Accuracy3.9
Cost5889
\[\begin{array}{l} \mathbf{if}\;\frac{x0}{1 - x1} - x0 \leq 0.00038777604519357745:\\ \;\;\;\;\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 - x1\right)}^{12}} + \left({x0}^{6} + {\left(\frac{1}{1 + \sqrt{x1}}\right)}^{6} \cdot {\left(\frac{x0}{1 - \sqrt{x1}}\right)}^{6}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 + \sqrt{x1}\right)}^{6} \cdot {\left(1 - \sqrt{x1}\right)}^{6}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \end{array}\]
Alternative 3
Accuracy3.9
Cost5505
\[\begin{array}{l} \mathbf{if}\;x1 \leq 0.018204597656249998:\\ \;\;\;\;\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 - x1\right)}^{12}} + \left({x0}^{6} + {\left(\frac{1}{1 + \sqrt{x1}}\right)}^{6} \cdot {\left(\frac{x0}{1 - \sqrt{x1}}\right)}^{6}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 + \sqrt{x1}\right)}^{6} \cdot {\left(1 - \sqrt{x1}\right)}^{6}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \end{array}\]
Alternative 4
Accuracy3.9
Cost5441
\[\begin{array}{l} \mathbf{if}\;1 - x1 \leq 0.9814:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 + \sqrt{x1}\right)}^{6} \cdot {\left(1 - \sqrt{x1}\right)}^{6}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{\left(\frac{{x0}^{3}}{{\left({\left(1 - x1\right)}^{\left(\sqrt[3]{6} \cdot \sqrt[3]{6}\right)}\right)}^{\left(\sqrt[3]{6}\right)}}\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)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \end{array}\]
Alternative 5
Accuracy4.0
Cost6081
\[\begin{array}{l} \mathbf{if}\;1 - x1 \leq 0.9814:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 + \sqrt{x1}\right)}^{6} \cdot {\left(1 - \sqrt{x1}\right)}^{6}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \mathbf{else}:\\ \;\;\;\;\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 - x1\right)}^{12}} + \left({x0}^{6} + {\left(\frac{\sqrt{x0}}{\sqrt[3]{1 - x1} \cdot \sqrt[3]{1 - x1}}\right)}^{6} \cdot {\left(\frac{\sqrt{x0}}{\sqrt[3]{1 - x1}}\right)}^{6}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \end{array}\]
Alternative 6
Accuracy4.0
Cost5441
\[\begin{array}{l} \mathbf{if}\;1 - x1 \leq 0.9814:\\ \;\;\;\;\frac{x0 \cdot \frac{\frac{{x0}^{3}}{{\left(1 + \sqrt{x1}\right)}^{6} \cdot {\left(1 - \sqrt{x1}\right)}^{6}} - {x0}^{3}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \mathbf{else}:\\ \;\;\;\;\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[3]{1 - x1}\right)}^{24} \cdot {\left(1 - x1\right)}^{4}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\\ \end{array}\]
Alternative 7
Accuracy5.5
Cost5120
\[\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[3]{1 - x1}\right)}^{24} \cdot {\left(1 - x1\right)}^{4}} + \left({x0}^{6} + {\left(\frac{x0}{1 - x1}\right)}^{6}\right)}}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]
Alternative 8
Accuracy7.3
Cost4160
\[\frac{x0 \cdot \frac{\left(x0 \cdot \sqrt{x0} + \frac{x0 \cdot \sqrt{x0}}{{\left(1 - x1\right)}^{3}}\right) \cdot \left(\frac{x0 \cdot \sqrt{x0}}{{\left(1 - x1\right)}^{3}} - x0 \cdot \sqrt{x0}\right)}{x0 \cdot x0 + \frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} + \frac{x0}{{\left(1 - x1\right)}^{3}}\right)}}{x0 + \frac{x0}{1 - x1}}\]

Derivation

  1. Initial program 8.4

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

  3. Applied flip--_binary64_24407.7

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

  4. Simplified6.9

    \[\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. Simplified6.9

    \[\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--_binary64_24696.1

    \[\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. Simplified6.1

    \[\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. Simplified6.1

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

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

  12. Simplified5.2

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

  14. Applied add-log-exp_binary64_25044.5

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

  15. Final simplification4.5

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

Reproduce

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