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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.009816372300169629028232520795427262783:\\ \;\;\;\;\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.8987700841367661785952236641605850309134:\\ \;\;\;\;\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.009816372300169629028232520795427262783:\\
\;\;\;\;\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.8987700841367661785952236641605850309134:\\
\;\;\;\;\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 r7640518 = x;
        double r7640519 = r7640518 * r7640518;
        double r7640520 = 1.0;
        double r7640521 = r7640519 + r7640520;
        double r7640522 = sqrt(r7640521);
        double r7640523 = r7640518 + r7640522;
        double r7640524 = log(r7640523);
        return r7640524;
}

↓

double f(double x) {
        double r7640525 = x;
        double r7640526 = -1.0098163723001696;
        bool r7640527 = r7640525 <= r7640526;
        double r7640528 = 0.125;
        double r7640529 = r7640525 * r7640525;
        double r7640530 = r7640529 * r7640525;
        double r7640531 = r7640528 / r7640530;
        double r7640532 = 0.0625;
        double r7640533 = 5.0;
        double r7640534 = pow(r7640525, r7640533);
        double r7640535 = r7640532 / r7640534;
        double r7640536 = 0.5;
        double r7640537 = r7640536 / r7640525;
        double r7640538 = r7640535 + r7640537;
        double r7640539 = r7640531 - r7640538;
        double r7640540 = log(r7640539);
        double r7640541 = 0.8987700841367662;
        bool r7640542 = r7640525 <= r7640541;
        double r7640543 = 1.0;
        double r7640544 = sqrt(r7640543);
        double r7640545 = log(r7640544);
        double r7640546 = r7640525 / r7640544;
        double r7640547 = r7640545 + r7640546;
        double r7640548 = 0.16666666666666666;
        double r7640549 = r7640548 / r7640543;
        double r7640550 = r7640530 / r7640544;
        double r7640551 = r7640549 * r7640550;
        double r7640552 = r7640547 - r7640551;
        double r7640553 = r7640525 + r7640537;
        double r7640554 = r7640553 - r7640531;
        double r7640555 = r7640554 + r7640525;
        double r7640556 = log(r7640555);
        double r7640557 = r7640542 ? r7640552 : r7640556;
        double r7640558 = r7640527 ? r7640540 : r7640557;
        return r7640558;
}

Original	53.3
Target	45.5
Herbie	0.2

Derivation

Split input into 3 regimes
if x < -1.0098163723001696
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.0098163723001696 < x < 0.8987700841367662
1. Initial program 58.8
  \[\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.8987700841367662 < x
1. Initial program 32.7
  \[\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.009816372300169629028232520795427262783:\\ \;\;\;\;\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.8987700841367661785952236641605850309134:\\ \;\;\;\;\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.0098163723001696`

`if -1.0098163723001696 < x < 0.8987700841367662`

`if 0.8987700841367662 < x`

Reproduce

In
Out