Average Error: 8.4 → 3.3
Time: 6.2s
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}\;1 - x1 \leq 0.9905955:\\ \;\;\;\;\frac{x0 \cdot \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} - x0\right)}{\frac{x0 \cdot x0 - \frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{x0 - \frac{1}{\frac{1 - x1}{x0}}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x0 \cdot e^{\log \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} - x0\right)}}{\frac{\log \left(e^{x0 \cdot x0 - \frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}\right)}{x0 - \frac{x0}{1 - x1}}}\\ \end{array}\]
\frac{x0}{1 - x1} - x0
↓
\begin{array}{l}
\mathbf{if}\;1 - x1 \leq 0.9905955:\\
\;\;\;\;\frac{x0 \cdot \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} - x0\right)}{\frac{x0 \cdot x0 - \frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{x0 - \frac{1}{\frac{1 - x1}{x0}}}}\\

\mathbf{else}:\\
\;\;\;\;\frac{x0 \cdot e^{\log \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} - x0\right)}}{\frac{\log \left(e^{x0 \cdot x0 - \frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}\right)}{x0 - \frac{x0}{1 - x1}}}\\

\end{array}
(FPCore (x0 x1) :precision binary64 (- (/ x0 (- 1.0 x1)) x0))
↓
(FPCore (x0 x1)
 :precision binary64
 (if (<= (- 1.0 x1) 0.9905955)
   (/
    (* x0 (- (/ x0 (* (- 1.0 x1) (- 1.0 x1))) x0))
    (/
     (- (* x0 x0) (* (/ x0 (- 1.0 x1)) (/ x0 (- 1.0 x1))))
     (- x0 (/ 1.0 (/ (- 1.0 x1) x0)))))
   (/
    (* x0 (exp (log (- (/ x0 (* (- 1.0 x1) (- 1.0 x1))) x0))))
    (/
     (log (exp (- (* x0 x0) (* (/ x0 (- 1.0 x1)) (/ x0 (- 1.0 x1))))))
     (- 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 ((1.0 - x1) <= 0.9905955) {
		tmp = (x0 * ((x0 / ((1.0 - x1) * (1.0 - x1))) - x0)) / (((x0 * x0) - ((x0 / (1.0 - x1)) * (x0 / (1.0 - x1)))) / (x0 - (1.0 / ((1.0 - x1) / x0))));
	} else {
		tmp = (x0 * exp(log((x0 / ((1.0 - x1) * (1.0 - x1))) - x0))) / (log(exp((x0 * x0) - ((x0 / (1.0 - x1)) * (x0 / (1.0 - x1))))) / (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.4
Target0.5
Herbie3.3
\[\frac{x0 \cdot x1}{1 - x1}\]

Derivation

  1. Split input into 2 regimes

  2. if (-.f64 1 x1) < 0.99059549999999996

    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 flip-+_binary645.8

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

    9. Applied clear-num_binary643.3

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

    if 0.99059549999999996 < (-.f64 1 x1)

    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 flip-+_binary647.7

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

    9. Applied add-log-exp_binary647.7

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

    10. Applied add-log-exp_binary647.7

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

    11. Applied diff-log_binary643.7

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

    12. Simplified3.7

      \[\leadsto \frac{x0 \cdot \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} - x0\right)}{\frac{\log \color{blue}{\left(e^{x0 \cdot x0 - \frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}\right)}}{x0 - \frac{x0}{1 - x1}}}\]
    13. Using strategy rm

    14. Applied add-exp-log_binary643.3

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

  4. Final simplification3.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;1 - x1 \leq 0.9905955:\\ \;\;\;\;\frac{x0 \cdot \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} - x0\right)}{\frac{x0 \cdot x0 - \frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}{x0 - \frac{1}{\frac{1 - x1}{x0}}}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x0 \cdot e^{\log \left(\frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)} - x0\right)}}{\frac{\log \left(e^{x0 \cdot x0 - \frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}\right)}{x0 - \frac{x0}{1 - x1}}}\\ \end{array}\]

Reproduce

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