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

↓

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

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

↓

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

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

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

\end{array}

double f(double x) {
        double r142814 = x;
        double r142815 = r142814 * r142814;
        double r142816 = 1.0;
        double r142817 = r142815 + r142816;
        double r142818 = sqrt(r142817);
        double r142819 = r142814 + r142818;
        double r142820 = log(r142819);
        return r142820;
}

↓

double f(double x) {
        double r142821 = x;
        double r142822 = -2247806780098569.0;
        double r142823 = 2251799813685248.0;
        double r142824 = r142822 / r142823;
        bool r142825 = r142821 <= r142824;
        double r142826 = 1.0;
        double r142827 = 8.0;
        double r142828 = r142826 / r142827;
        double r142829 = 3.0;
        double r142830 = pow(r142821, r142829);
        double r142831 = r142828 / r142830;
        double r142832 = 2.0;
        double r142833 = r142826 / r142832;
        double r142834 = r142833 / r142821;
        double r142835 = 16.0;
        double r142836 = r142826 / r142835;
        double r142837 = -r142836;
        double r142838 = 5.0;
        double r142839 = pow(r142821, r142838);
        double r142840 = r142837 / r142839;
        double r142841 = r142834 - r142840;
        double r142842 = r142831 - r142841;
        double r142843 = log(r142842);
        double r142844 = 8537948473492591.0;
        double r142845 = 9007199254740992.0;
        double r142846 = r142844 / r142845;
        bool r142847 = r142821 <= r142846;
        double r142848 = sqrt(r142826);
        double r142849 = log(r142848);
        double r142850 = r142821 / r142848;
        double r142851 = r142849 + r142850;
        double r142852 = 0.16666666666666666;
        double r142853 = pow(r142848, r142829);
        double r142854 = r142830 / r142853;
        double r142855 = r142852 * r142854;
        double r142856 = r142851 - r142855;
        double r142857 = 2.0;
        double r142858 = log(r142857);
        double r142859 = 3.0;
        double r142860 = 32.0;
        double r142861 = r142859 / r142860;
        double r142862 = 4.0;
        double r142863 = pow(r142821, r142862);
        double r142864 = r142861 / r142863;
        double r142865 = log(r142821);
        double r142866 = r142864 - r142865;
        double r142867 = 4.0;
        double r142868 = r142826 / r142867;
        double r142869 = r142868 / r142821;
        double r142870 = r142869 / r142821;
        double r142871 = r142866 - r142870;
        double r142872 = r142858 - r142871;
        double r142873 = r142847 ? r142856 : r142872;
        double r142874 = r142825 ? r142843 : r142873;
        return r142874;
}

Original	53.0
Target	45.4
Herbie	0.3

Derivation

Split input into 3 regimes
if x < -0.998226736869587
1. Initial program 62.6
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around -inf 0.3
  \[\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.3
  \[\leadsto \log \color{blue}{\left(\frac{\frac{1}{8}}{{x}^{3}} - \left(\frac{\frac{1}{2}}{x} - \frac{-\frac{1}{16}}{{x}^{5}}\right)\right)}\]
if -0.998226736869587 < x < 0.9479026978334683
1. Initial program 58.7
  \[\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}}}\]
if 0.9479026978334683 < x
1. Initial program 31.9
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around inf 0.3
  \[\leadsto \color{blue}{\left(0.25 \cdot \frac{1}{{x}^{2}} + \log 2\right) - \left(\log \left(\frac{1}{x}\right) + 0.09375 \cdot \frac{1}{{x}^{4}}\right)}\]
3. Simplified0.3
  \[\leadsto \color{blue}{\log 2 - \left(\left(\frac{\frac{3}{32}}{{x}^{4}} - \log x\right) - \frac{\frac{\frac{1}{4}}{x}}{x}\right)}\]
Recombined 3 regimes into one program.
Final simplification0.3
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le \frac{-2247806780098569}{2251799813685248}:\\ \;\;\;\;\log \left(\frac{\frac{1}{8}}{{x}^{3}} - \left(\frac{\frac{1}{2}}{x} - \frac{-\frac{1}{16}}{{x}^{5}}\right)\right)\\ \mathbf{elif}\;x \le \frac{8537948473492591}{9007199254740992}:\\ \;\;\;\;\left(\log \left(\sqrt{1}\right) + \frac{x}{\sqrt{1}}\right) - \frac{1}{6} \cdot \frac{{x}^{3}}{{\left(\sqrt{1}\right)}^{3}}\\ \mathbf{else}:\\ \;\;\;\;\log 2 - \left(\left(\frac{\frac{3}{32}}{{x}^{4}} - \log x\right) - \frac{\frac{\frac{1}{4}}{x}}{x}\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if x < -0.998226736869587`

`if -0.998226736869587 < x < 0.9479026978334683`

`if 0.9479026978334683 < x`

Reproduce

In
Out