\[\log \left(x + \sqrt{x \cdot x + 1}\right)\]

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.004281043358186797931352884916123002768:\\ \;\;\;\;\log \left(\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} + \frac{0.0625}{{x}^{5}}\right)\right)\\ \mathbf{elif}\;x \le 0.8904752561288424850260980747407302260399:\\ \;\;\;\;\mathsf{fma}\left(\frac{{x}^{3}}{{\left(\sqrt{1}\right)}^{3}}, \frac{-1}{6}, \log \left(\sqrt{1}\right) + \frac{x}{\sqrt{1}}\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(\mathsf{fma}\left(x, 2, \mathsf{fma}\left(\frac{1}{x}, \frac{1}{2}, \frac{-1}{8} \cdot \frac{1 \cdot 1}{{x}^{3}}\right)\right)\right)\\ \end{array}\]

\log \left(x + \sqrt{x \cdot x + 1}\right)

↓

\begin{array}{l}
\mathbf{if}\;x \le -1.004281043358186797931352884916123002768:\\
\;\;\;\;\log \left(\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} + \frac{0.0625}{{x}^{5}}\right)\right)\\

\mathbf{elif}\;x \le 0.8904752561288424850260980747407302260399:\\
\;\;\;\;\mathsf{fma}\left(\frac{{x}^{3}}{{\left(\sqrt{1}\right)}^{3}}, \frac{-1}{6}, \log \left(\sqrt{1}\right) + \frac{x}{\sqrt{1}}\right)\\

\mathbf{else}:\\
\;\;\;\;\log \left(\mathsf{fma}\left(x, 2, \mathsf{fma}\left(\frac{1}{x}, \frac{1}{2}, \frac{-1}{8} \cdot \frac{1 \cdot 1}{{x}^{3}}\right)\right)\right)\\

\end{array}

double f(double x) {
        double r128340 = x;
        double r128341 = r128340 * r128340;
        double r128342 = 1.0;
        double r128343 = r128341 + r128342;
        double r128344 = sqrt(r128343);
        double r128345 = r128340 + r128344;
        double r128346 = log(r128345);
        return r128346;
}

↓

double f(double x) {
        double r128347 = x;
        double r128348 = -1.0042810433581868;
        bool r128349 = r128347 <= r128348;
        double r128350 = 0.125;
        double r128351 = 3.0;
        double r128352 = pow(r128347, r128351);
        double r128353 = r128350 / r128352;
        double r128354 = 0.5;
        double r128355 = r128354 / r128347;
        double r128356 = 0.0625;
        double r128357 = 5.0;
        double r128358 = pow(r128347, r128357);
        double r128359 = r128356 / r128358;
        double r128360 = r128355 + r128359;
        double r128361 = r128353 - r128360;
        double r128362 = log(r128361);
        double r128363 = 0.8904752561288425;
        bool r128364 = r128347 <= r128363;
        double r128365 = 1.0;
        double r128366 = sqrt(r128365);
        double r128367 = pow(r128366, r128351);
        double r128368 = r128352 / r128367;
        double r128369 = -0.16666666666666666;
        double r128370 = log(r128366);
        double r128371 = r128347 / r128366;
        double r128372 = r128370 + r128371;
        double r128373 = fma(r128368, r128369, r128372);
        double r128374 = 2.0;
        double r128375 = r128365 / r128347;
        double r128376 = 0.5;
        double r128377 = -0.125;
        double r128378 = r128365 * r128365;
        double r128379 = r128378 / r128352;
        double r128380 = r128377 * r128379;
        double r128381 = fma(r128375, r128376, r128380);
        double r128382 = fma(r128347, r128374, r128381);
        double r128383 = log(r128382);
        double r128384 = r128364 ? r128373 : r128383;
        double r128385 = r128349 ? r128362 : r128384;
        return r128385;
}

Original	53.1
Target	45.4
Herbie	0.3

Derivation

Split input into 3 regimes
if x < -1.0042810433581868
1. Initial program 62.8
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around -inf 0.2
  \[\leadsto \log \color{blue}{\left(0.125 \cdot \frac{1}{{x}^{3}} - \left(0.5 \cdot \frac{1}{x} + 0.0625 \cdot \frac{1}{{x}^{5}}\right)\right)}\]
3. Simplified0.2
  \[\leadsto \log \color{blue}{\left(\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} + \frac{0.0625}{{x}^{5}}\right)\right)}\]
if -1.0042810433581868 < x < 0.8904752561288425
1. Initial program 58.6
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around 0 0.3
  \[\leadsto \color{blue}{\left(\log \left(\sqrt{1}\right) + \frac{x}{\sqrt{1}}\right) - \frac{1}{6} \cdot \frac{{x}^{3}}{{\left(\sqrt{1}\right)}^{3}}}\]
3. Simplified0.3
  \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{{x}^{3}}{{\left(\sqrt{1}\right)}^{3}}, \frac{-1}{6}, \log \left(\sqrt{1}\right) + \frac{x}{\sqrt{1}}\right)}\]
if 0.8904752561288425 < x
1. Initial program 32.2
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Using strategy rm
3. Applied add-sqr-sqrt32.2
  \[\leadsto \log \left(x + \sqrt{x \cdot x + \color{blue}{\sqrt{1} \cdot \sqrt{1}}}\right)\]
4. Applied hypot-def0.1
  \[\leadsto \log \left(x + \color{blue}{\mathsf{hypot}\left(x, \sqrt{1}\right)}\right)\]
5. Taylor expanded around inf 0.2
  \[\leadsto \log \color{blue}{\left(\left(2 \cdot x + \frac{1}{2} \cdot \frac{{\left(\sqrt{1}\right)}^{2}}{x}\right) - \frac{1}{8} \cdot \frac{{\left(\sqrt{1}\right)}^{4}}{{x}^{3}}\right)}\]
6. Simplified0.2
  \[\leadsto \log \color{blue}{\left(\mathsf{fma}\left(x, 2, \mathsf{fma}\left(\frac{1}{x}, \frac{1}{2}, \frac{-1}{8} \cdot \frac{1 \cdot 1}{{x}^{3}}\right)\right)\right)}\]
Recombined 3 regimes into one program.
Final simplification0.3
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -1.004281043358186797931352884916123002768:\\ \;\;\;\;\log \left(\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} + \frac{0.0625}{{x}^{5}}\right)\right)\\ \mathbf{elif}\;x \le 0.8904752561288424850260980747407302260399:\\ \;\;\;\;\mathsf{fma}\left(\frac{{x}^{3}}{{\left(\sqrt{1}\right)}^{3}}, \frac{-1}{6}, \log \left(\sqrt{1}\right) + \frac{x}{\sqrt{1}}\right)\\ \mathbf{else}:\\ \;\;\;\;\log \left(\mathsf{fma}\left(x, 2, \mathsf{fma}\left(\frac{1}{x}, \frac{1}{2}, \frac{-1}{8} \cdot \frac{1 \cdot 1}{{x}^{3}}\right)\right)\right)\\ \end{array}\]

Error

Target

Derivation

`if x < -1.0042810433581868`

`if -1.0042810433581868 < x < 0.8904752561288425`

`if 0.8904752561288425 < x`

Reproduce