Average Error: 8.4 → 2.7
Time: 4.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} t_0 := \sqrt[3]{x0} \cdot \sqrt[3]{x0}\\ {e}^{\log \left(x0 \cdot \left(-1 + \frac{1}{1 - x1}\right)\right)} + \mathsf{fma}\left(-\sqrt[3]{x0}, t_0, \sqrt[3]{x0} \cdot t_0\right) \end{array} \]
\frac{x0}{1 - x1} - x0
\begin{array}{l}
t_0 := \sqrt[3]{x0} \cdot \sqrt[3]{x0}\\
{e}^{\log \left(x0 \cdot \left(-1 + \frac{1}{1 - x1}\right)\right)} + \mathsf{fma}\left(-\sqrt[3]{x0}, t_0, \sqrt[3]{x0} \cdot t_0\right)
\end{array}
(FPCore (x0 x1) :precision binary64 (- (/ x0 (- 1.0 x1)) x0))
(FPCore (x0 x1)
 :precision binary64
 (let* ((t_0 (* (cbrt x0) (cbrt x0))))
   (+
    (pow E (log (* x0 (+ -1.0 (/ 1.0 (- 1.0 x1))))))
    (fma (- (cbrt x0)) t_0 (* (cbrt x0) t_0)))))
double code(double x0, double x1) {
	return (x0 / (1.0 - x1)) - x0;
}
double code(double x0, double x1) {
	double t_0 = cbrt(x0) * cbrt(x0);
	return pow(((double) M_E), log(x0 * (-1.0 + (1.0 / (1.0 - x1))))) + fma(-cbrt(x0), t_0, (cbrt(x0) * t_0));
}

Error

Bits error versus x0

Bits error versus x1

Target

Original8.4
Target0.5
Herbie2.7
\[\frac{x0 \cdot x1}{1 - x1} \]

Derivation

  1. Initial program 8.4

    \[\frac{x0}{1 - x1} - x0 \]
  2. Applied add-cube-cbrt_binary648.4

    \[\leadsto \frac{x0}{1 - x1} - \color{blue}{\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \sqrt[3]{x0}} \]
  3. Applied div-inv_binary648.1

    \[\leadsto \color{blue}{x0 \cdot \frac{1}{1 - x1}} - \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \sqrt[3]{x0} \]
  4. Applied prod-diff_binary643.7

    \[\leadsto \color{blue}{\mathsf{fma}\left(x0, \frac{1}{1 - x1}, -\sqrt[3]{x0} \cdot \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)\right) + \mathsf{fma}\left(-\sqrt[3]{x0}, \sqrt[3]{x0} \cdot \sqrt[3]{x0}, \sqrt[3]{x0} \cdot \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)\right)} \]
  5. Applied add-exp-log_binary643.5

    \[\leadsto \color{blue}{e^{\log \left(\mathsf{fma}\left(x0, \frac{1}{1 - x1}, -\sqrt[3]{x0} \cdot \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)\right)\right)}} + \mathsf{fma}\left(-\sqrt[3]{x0}, \sqrt[3]{x0} \cdot \sqrt[3]{x0}, \sqrt[3]{x0} \cdot \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)\right) \]
  6. Applied pow1_binary643.5

    \[\leadsto e^{\log \color{blue}{\left({\left(\mathsf{fma}\left(x0, \frac{1}{1 - x1}, -\sqrt[3]{x0} \cdot \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)\right)\right)}^{1}\right)}} + \mathsf{fma}\left(-\sqrt[3]{x0}, \sqrt[3]{x0} \cdot \sqrt[3]{x0}, \sqrt[3]{x0} \cdot \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)\right) \]
  7. Applied log-pow_binary643.5

    \[\leadsto e^{\color{blue}{1 \cdot \log \left(\mathsf{fma}\left(x0, \frac{1}{1 - x1}, -\sqrt[3]{x0} \cdot \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)\right)\right)}} + \mathsf{fma}\left(-\sqrt[3]{x0}, \sqrt[3]{x0} \cdot \sqrt[3]{x0}, \sqrt[3]{x0} \cdot \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)\right) \]
  8. Applied exp-prod_binary642.7

    \[\leadsto \color{blue}{{\left(e^{1}\right)}^{\log \left(\mathsf{fma}\left(x0, \frac{1}{1 - x1}, -\sqrt[3]{x0} \cdot \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)\right)\right)}} + \mathsf{fma}\left(-\sqrt[3]{x0}, \sqrt[3]{x0} \cdot \sqrt[3]{x0}, \sqrt[3]{x0} \cdot \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)\right) \]
  9. Simplified2.7

    \[\leadsto {\color{blue}{e}}^{\log \left(\mathsf{fma}\left(x0, \frac{1}{1 - x1}, -\sqrt[3]{x0} \cdot \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)\right)\right)} + \mathsf{fma}\left(-\sqrt[3]{x0}, \sqrt[3]{x0} \cdot \sqrt[3]{x0}, \sqrt[3]{x0} \cdot \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)\right) \]
  10. Taylor expanded in x0 around -inf 2.7

    \[\leadsto {e}^{\log \color{blue}{\left(-1 \cdot \left(\left(1 - \frac{1}{1 - x1}\right) \cdot x0\right)\right)}} + \mathsf{fma}\left(-\sqrt[3]{x0}, \sqrt[3]{x0} \cdot \sqrt[3]{x0}, \sqrt[3]{x0} \cdot \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)\right) \]
  11. Final simplification2.7

    \[\leadsto {e}^{\log \left(x0 \cdot \left(-1 + \frac{1}{1 - x1}\right)\right)} + \mathsf{fma}\left(-\sqrt[3]{x0}, \sqrt[3]{x0} \cdot \sqrt[3]{x0}, \sqrt[3]{x0} \cdot \left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)\right) \]

Reproduce

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