Average Error: 8.4 → 2.4
Time: 3.1s
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.9814:\\ \;\;\;\;e^{\log \log \left(e^{\frac{\frac{x0 \cdot x0}{{\left(1 - x1\right)}^{2}} - x0 \cdot x0}{x0 + \frac{x0}{\left(1 - \sqrt{x1}\right) \cdot \left(1 + \sqrt{x1}\right)}}}\right)}\\ \mathbf{else}:\\ \;\;\;\;x0 \cdot \left(\left(\mathsf{fma}\left(x1, x1, x1\right) + {x1}^{3}\right) + {x1}^{4}\right)\\ \end{array} \]
\frac{x0}{1 - x1} - x0
↓
\begin{array}{l}
\mathbf{if}\;1 - x1 \leq 0.9814:\\
\;\;\;\;e^{\log \log \left(e^{\frac{\frac{x0 \cdot x0}{{\left(1 - x1\right)}^{2}} - x0 \cdot x0}{x0 + \frac{x0}{\left(1 - \sqrt{x1}\right) \cdot \left(1 + \sqrt{x1}\right)}}}\right)}\\

\mathbf{else}:\\
\;\;\;\;x0 \cdot \left(\left(\mathsf{fma}\left(x1, x1, x1\right) + {x1}^{3}\right) + {x1}^{4}\right)\\


\end{array}

(FPCore (x0 x1) :precision binary64 (- (/ x0 (- 1.0 x1)) x0))
↓
(FPCore (x0 x1)
 :precision binary64
 (if (<= (- 1.0 x1) 0.9814)
   (exp
    (log
     (log
      (exp
       (/
        (- (/ (* x0 x0) (pow (- 1.0 x1) 2.0)) (* x0 x0))
        (+ x0 (/ x0 (* (- 1.0 (sqrt x1)) (+ 1.0 (sqrt x1))))))))))
   (* x0 (+ (+ (fma x1 x1 x1) (pow x1 3.0)) (pow x1 4.0)))))
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.9814) {
		tmp = exp(log(log(exp((((x0 * x0) / pow((1.0 - x1), 2.0)) - (x0 * x0)) / (x0 + (x0 / ((1.0 - sqrt(x1)) * (1.0 + sqrt(x1)))))))));
	} else {
		tmp = x0 * ((fma(x1, x1, x1) + pow(x1, 3.0)) + pow(x1, 4.0));
	}
	return tmp;
}

Error

Bits error versus x0

Bits error versus x1

Target

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

Derivation

  1. Split input into 2 regimes

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

    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.0

      \[\leadsto \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{\color{blue}{x0 + \frac{x0}{1 - x1}}} \]
    5. Using strategy rm

    6. Applied add-sqr-sqrt_binary644.0

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

    7. Applied add-sqr-sqrt_binary644.0

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

    8. Applied difference-of-squares_binary644.0

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

    9. Applied add-sqr-sqrt_binary644.0

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

    10. Applied times-frac_binary643.9

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

    11. Simplified3.9

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

    12. Simplified3.9

      \[\leadsto \frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{x0 + \frac{\sqrt{x0}}{1 + \sqrt{x1}} \cdot \color{blue}{\frac{\sqrt{x0}}{1 - \sqrt{x1}}}} \]
    13. Using strategy rm

    14. Applied add-log-exp_binary641.6

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

    15. Simplified1.6

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

    17. Applied add-exp-log_binary641.0

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

    if 0.98140000000000005 < (-.f64 1 x1)

    1. Initial program 11.3

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

    2. Taylor expanded around 0 3.9

      \[\leadsto \color{blue}{{x1}^{2} \cdot x0 + \left({x1}^{4} \cdot x0 + \left(x1 \cdot x0 + {x1}^{3} \cdot x0\right)\right)} \]

    3. Simplified3.9

      \[\leadsto \color{blue}{x0 \cdot \left(\left(\mathsf{fma}\left(x1, x1, x1\right) + {x1}^{3}\right) + {x1}^{4}\right)} \]
  3. Recombined 2 regimes into one program.

  4. Final simplification2.4

    \[\leadsto \begin{array}{l} \mathbf{if}\;1 - x1 \leq 0.9814:\\ \;\;\;\;e^{\log \log \left(e^{\frac{\frac{x0 \cdot x0}{{\left(1 - x1\right)}^{2}} - x0 \cdot x0}{x0 + \frac{x0}{\left(1 - \sqrt{x1}\right) \cdot \left(1 + \sqrt{x1}\right)}}}\right)}\\ \mathbf{else}:\\ \;\;\;\;x0 \cdot \left(\left(\mathsf{fma}\left(x1, x1, x1\right) + {x1}^{3}\right) + {x1}^{4}\right)\\ \end{array} \]

Reproduce

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