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

↓

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

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

↓

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

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

\mathbf{else}:\\
\;\;\;\;\log \left(\left(2 \cdot x + \frac{1}{2} \cdot \frac{1}{x}\right) - \frac{1}{8} \cdot \frac{1}{{x}^{3}}\right)\\

\end{array}

double f(double x) {
        double r129859 = x;
        double r129860 = r129859 * r129859;
        double r129861 = 1.0;
        double r129862 = r129860 + r129861;
        double r129863 = sqrt(r129862);
        double r129864 = r129859 + r129863;
        double r129865 = log(r129864);
        return r129865;
}

↓

double f(double x) {
        double r129866 = x;
        double r129867 = -1145095798178443.0;
        double r129868 = 1125899906842624.0;
        double r129869 = r129867 / r129868;
        bool r129870 = r129866 <= r129869;
        double r129871 = 1.0;
        double r129872 = 8.0;
        double r129873 = r129871 / r129872;
        double r129874 = 1.0;
        double r129875 = 3.0;
        double r129876 = pow(r129866, r129875);
        double r129877 = r129874 / r129876;
        double r129878 = r129873 * r129877;
        double r129879 = 2.0;
        double r129880 = r129871 / r129879;
        double r129881 = r129874 / r129866;
        double r129882 = r129880 * r129881;
        double r129883 = 16.0;
        double r129884 = r129871 / r129883;
        double r129885 = 5.0;
        double r129886 = pow(r129866, r129885);
        double r129887 = r129874 / r129886;
        double r129888 = r129884 * r129887;
        double r129889 = r129882 + r129888;
        double r129890 = r129878 - r129889;
        double r129891 = log(r129890);
        double r129892 = 8089726143435971.0;
        double r129893 = 9007199254740992.0;
        double r129894 = r129892 / r129893;
        bool r129895 = r129866 <= r129894;
        double r129896 = sqrt(r129871);
        double r129897 = r129866 / r129896;
        double r129898 = pow(r129896, r129875);
        double r129899 = r129876 / r129898;
        double r129900 = 6.0;
        double r129901 = r129899 / r129900;
        double r129902 = log(r129896);
        double r129903 = r129901 - r129902;
        double r129904 = r129897 - r129903;
        double r129905 = 2.0;
        double r129906 = r129905 * r129866;
        double r129907 = r129906 + r129882;
        double r129908 = r129907 - r129878;
        double r129909 = log(r129908);
        double r129910 = r129895 ? r129904 : r129909;
        double r129911 = r129870 ? r129891 : r129910;
        return r129911;
}

Original	53.3
Target	45.4
Herbie	0.3

Derivation

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

Error

Try it out

Target

Derivation

`if x < -1.017049376431383`

`if -1.017049376431383 < x < 0.8981400227354687`

`if 0.8981400227354687 < x`

Reproduce

In
Out