Average Error: 8.3 → 3.9
Time: 13.6s
Precision: binary64
\[x0 = 1.855 \land x1 = 0.000209 \lor x0 = 2.985 \land x1 = 0.0186\]
\[\frac{x0}{1 - x1} - x0\]
↓
\[\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}}{{x0}^{6} + \frac{{x0}^{6} + \frac{{x0}^{6}}{{\left(1 - x1\right)}^{6}}}{{\left(1 + \sqrt{x1}\right)}^{6} \cdot {\left(1 - \sqrt{x1}\right)}^{6}}}}{x0 \cdot \left(\frac{x0}{{\left(1 - x1\right)}^{4}} + \left(x0 + \frac{x0}{{\left(\sqrt{1 - x1}\right)}^{4}}\right)\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 \left(\frac{x0}{{\left(1 - x1\right)}^{4}} + \left(x0 + \frac{x0}{{\left(\sqrt{1 - x1}\right)}^{4}}\right)\right)}}{x0 + \frac{x0}{1 - x1}}\\ \end{array}\]
\frac{x0}{1 - x1} - x0
↓
\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}}{{x0}^{6} + \frac{{x0}^{6} + \frac{{x0}^{6}}{{\left(1 - x1\right)}^{6}}}{{\left(1 + \sqrt{x1}\right)}^{6} \cdot {\left(1 - \sqrt{x1}\right)}^{6}}}}{x0 \cdot \left(\frac{x0}{{\left(1 - x1\right)}^{4}} + \left(x0 + \frac{x0}{{\left(\sqrt{1 - x1}\right)}^{4}}\right)\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 \left(\frac{x0}{{\left(1 - x1\right)}^{4}} + \left(x0 + \frac{x0}{{\left(\sqrt{1 - x1}\right)}^{4}}\right)\right)}}{x0 + \frac{x0}{1 - x1}}\\

\end{array}
(FPCore (x0 x1) :precision binary64 (- (/ x0 (- 1.0 x1)) x0))
↓
(FPCore (x0 x1)
 :precision binary64
 (if (<= x1 0.018204597656249998)
   (/
    (*
     x0
     (/
      (/
       (-
        (pow (/ (pow x0 3.0) (pow (- 1.0 x1) 6.0)) 3.0)
        (pow (pow x0 3.0) 3.0))
       (+
        (pow x0 6.0)
        (/
         (+ (pow x0 6.0) (/ (pow x0 6.0) (pow (- 1.0 x1) 6.0)))
         (* (pow (+ 1.0 (sqrt x1)) 6.0) (pow (- 1.0 (sqrt x1)) 6.0)))))
      (*
       x0
       (+
        (/ x0 (pow (- 1.0 x1) 4.0))
        (+ x0 (/ x0 (pow (sqrt (- 1.0 x1)) 4.0)))))))
    (+ x0 (/ x0 (- 1.0 x1))))
   (/
    (*
     x0
     (/
      (-
       (/
        (pow x0 3.0)
        (* (pow (+ 1.0 (sqrt x1)) 6.0) (pow (- 1.0 (sqrt x1)) 6.0)))
       (pow x0 3.0))
      (*
       x0
       (+
        (/ x0 (pow (- 1.0 x1) 4.0))
        (+ x0 (/ x0 (pow (sqrt (- 1.0 x1)) 4.0)))))))
    (+ x0 (/ x0 (- 1.0 x1))))))
double code(double x0, double x1) {
	return (x0 / (1.0 - x1)) - x0;
}
↓
double code(double x0, double x1) {
	double tmp;
	if (x1 <= 0.018204597656249998) {
		tmp = (x0 * (((pow((pow(x0, 3.0) / pow((1.0 - x1), 6.0)), 3.0) - pow(pow(x0, 3.0), 3.0)) / (pow(x0, 6.0) + ((pow(x0, 6.0) + (pow(x0, 6.0) / pow((1.0 - x1), 6.0))) / (pow((1.0 + sqrt(x1)), 6.0) * pow((1.0 - sqrt(x1)), 6.0))))) / (x0 * ((x0 / pow((1.0 - x1), 4.0)) + (x0 + (x0 / pow(sqrt(1.0 - x1), 4.0))))))) / (x0 + (x0 / (1.0 - x1)));
	} else {
		tmp = (x0 * (((pow(x0, 3.0) / (pow((1.0 + sqrt(x1)), 6.0) * pow((1.0 - sqrt(x1)), 6.0))) - pow(x0, 3.0)) / (x0 * ((x0 / pow((1.0 - x1), 4.0)) + (x0 + (x0 / pow(sqrt(1.0 - x1), 4.0))))))) / (x0 + (x0 / (1.0 - x1)));
	}
	return tmp;
}

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.3
Target0.5
Herbie3.9
\[\frac{x0 \cdot x1}{1 - x1}\]

Derivation

  1. Split input into 2 regimes

  2. if x1 < 0.0182045976562499982

    1. Initial program 11.3

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

    3. Applied flip--_binary6411.4

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

    4. Simplified9.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. Simplified9.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--_binary647.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. Simplified7.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. Simplified7.8

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

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

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

    14. Applied add-sqr-sqrt_binary646.3

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

    15. Applied *-un-lft-identity_binary646.3

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

    16. Applied difference-of-squares_binary646.2

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

    17. Applied unpow-prod-down_binary646.2

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

    if 0.0182045976562499982 < x1

    1. Initial program 5.5

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

    3. Applied flip--_binary644.0

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

    4. Simplified4.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. Simplified4.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--_binary644.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. Simplified4.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. Simplified4.4

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

    11. Applied add-sqr-sqrt_binary644.4

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

    12. Applied *-un-lft-identity_binary644.4

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

    13. Applied difference-of-squares_binary644.4

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

    14. Applied unpow-prod-down_binary641.6

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

  4. Final simplification3.9

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

Reproduce

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