(- (/ x0 (- 1 x1)) x0)

Average Error: 8.4 → 2.7

Time: 5.6s

Precision: binary64

\[x0 = 1.855 \land x1 = 0.000209 \lor x0 = 2.985 \land x1 = 0.0186\]

Math

\[\frac{x0}{1 - x1} - x0 \]

↓

\[\begin{array}{l} t_0 := \sqrt[3]{x0} \cdot \sqrt[3]{x0}\\ t_1 := \sqrt[3]{x0} \cdot t_0\\ {e}^{\log \left(\mathsf{fma}\left(x0, \frac{1}{1 - x1}, -t_1\right)\right)} + \mathsf{fma}\left(-\sqrt[3]{x0}, t_0, t_1\right) \end{array} \]

FPCore

(FPCore (x0 x1) :precision binary64 (- (/ x0 (- 1.0 x1)) x0))

↓

(FPCore (x0 x1)
 :precision binary64
 (let* ((t_0 (* (cbrt x0) (cbrt x0))) (t_1 (* (cbrt x0) t_0)))
   (+
    (pow E (log (fma x0 (/ 1.0 (- 1.0 x1)) (- t_1))))
    (fma (- (cbrt x0)) t_0 t_1))))

C

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);
	double t_1 = cbrt(x0) * t_0;
	return pow(((double) M_E), log(fma(x0, (1.0 / (1.0 - x1)), -t_1))) + fma(-cbrt(x0), t_0, t_1);
}

Error

Bits error versus x0

Bits error versus x1

Target

Original	8.4
Target	0.5
Herbie	2.7

\[\frac{x0 \cdot x1}{1 - x1} \]

Derivation

1. Initial program 8.4

   \[\frac{x0}{1 - x1} - x0 \]

2. Applied add-cube-cbrt_binary64 8.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_binary64 8.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_binary64 3.8

   \[\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_binary64 3.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_binary64 3.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_binary64 3.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_binary64 2.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. Simplified 2.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. Final simplification 2.7

    \[\leadsto {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) \]

Reproduce

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