Average Error: 8.4 → 0
Time: 2.5s
Precision: binary64
\[x0 = 1.855 \land x1 = 0.000209 \lor x0 = 2.985 \land x1 = 0.0186\]
\[\frac{x0}{1 - x1} - x0 \]
\[\frac{e^{\log \left(\left(x0 \cdot x0\right) \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(-x1\right) \cdot -2\right)\right)}}{x0 + \frac{x0}{1 - x1}} \]
\frac{x0}{1 - x1} - x0
\frac{e^{\log \left(\left(x0 \cdot x0\right) \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(-x1\right) \cdot -2\right)\right)}}{x0 + \frac{x0}{1 - x1}}
(FPCore (x0 x1) :precision binary64 (- (/ x0 (- 1.0 x1)) x0))
(FPCore (x0 x1)
 :precision binary64
 (/
  (exp (log (* (* x0 x0) (expm1 (* (log1p (- x1)) -2.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 exp(log((x0 * x0) * expm1(log1p(-x1) * -2.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
Herbie0
\[\frac{x0 \cdot x1}{1 - x1} \]

Derivation

  1. Initial program 8.4

    \[\frac{x0}{1 - x1} - x0 \]
  2. Using strategy rm
  3. Applied pow1_binary648.4

    \[\leadsto \color{blue}{{\left(\frac{x0}{1 - x1}\right)}^{1}} - x0 \]
  4. Applied sqr-pow_binary647.5

    \[\leadsto \color{blue}{{\left(\frac{x0}{1 - x1}\right)}^{\left(\frac{1}{2}\right)} \cdot {\left(\frac{x0}{1 - x1}\right)}^{\left(\frac{1}{2}\right)}} - x0 \]
  5. Simplified7.5

    \[\leadsto \color{blue}{\sqrt{\frac{x0}{1 - x1}}} \cdot {\left(\frac{x0}{1 - x1}\right)}^{\left(\frac{1}{2}\right)} - x0 \]
  6. Simplified7.5

    \[\leadsto \sqrt{\frac{x0}{1 - x1}} \cdot \color{blue}{\sqrt{\frac{x0}{1 - x1}}} - x0 \]
  7. Using strategy rm
  8. Applied flip--_binary647.7

    \[\leadsto \color{blue}{\frac{\left(\sqrt{\frac{x0}{1 - x1}} \cdot \sqrt{\frac{x0}{1 - x1}}\right) \cdot \left(\sqrt{\frac{x0}{1 - x1}} \cdot \sqrt{\frac{x0}{1 - x1}}\right) - x0 \cdot x0}{\sqrt{\frac{x0}{1 - x1}} \cdot \sqrt{\frac{x0}{1 - x1}} + x0}} \]
  9. Simplified7.8

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

    \[\leadsto \frac{{\left(\frac{x0}{1 - x1}\right)}^{2} - x0 \cdot x0}{\color{blue}{x0 + \frac{x0}{1 - x1}}} \]
  11. Taylor expanded around 0 7.3

    \[\leadsto \frac{\color{blue}{{x0}^{2} \cdot \left(\frac{1}{{\left(1 - x1\right)}^{2}} - 1\right)}}{x0 + \frac{x0}{1 - x1}} \]
  12. Simplified0.5

    \[\leadsto \frac{\color{blue}{\left(x0 \cdot x0\right) \cdot \mathsf{expm1}\left(-2 \cdot \mathsf{log1p}\left(-x1\right)\right)}}{x0 + \frac{x0}{1 - x1}} \]
  13. Using strategy rm
  14. Applied add-exp-log_binary640

    \[\leadsto \frac{\color{blue}{e^{\log \left(\left(x0 \cdot x0\right) \cdot \mathsf{expm1}\left(-2 \cdot \mathsf{log1p}\left(-x1\right)\right)\right)}}}{x0 + \frac{x0}{1 - x1}} \]
  15. Final simplification0

    \[\leadsto \frac{e^{\log \left(\left(x0 \cdot x0\right) \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(-x1\right) \cdot -2\right)\right)}}{x0 + \frac{x0}{1 - x1}} \]

Reproduce

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