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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.024334867874778:\\ \;\;\;\;\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.0010473279622313881:\\ \;\;\;\;\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.024334867874778:\\
\;\;\;\;\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.0010473279622313881:\\
\;\;\;\;\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 r166039 = x;
        double r166040 = r166039 * r166039;
        double r166041 = 1.0;
        double r166042 = r166040 + r166041;
        double r166043 = sqrt(r166042);
        double r166044 = r166039 + r166043;
        double r166045 = log(r166044);
        return r166045;
}

↓

double f(double x) {
        double r166046 = x;
        double r166047 = -1.024334867874778;
        bool r166048 = r166046 <= r166047;
        double r166049 = 0.125;
        double r166050 = 3.0;
        double r166051 = pow(r166046, r166050);
        double r166052 = r166049 / r166051;
        double r166053 = 1.0;
        double r166054 = r166053 * r166053;
        double r166055 = 0.5;
        double r166056 = -r166055;
        double r166057 = r166053 / r166046;
        double r166058 = r166056 * r166057;
        double r166059 = pow(r166053, r166050);
        double r166060 = 5.0;
        double r166061 = pow(r166046, r166060);
        double r166062 = 0.0625;
        double r166063 = r166061 / r166062;
        double r166064 = r166059 / r166063;
        double r166065 = r166058 - r166064;
        double r166066 = fma(r166052, r166054, r166065);
        double r166067 = log(r166066);
        double r166068 = 0.0010473279622313881;
        bool r166069 = r166046 <= r166068;
        double r166070 = sqrt(r166053);
        double r166071 = log(r166070);
        double r166072 = r166046 / r166070;
        double r166073 = r166071 + r166072;
        double r166074 = 0.16666666666666666;
        double r166075 = pow(r166070, r166050);
        double r166076 = r166051 / r166075;
        double r166077 = r166074 * r166076;
        double r166078 = r166073 - r166077;
        double r166079 = 1.0;
        double r166080 = sqrt(r166079);
        double r166081 = hypot(r166046, r166070);
        double r166082 = r166080 * r166081;
        double r166083 = r166046 + r166082;
        double r166084 = log(r166083);
        double r166085 = r166069 ? r166078 : r166084;
        double r166086 = r166048 ? r166067 : r166085;
        return r166086;
}

Original	53.6
Target	45.7
Herbie	0.1

Derivation

Split input into 3 regimes
if x < -1.024334867874778
1. Initial program 63.0
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Using strategy rm
3. Applied *-un-lft-identity63.0
  \[\leadsto \log \left(x + \sqrt{\color{blue}{1 \cdot \left(x \cdot x + 1\right)}}\right)\]
4. Applied sqrt-prod63.0
  \[\leadsto \log \left(x + \color{blue}{\sqrt{1} \cdot \sqrt{x \cdot x + 1}}\right)\]
5. Simplified62.9
  \[\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 -1.024334867874778 < x < 0.0010473279622313881
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.0010473279622313881 < x
1. Initial program 32.9
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Using strategy rm
3. Applied *-un-lft-identity32.9
  \[\leadsto \log \left(x + \sqrt{\color{blue}{1 \cdot \left(x \cdot x + 1\right)}}\right)\]
4. Applied sqrt-prod32.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 -1.024334867874778:\\ \;\;\;\;\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.0010473279622313881:\\ \;\;\;\;\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.024334867874778`

`if -1.024334867874778 < x < 0.0010473279622313881`

`if 0.0010473279622313881 < x`

Reproduce