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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.014477909773237040980120582389645278454:\\ \;\;\;\;\log \left(\frac{\frac{0.125}{x}}{x \cdot x} - \left(\frac{0.5}{x} + \frac{0.0625}{{x}^{5}}\right)\right)\\ \mathbf{elif}\;x \le 0.8909481582438814051272402139147743582726:\\ \;\;\;\;\left(\log \left(\sqrt{1}\right) + \frac{x}{\sqrt{1}}\right) + \frac{\left(x \cdot x\right) \cdot x}{1} \cdot \frac{\frac{-1}{6}}{\sqrt{1}}\\ \mathbf{else}:\\ \;\;\;\;\log \left(x + \left(\left(\frac{0.5}{x} - \frac{\frac{0.125}{x}}{x \cdot x}\right) + x\right)\right)\\ \end{array}\]

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

↓

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

\mathbf{elif}\;x \le 0.8909481582438814051272402139147743582726:\\
\;\;\;\;\left(\log \left(\sqrt{1}\right) + \frac{x}{\sqrt{1}}\right) + \frac{\left(x \cdot x\right) \cdot x}{1} \cdot \frac{\frac{-1}{6}}{\sqrt{1}}\\

\mathbf{else}:\\
\;\;\;\;\log \left(x + \left(\left(\frac{0.5}{x} - \frac{\frac{0.125}{x}}{x \cdot x}\right) + x\right)\right)\\

\end{array}

double f(double x) {
        double r6919469 = x;
        double r6919470 = r6919469 * r6919469;
        double r6919471 = 1.0;
        double r6919472 = r6919470 + r6919471;
        double r6919473 = sqrt(r6919472);
        double r6919474 = r6919469 + r6919473;
        double r6919475 = log(r6919474);
        return r6919475;
}

↓

double f(double x) {
        double r6919476 = x;
        double r6919477 = -1.014477909773237;
        bool r6919478 = r6919476 <= r6919477;
        double r6919479 = 0.125;
        double r6919480 = r6919479 / r6919476;
        double r6919481 = r6919476 * r6919476;
        double r6919482 = r6919480 / r6919481;
        double r6919483 = 0.5;
        double r6919484 = r6919483 / r6919476;
        double r6919485 = 0.0625;
        double r6919486 = 5.0;
        double r6919487 = pow(r6919476, r6919486);
        double r6919488 = r6919485 / r6919487;
        double r6919489 = r6919484 + r6919488;
        double r6919490 = r6919482 - r6919489;
        double r6919491 = log(r6919490);
        double r6919492 = 0.8909481582438814;
        bool r6919493 = r6919476 <= r6919492;
        double r6919494 = 1.0;
        double r6919495 = sqrt(r6919494);
        double r6919496 = log(r6919495);
        double r6919497 = r6919476 / r6919495;
        double r6919498 = r6919496 + r6919497;
        double r6919499 = r6919481 * r6919476;
        double r6919500 = r6919499 / r6919494;
        double r6919501 = -0.16666666666666666;
        double r6919502 = r6919501 / r6919495;
        double r6919503 = r6919500 * r6919502;
        double r6919504 = r6919498 + r6919503;
        double r6919505 = r6919484 - r6919482;
        double r6919506 = r6919505 + r6919476;
        double r6919507 = r6919476 + r6919506;
        double r6919508 = log(r6919507);
        double r6919509 = r6919493 ? r6919504 : r6919508;
        double r6919510 = r6919478 ? r6919491 : r6919509;
        return r6919510;
}

Original	52.7
Target	44.9
Herbie	0.2

Derivation

Split input into 3 regimes
if x < -1.014477909773237
1. Initial program 63.0
  \[\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{\frac{0.125}{x}}{x \cdot x} - \left(\frac{0.5}{x} + \frac{0.0625}{{x}^{5}}\right)\right)}\]
if -1.014477909773237 < x < 0.8909481582438814
1. Initial program 58.4
  \[\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}{\frac{x \cdot \left(x \cdot x\right)}{1} \cdot \frac{\frac{-1}{6}}{\sqrt{1}} + \left(\log \left(\sqrt{1}\right) + \frac{x}{\sqrt{1}}\right)}\]
if 0.8909481582438814 < x
1. Initial program 31.4
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around inf 0.1
  \[\leadsto \log \left(x + \color{blue}{\left(\left(x + 0.5 \cdot \frac{1}{x}\right) - 0.125 \cdot \frac{1}{{x}^{3}}\right)}\right)\]
3. Simplified0.1
  \[\leadsto \log \left(x + \color{blue}{\left(x + \left(\frac{0.5}{x} - \frac{\frac{0.125}{x}}{x \cdot x}\right)\right)}\right)\]
Recombined 3 regimes into one program.
Final simplification0.2
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -1.014477909773237040980120582389645278454:\\ \;\;\;\;\log \left(\frac{\frac{0.125}{x}}{x \cdot x} - \left(\frac{0.5}{x} + \frac{0.0625}{{x}^{5}}\right)\right)\\ \mathbf{elif}\;x \le 0.8909481582438814051272402139147743582726:\\ \;\;\;\;\left(\log \left(\sqrt{1}\right) + \frac{x}{\sqrt{1}}\right) + \frac{\left(x \cdot x\right) \cdot x}{1} \cdot \frac{\frac{-1}{6}}{\sqrt{1}}\\ \mathbf{else}:\\ \;\;\;\;\log \left(x + \left(\left(\frac{0.5}{x} - \frac{\frac{0.125}{x}}{x \cdot x}\right) + x\right)\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if x < -1.014477909773237`

`if -1.014477909773237 < x < 0.8909481582438814`

`if 0.8909481582438814 < x`

Reproduce

In
Out