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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.03811431304857993:\\ \;\;\;\;\log \left(\mathsf{fma}\left(\frac{\frac{1}{8}}{{x}^{3}}, 1 \cdot 1, \left(-\frac{1}{2}\right) \cdot \frac{1}{x} - \frac{{1}^{3}}{\frac{{x}^{5}}{\frac{1}{16}}}\right)\right)\\ \mathbf{elif}\;x \le 9.19903403515578391 \cdot 10^{-4}:\\ \;\;\;\;\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 \left(x + \sqrt{1} \cdot \mathsf{hypot}\left(x, \sqrt{1}\right)\right)\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;x \le -1.03811431304857993:\\
\;\;\;\;\log \left(\mathsf{fma}\left(\frac{\frac{1}{8}}{{x}^{3}}, 1 \cdot 1, \left(-\frac{1}{2}\right) \cdot \frac{1}{x} - \frac{{1}^{3}}{\frac{{x}^{5}}{\frac{1}{16}}}\right)\right)\\

\mathbf{elif}\;x \le 9.19903403515578391 \cdot 10^{-4}:\\
\;\;\;\;\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 \left(x + \sqrt{1} \cdot \mathsf{hypot}\left(x, \sqrt{1}\right)\right)\\

\end{array}

double f(double x) {
        double r170940 = x;
        double r170941 = r170940 * r170940;
        double r170942 = 1.0;
        double r170943 = r170941 + r170942;
        double r170944 = sqrt(r170943);
        double r170945 = r170940 + r170944;
        double r170946 = log(r170945);
        return r170946;
}

↓

double f(double x) {
        double r170947 = x;
        double r170948 = -1.03811431304858;
        bool r170949 = r170947 <= r170948;
        double r170950 = 0.125;
        double r170951 = 3.0;
        double r170952 = pow(r170947, r170951);
        double r170953 = r170950 / r170952;
        double r170954 = 1.0;
        double r170955 = r170954 * r170954;
        double r170956 = 0.5;
        double r170957 = -r170956;
        double r170958 = r170954 / r170947;
        double r170959 = r170957 * r170958;
        double r170960 = pow(r170954, r170951);
        double r170961 = 5.0;
        double r170962 = pow(r170947, r170961);
        double r170963 = 0.0625;
        double r170964 = r170962 / r170963;
        double r170965 = r170960 / r170964;
        double r170966 = r170959 - r170965;
        double r170967 = fma(r170953, r170955, r170966);
        double r170968 = log(r170967);
        double r170969 = 0.0009199034035155784;
        bool r170970 = r170947 <= r170969;
        double r170971 = sqrt(r170954);
        double r170972 = log(r170971);
        double r170973 = r170947 / r170971;
        double r170974 = r170972 + r170973;
        double r170975 = 0.16666666666666666;
        double r170976 = pow(r170971, r170951);
        double r170977 = r170952 / r170976;
        double r170978 = r170975 * r170977;
        double r170979 = r170974 - r170978;
        double r170980 = 1.0;
        double r170981 = sqrt(r170980);
        double r170982 = hypot(r170947, r170971);
        double r170983 = r170981 * r170982;
        double r170984 = r170947 + r170983;
        double r170985 = log(r170984);
        double r170986 = r170970 ? r170979 : r170985;
        double r170987 = r170949 ? r170968 : r170986;
        return r170987;
}

Original	53.0
Target	45.4
Herbie	0.2

Derivation

Split input into 3 regimes
if x < -1.03811431304858
1. Initial program 62.7
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Using strategy rm
3. Applied *-un-lft-identity62.7
  \[\leadsto \log \left(x + \sqrt{\color{blue}{1 \cdot \left(x \cdot x + 1\right)}}\right)\]
4. Applied sqrt-prod62.7
  \[\leadsto \log \left(x + \color{blue}{\sqrt{1} \cdot \sqrt{x \cdot x + 1}}\right)\]
5. Simplified62.7
  \[\leadsto \log \left(x + \sqrt{1} \cdot \color{blue}{\mathsf{hypot}\left(x, \sqrt{1}\right)}\right)\]
6. Taylor expanded around -inf 0.3
  \[\leadsto \log \color{blue}{\left(\frac{1}{8} \cdot \frac{{\left(\sqrt{1}\right)}^{4}}{{x}^{3}} - \left(\frac{1}{16} \cdot \frac{{\left(\sqrt{1}\right)}^{6}}{{x}^{5}} + \frac{1}{2} \cdot \frac{{\left(\sqrt{1}\right)}^{2}}{x}\right)\right)}\]
7. Simplified0.3
  \[\leadsto \log \color{blue}{\left(\mathsf{fma}\left(\frac{\frac{1}{8}}{{x}^{3}}, 1 \cdot 1, \left(-\frac{1}{2}\right) \cdot \frac{1}{x} - \frac{{1}^{3}}{\frac{{x}^{5}}{\frac{1}{16}}}\right)\right)}\]
if -1.03811431304858 < x < 0.0009199034035155784
1. Initial program 59.0
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around 0 0.1
  \[\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.0009199034035155784 < x
1. Initial program 32.3
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Using strategy rm
3. Applied *-un-lft-identity32.3
  \[\leadsto \log \left(x + \sqrt{\color{blue}{1 \cdot \left(x \cdot x + 1\right)}}\right)\]
4. Applied sqrt-prod32.3
  \[\leadsto \log \left(x + \color{blue}{\sqrt{1} \cdot \sqrt{x \cdot x + 1}}\right)\]
5. Simplified0.0
  \[\leadsto \log \left(x + \sqrt{1} \cdot \color{blue}{\mathsf{hypot}\left(x, \sqrt{1}\right)}\right)\]
Recombined 3 regimes into one program.
Final simplification0.2
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -1.03811431304857993:\\ \;\;\;\;\log \left(\mathsf{fma}\left(\frac{\frac{1}{8}}{{x}^{3}}, 1 \cdot 1, \left(-\frac{1}{2}\right) \cdot \frac{1}{x} - \frac{{1}^{3}}{\frac{{x}^{5}}{\frac{1}{16}}}\right)\right)\\ \mathbf{elif}\;x \le 9.19903403515578391 \cdot 10^{-4}:\\ \;\;\;\;\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 \left(x + \sqrt{1} \cdot \mathsf{hypot}\left(x, \sqrt{1}\right)\right)\\ \end{array}\]

Error

Target

Derivation

`if x < -1.03811431304858`

`if -1.03811431304858 < x < 0.0009199034035155784`

`if 0.0009199034035155784 < x`

Reproduce