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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.0577364498603914:\\ \;\;\;\;\log \left(\left(\frac{\frac{\frac{\frac{1}{8}}{x}}{x}}{x} + \frac{\frac{-1}{2}}{x}\right) - \frac{\frac{1}{16}}{{x}^{5}}\right)\\ \mathbf{elif}\;x \le 1.017737757509055:\\ \;\;\;\;{x}^{5} \cdot \frac{3}{40} + \left(x + x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\log 2 - \left(\frac{\frac{-1}{4}}{x \cdot x} - \left(\log x - \frac{\frac{3}{32}}{\left(x \cdot x\right) \cdot \left(x \cdot x\right)}\right)\right)\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;x \le -1.0577364498603914:\\
\;\;\;\;\log \left(\left(\frac{\frac{\frac{\frac{1}{8}}{x}}{x}}{x} + \frac{\frac{-1}{2}}{x}\right) - \frac{\frac{1}{16}}{{x}^{5}}\right)\\

\mathbf{elif}\;x \le 1.017737757509055:\\
\;\;\;\;{x}^{5} \cdot \frac{3}{40} + \left(x + x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\log 2 - \left(\frac{\frac{-1}{4}}{x \cdot x} - \left(\log x - \frac{\frac{3}{32}}{\left(x \cdot x\right) \cdot \left(x \cdot x\right)}\right)\right)\\

\end{array}

double f(double x) {
        double r20271662 = x;
        double r20271663 = r20271662 * r20271662;
        double r20271664 = 1.0;
        double r20271665 = r20271663 + r20271664;
        double r20271666 = sqrt(r20271665);
        double r20271667 = r20271662 + r20271666;
        double r20271668 = log(r20271667);
        return r20271668;
}

↓

double f(double x) {
        double r20271669 = x;
        double r20271670 = -1.0577364498603914;
        bool r20271671 = r20271669 <= r20271670;
        double r20271672 = 0.125;
        double r20271673 = r20271672 / r20271669;
        double r20271674 = r20271673 / r20271669;
        double r20271675 = r20271674 / r20271669;
        double r20271676 = -0.5;
        double r20271677 = r20271676 / r20271669;
        double r20271678 = r20271675 + r20271677;
        double r20271679 = 0.0625;
        double r20271680 = 5.0;
        double r20271681 = pow(r20271669, r20271680);
        double r20271682 = r20271679 / r20271681;
        double r20271683 = r20271678 - r20271682;
        double r20271684 = log(r20271683);
        double r20271685 = 1.017737757509055;
        bool r20271686 = r20271669 <= r20271685;
        double r20271687 = 0.075;
        double r20271688 = r20271681 * r20271687;
        double r20271689 = r20271669 * r20271669;
        double r20271690 = -0.16666666666666666;
        double r20271691 = r20271689 * r20271690;
        double r20271692 = r20271669 * r20271691;
        double r20271693 = r20271669 + r20271692;
        double r20271694 = r20271688 + r20271693;
        double r20271695 = 2.0;
        double r20271696 = log(r20271695);
        double r20271697 = -0.25;
        double r20271698 = r20271697 / r20271689;
        double r20271699 = log(r20271669);
        double r20271700 = 0.09375;
        double r20271701 = r20271689 * r20271689;
        double r20271702 = r20271700 / r20271701;
        double r20271703 = r20271699 - r20271702;
        double r20271704 = r20271698 - r20271703;
        double r20271705 = r20271696 - r20271704;
        double r20271706 = r20271686 ? r20271694 : r20271705;
        double r20271707 = r20271671 ? r20271684 : r20271706;
        return r20271707;
}

Original	52.4
Target	44.9
Herbie	0.2

Derivation

Split input into 3 regimes
if x < -1.0577364498603914
1. Initial program 61.8
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around -inf 0.2
  \[\leadsto \log \color{blue}{\left(\frac{1}{8} \cdot \frac{1}{{x}^{3}} - \left(\frac{1}{16} \cdot \frac{1}{{x}^{5}} + \frac{1}{2} \cdot \frac{1}{x}\right)\right)}\]
3. Simplified0.2
  \[\leadsto \log \color{blue}{\left(\left(\frac{\frac{-1}{2}}{x} + \frac{\frac{\frac{\frac{1}{8}}{x}}{x}}{x}\right) - \frac{\frac{1}{16}}{{x}^{5}}\right)}\]
if -1.0577364498603914 < x < 1.017737757509055
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(x + \frac{3}{40} \cdot {x}^{5}\right) - \frac{1}{6} \cdot {x}^{3}}\]
3. Simplified0.2
  \[\leadsto \color{blue}{\left(\left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right) \cdot x + x\right) + {x}^{5} \cdot \frac{3}{40}}\]
if 1.017737757509055 < x
1. Initial program 30.5
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around inf 0.4
  \[\leadsto \color{blue}{\left(\log 2 + \frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) - \left(\log \left(\frac{1}{x}\right) + \frac{3}{32} \cdot \frac{1}{{x}^{4}}\right)}\]
3. Simplified0.4
  \[\leadsto \color{blue}{\log 2 - \left(\frac{\frac{-1}{4}}{x \cdot x} - \left(\log x - \frac{\frac{3}{32}}{\left(x \cdot x\right) \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.0577364498603914:\\ \;\;\;\;\log \left(\left(\frac{\frac{\frac{\frac{1}{8}}{x}}{x}}{x} + \frac{\frac{-1}{2}}{x}\right) - \frac{\frac{1}{16}}{{x}^{5}}\right)\\ \mathbf{elif}\;x \le 1.017737757509055:\\ \;\;\;\;{x}^{5} \cdot \frac{3}{40} + \left(x + x \cdot \left(\left(x \cdot x\right) \cdot \frac{-1}{6}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\log 2 - \left(\frac{\frac{-1}{4}}{x \cdot x} - \left(\log x - \frac{\frac{3}{32}}{\left(x \cdot x\right) \cdot \left(x \cdot x\right)}\right)\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if x < -1.0577364498603914`

`if -1.0577364498603914 < x < 1.017737757509055`

`if 1.017737757509055 < x`

Reproduce

In
Out