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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -0.997323780249505298:\\ \;\;\;\;\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 0.001113141778355475:\\ \;\;\;\;\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 -0.997323780249505298:\\
\;\;\;\;\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 0.001113141778355475:\\
\;\;\;\;\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 r136199 = x;
        double r136200 = r136199 * r136199;
        double r136201 = 1.0;
        double r136202 = r136200 + r136201;
        double r136203 = sqrt(r136202);
        double r136204 = r136199 + r136203;
        double r136205 = log(r136204);
        return r136205;
}

↓

double f(double x) {
        double r136206 = x;
        double r136207 = -0.9973237802495053;
        bool r136208 = r136206 <= r136207;
        double r136209 = 0.125;
        double r136210 = 3.0;
        double r136211 = pow(r136206, r136210);
        double r136212 = r136209 / r136211;
        double r136213 = 1.0;
        double r136214 = r136213 * r136213;
        double r136215 = 0.5;
        double r136216 = -r136215;
        double r136217 = r136213 / r136206;
        double r136218 = r136216 * r136217;
        double r136219 = pow(r136213, r136210);
        double r136220 = 5.0;
        double r136221 = pow(r136206, r136220);
        double r136222 = 0.0625;
        double r136223 = r136221 / r136222;
        double r136224 = r136219 / r136223;
        double r136225 = r136218 - r136224;
        double r136226 = fma(r136212, r136214, r136225);
        double r136227 = log(r136226);
        double r136228 = 0.0011131417783554753;
        bool r136229 = r136206 <= r136228;
        double r136230 = sqrt(r136213);
        double r136231 = log(r136230);
        double r136232 = r136206 / r136230;
        double r136233 = r136231 + r136232;
        double r136234 = 0.16666666666666666;
        double r136235 = pow(r136230, r136210);
        double r136236 = r136211 / r136235;
        double r136237 = r136234 * r136236;
        double r136238 = r136233 - r136237;
        double r136239 = 1.0;
        double r136240 = sqrt(r136239);
        double r136241 = hypot(r136206, r136230);
        double r136242 = r136240 * r136241;
        double r136243 = r136206 + r136242;
        double r136244 = log(r136243);
        double r136245 = r136229 ? r136238 : r136244;
        double r136246 = r136208 ? r136227 : r136245;
        return r136246;
}

Original	52.9
Target	45.3
Herbie	0.1

Derivation

Split input into 3 regimes
if x < -0.9973237802495053
1. Initial program 63.1
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Using strategy rm
3. Applied *-un-lft-identity63.1
  \[\leadsto \log \left(x + \sqrt{\color{blue}{1 \cdot \left(x \cdot x + 1\right)}}\right)\]
4. Applied sqrt-prod63.1
  \[\leadsto \log \left(x + \color{blue}{\sqrt{1} \cdot \sqrt{x \cdot x + 1}}\right)\]
5. Simplified63.1
  \[\leadsto \log \left(x + \sqrt{1} \cdot \color{blue}{\mathsf{hypot}\left(x, \sqrt{1}\right)}\right)\]
6. 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)}\]
7. 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 -0.9973237802495053 < x < 0.0011131417783554753
1. Initial program 58.8
  \[\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.0011131417783554753 < x
1. Initial program 30.9
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Using strategy rm
3. Applied *-un-lft-identity30.9
  \[\leadsto \log \left(x + \sqrt{\color{blue}{1 \cdot \left(x \cdot x + 1\right)}}\right)\]
4. Applied sqrt-prod30.9
  \[\leadsto \log \left(x + \color{blue}{\sqrt{1} \cdot \sqrt{x \cdot x + 1}}\right)\]
5. Simplified0.1
  \[\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.1
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -0.997323780249505298:\\ \;\;\;\;\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 0.001113141778355475:\\ \;\;\;\;\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 < -0.9973237802495053`

`if -0.9973237802495053 < x < 0.0011131417783554753`

`if 0.0011131417783554753 < x`

Reproduce