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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.004655468536683526892261397733818739653:\\ \;\;\;\;\log \left(\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)\right)\\ \mathbf{elif}\;x \le 8.459866212628740049506159692782603087835 \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(1 \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(\mathsf{hypot}\left(x, \sqrt{1}\right) + x\right)\right)\right)\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;x \le -1.004655468536683526892261397733818739653:\\
\;\;\;\;\log \left(\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)\right)\\

\mathbf{elif}\;x \le 8.459866212628740049506159692782603087835 \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(1 \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(\mathsf{hypot}\left(x, \sqrt{1}\right) + x\right)\right)\right)\\

\end{array}

double f(double x) {
        double r221216 = x;
        double r221217 = r221216 * r221216;
        double r221218 = 1.0;
        double r221219 = r221217 + r221218;
        double r221220 = sqrt(r221219);
        double r221221 = r221216 + r221220;
        double r221222 = log(r221221);
        return r221222;
}

↓

double f(double x) {
        double r221223 = x;
        double r221224 = -1.0046554685366835;
        bool r221225 = r221223 <= r221224;
        double r221226 = 0.125;
        double r221227 = 3.0;
        double r221228 = pow(r221223, r221227);
        double r221229 = r221226 / r221228;
        double r221230 = 0.5;
        double r221231 = r221230 / r221223;
        double r221232 = 0.0625;
        double r221233 = -r221232;
        double r221234 = 5.0;
        double r221235 = pow(r221223, r221234);
        double r221236 = r221233 / r221235;
        double r221237 = r221231 - r221236;
        double r221238 = r221229 - r221237;
        double r221239 = log(r221238);
        double r221240 = 0.000845986621262874;
        bool r221241 = r221223 <= r221240;
        double r221242 = 1.0;
        double r221243 = sqrt(r221242);
        double r221244 = log(r221243);
        double r221245 = r221223 / r221243;
        double r221246 = r221244 + r221245;
        double r221247 = 0.16666666666666666;
        double r221248 = pow(r221243, r221227);
        double r221249 = r221228 / r221248;
        double r221250 = r221247 * r221249;
        double r221251 = r221246 - r221250;
        double r221252 = 1.0;
        double r221253 = hypot(r221223, r221243);
        double r221254 = r221253 + r221223;
        double r221255 = log1p(r221254);
        double r221256 = expm1(r221255);
        double r221257 = r221252 * r221256;
        double r221258 = log(r221257);
        double r221259 = r221241 ? r221251 : r221258;
        double r221260 = r221225 ? r221239 : r221259;
        return r221260;
}

Original	53.1
Target	45.3
Herbie	0.2

Derivation

Split input into 3 regimes
if x < -1.0046554685366835
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{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)\right)}\]
if -1.0046554685366835 < x < 0.000845986621262874
1. Initial program 58.9
  \[\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.000845986621262874 < x
1. Initial program 32.6
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Using strategy rm
3. Applied *-un-lft-identity32.6
  \[\leadsto \log \left(x + \color{blue}{1 \cdot \sqrt{x \cdot x + 1}}\right)\]
4. Applied *-un-lft-identity32.6
  \[\leadsto \log \left(\color{blue}{1 \cdot x} + 1 \cdot \sqrt{x \cdot x + 1}\right)\]
5. Applied distribute-lft-out32.6
  \[\leadsto \log \color{blue}{\left(1 \cdot \left(x + \sqrt{x \cdot x + 1}\right)\right)}\]
6. Simplified0.1
  \[\leadsto \log \left(1 \cdot \color{blue}{\left(\mathsf{hypot}\left(x, \sqrt{1}\right) + x\right)}\right)\]
7. Using strategy rm
8. Applied expm1-log1p-u0.1
  \[\leadsto \log \left(1 \cdot \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\mathsf{hypot}\left(x, \sqrt{1}\right) + x\right)\right)}\right)\]
Recombined 3 regimes into one program.
Final simplification0.2
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -1.004655468536683526892261397733818739653:\\ \;\;\;\;\log \left(\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)\right)\\ \mathbf{elif}\;x \le 8.459866212628740049506159692782603087835 \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(1 \cdot \mathsf{expm1}\left(\mathsf{log1p}\left(\mathsf{hypot}\left(x, \sqrt{1}\right) + x\right)\right)\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if x < -1.0046554685366835`

`if -1.0046554685366835 < x < 0.000845986621262874`

`if 0.000845986621262874 < x`

Reproduce

In
Out