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

↓

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

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

↓

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

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

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

\end{array}

double f(double x) {
        double r6965366 = x;
        double r6965367 = r6965366 * r6965366;
        double r6965368 = 1.0;
        double r6965369 = r6965367 + r6965368;
        double r6965370 = sqrt(r6965369);
        double r6965371 = r6965366 + r6965370;
        double r6965372 = log(r6965371);
        return r6965372;
}

↓

double f(double x) {
        double r6965373 = x;
        double r6965374 = -1.0196402015835608;
        bool r6965375 = r6965373 <= r6965374;
        double r6965376 = 0.125;
        double r6965377 = r6965373 * r6965373;
        double r6965378 = r6965377 * r6965373;
        double r6965379 = r6965376 / r6965378;
        double r6965380 = 0.0625;
        double r6965381 = 5.0;
        double r6965382 = pow(r6965373, r6965381);
        double r6965383 = r6965380 / r6965382;
        double r6965384 = 0.5;
        double r6965385 = r6965384 / r6965373;
        double r6965386 = r6965383 + r6965385;
        double r6965387 = r6965379 - r6965386;
        double r6965388 = log(r6965387);
        double r6965389 = 0.9010700472866574;
        bool r6965390 = r6965373 <= r6965389;
        double r6965391 = 1.0;
        double r6965392 = sqrt(r6965391);
        double r6965393 = log(r6965392);
        double r6965394 = r6965373 / r6965392;
        double r6965395 = r6965393 + r6965394;
        double r6965396 = 0.16666666666666666;
        double r6965397 = r6965396 / r6965391;
        double r6965398 = r6965378 / r6965392;
        double r6965399 = r6965397 * r6965398;
        double r6965400 = r6965395 - r6965399;
        double r6965401 = r6965373 + r6965385;
        double r6965402 = r6965401 - r6965379;
        double r6965403 = r6965402 + r6965373;
        double r6965404 = log(r6965403);
        double r6965405 = r6965390 ? r6965400 : r6965404;
        double r6965406 = r6965375 ? r6965388 : r6965405;
        return r6965406;
}

Original	53.1
Target	45.5
Herbie	0.2

Derivation

Split input into 3 regimes
if x < -1.0196402015835608
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.0625 \cdot \frac{1}{{x}^{5}} + 0.5 \cdot \frac{1}{x}\right)\right)}\]
3. Simplified0.2
  \[\leadsto \log \color{blue}{\left(\frac{0.125}{x \cdot \left(x \cdot x\right)} - \left(\frac{0.5}{x} + \frac{0.0625}{{x}^{5}}\right)\right)}\]
if -1.0196402015835608 < x < 0.9010700472866574
1. Initial program 58.6
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around 0 0.2
  \[\leadsto \color{blue}{\left(\frac{x}{\sqrt{1}} + \log \left(\sqrt{1}\right)\right) - \frac{1}{6} \cdot \frac{{x}^{3}}{{\left(\sqrt{1}\right)}^{3}}}\]
3. Simplified0.2
  \[\leadsto \color{blue}{\left(\log \left(\sqrt{1}\right) + \frac{x}{\sqrt{1}}\right) - \frac{x \cdot \left(x \cdot x\right)}{\sqrt{1}} \cdot \frac{\frac{1}{6}}{1}}\]
if 0.9010700472866574 < x
1. Initial program 32.0
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around inf 0.2
  \[\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.2
  \[\leadsto \log \left(x + \color{blue}{\left(\left(x + \frac{0.5}{x}\right) - \frac{0.125}{x \cdot \left(x \cdot x\right)}\right)}\right)\]
Recombined 3 regimes into one program.
Final simplification0.2
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -1.019640201583560834563968455768190324306:\\ \;\;\;\;\log \left(\frac{0.125}{\left(x \cdot x\right) \cdot x} - \left(\frac{0.0625}{{x}^{5}} + \frac{0.5}{x}\right)\right)\\ \mathbf{elif}\;x \le 0.9010700472866574051167276593332644551992:\\ \;\;\;\;\left(\log \left(\sqrt{1}\right) + \frac{x}{\sqrt{1}}\right) - \frac{\frac{1}{6}}{1} \cdot \frac{\left(x \cdot x\right) \cdot x}{\sqrt{1}}\\ \mathbf{else}:\\ \;\;\;\;\log \left(\left(\left(x + \frac{0.5}{x}\right) - \frac{0.125}{\left(x \cdot x\right) \cdot x}\right) + x\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if x < -1.0196402015835608`

`if -1.0196402015835608 < x < 0.9010700472866574`

`if 0.9010700472866574 < x`

Reproduce

In
Out