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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.019834309395676097409477733890525996685:\\ \;\;\;\;\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 6.500471130900369607155675488741053413833 \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 + \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.019834309395676097409477733890525996685:\\
\;\;\;\;\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 6.500471130900369607155675488741053413833 \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 + \mathsf{hypot}\left(x, \sqrt{1}\right)\right)\\

\end{array}

double f(double x) {
        double r186035 = x;
        double r186036 = r186035 * r186035;
        double r186037 = 1.0;
        double r186038 = r186036 + r186037;
        double r186039 = sqrt(r186038);
        double r186040 = r186035 + r186039;
        double r186041 = log(r186040);
        return r186041;
}

↓

double f(double x) {
        double r186042 = x;
        double r186043 = -1.019834309395676;
        bool r186044 = r186042 <= r186043;
        double r186045 = 0.125;
        double r186046 = 3.0;
        double r186047 = pow(r186042, r186046);
        double r186048 = r186045 / r186047;
        double r186049 = 1.0;
        double r186050 = r186049 * r186049;
        double r186051 = 0.5;
        double r186052 = -r186051;
        double r186053 = r186049 / r186042;
        double r186054 = r186052 * r186053;
        double r186055 = pow(r186049, r186046);
        double r186056 = 5.0;
        double r186057 = pow(r186042, r186056);
        double r186058 = 0.0625;
        double r186059 = r186057 / r186058;
        double r186060 = r186055 / r186059;
        double r186061 = r186054 - r186060;
        double r186062 = fma(r186048, r186050, r186061);
        double r186063 = log(r186062);
        double r186064 = 0.000650047113090037;
        bool r186065 = r186042 <= r186064;
        double r186066 = sqrt(r186049);
        double r186067 = log(r186066);
        double r186068 = r186042 / r186066;
        double r186069 = r186067 + r186068;
        double r186070 = 0.16666666666666666;
        double r186071 = pow(r186066, r186046);
        double r186072 = r186047 / r186071;
        double r186073 = r186070 * r186072;
        double r186074 = r186069 - r186073;
        double r186075 = hypot(r186042, r186066);
        double r186076 = r186042 + r186075;
        double r186077 = log(r186076);
        double r186078 = r186065 ? r186074 : r186077;
        double r186079 = r186044 ? r186063 : r186078;
        return r186079;
}

Original	53.1
Target	45.5
Herbie	0.2

Derivation

Split input into 3 regimes
if x < -1.019834309395676
1. Initial program 63.0
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Using strategy rm
3. Applied add-sqr-sqrt63.0
  \[\leadsto \log \left(x + \sqrt{x \cdot x + \color{blue}{\sqrt{1} \cdot \sqrt{1}}}\right)\]
4. Applied hypot-def63.0
  \[\leadsto \log \left(x + \color{blue}{\mathsf{hypot}\left(x, \sqrt{1}\right)}\right)\]
5. Taylor expanded around -inf 0.1
  \[\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)}\]
6. Simplified0.1
  \[\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.019834309395676 < x < 0.000650047113090037
1. Initial program 59.1
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around 0 0.2
  \[\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.000650047113090037 < x
1. Initial program 31.7
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Using strategy rm
3. Applied add-sqr-sqrt31.7
  \[\leadsto \log \left(x + \sqrt{x \cdot x + \color{blue}{\sqrt{1} \cdot \sqrt{1}}}\right)\]
4. Applied hypot-def0.2
  \[\leadsto \log \left(x + \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.019834309395676097409477733890525996685:\\ \;\;\;\;\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 6.500471130900369607155675488741053413833 \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 + \mathsf{hypot}\left(x, \sqrt{1}\right)\right)\\ \end{array}\]

Error

Target

Derivation

`if x < -1.019834309395676`

`if -1.019834309395676 < x < 0.000650047113090037`

`if 0.000650047113090037 < x`

Reproduce