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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.0577364498603914:\\ \;\;\;\;\log \left(\frac{\frac{\frac{1}{8}}{x}}{x \cdot x} - \left(\frac{\frac{1}{2}}{x} + \frac{\frac{1}{16}}{{x}^{5}}\right)\right)\\ \mathbf{elif}\;x \le 1.017737757509055:\\ \;\;\;\;\mathsf{fma}\left(\left(x \cdot \frac{-1}{6}\right), \left(x \cdot x\right), \left(\mathsf{fma}\left(\frac{3}{40}, \left({x}^{5}\right), x\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\log x + \left(\left(\frac{\frac{1}{4}}{x \cdot x} + \log 2\right) + \frac{\frac{-3}{32}}{\left(x \cdot x\right) \cdot \left(x \cdot x\right)}\right)\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;x \le -1.0577364498603914:\\
\;\;\;\;\log \left(\frac{\frac{\frac{1}{8}}{x}}{x \cdot x} - \left(\frac{\frac{1}{2}}{x} + \frac{\frac{1}{16}}{{x}^{5}}\right)\right)\\

\mathbf{elif}\;x \le 1.017737757509055:\\
\;\;\;\;\mathsf{fma}\left(\left(x \cdot \frac{-1}{6}\right), \left(x \cdot x\right), \left(\mathsf{fma}\left(\frac{3}{40}, \left({x}^{5}\right), x\right)\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\log x + \left(\left(\frac{\frac{1}{4}}{x \cdot x} + \log 2\right) + \frac{\frac{-3}{32}}{\left(x \cdot x\right) \cdot \left(x \cdot x\right)}\right)\\

\end{array}

double f(double x) {
        double r23525186 = x;
        double r23525187 = r23525186 * r23525186;
        double r23525188 = 1.0;
        double r23525189 = r23525187 + r23525188;
        double r23525190 = sqrt(r23525189);
        double r23525191 = r23525186 + r23525190;
        double r23525192 = log(r23525191);
        return r23525192;
}

↓

double f(double x) {
        double r23525193 = x;
        double r23525194 = -1.0577364498603914;
        bool r23525195 = r23525193 <= r23525194;
        double r23525196 = 0.125;
        double r23525197 = r23525196 / r23525193;
        double r23525198 = r23525193 * r23525193;
        double r23525199 = r23525197 / r23525198;
        double r23525200 = 0.5;
        double r23525201 = r23525200 / r23525193;
        double r23525202 = 0.0625;
        double r23525203 = 5.0;
        double r23525204 = pow(r23525193, r23525203);
        double r23525205 = r23525202 / r23525204;
        double r23525206 = r23525201 + r23525205;
        double r23525207 = r23525199 - r23525206;
        double r23525208 = log(r23525207);
        double r23525209 = 1.017737757509055;
        bool r23525210 = r23525193 <= r23525209;
        double r23525211 = -0.16666666666666666;
        double r23525212 = r23525193 * r23525211;
        double r23525213 = 0.075;
        double r23525214 = fma(r23525213, r23525204, r23525193);
        double r23525215 = fma(r23525212, r23525198, r23525214);
        double r23525216 = log(r23525193);
        double r23525217 = 0.25;
        double r23525218 = r23525217 / r23525198;
        double r23525219 = 2.0;
        double r23525220 = log(r23525219);
        double r23525221 = r23525218 + r23525220;
        double r23525222 = -0.09375;
        double r23525223 = r23525198 * r23525198;
        double r23525224 = r23525222 / r23525223;
        double r23525225 = r23525221 + r23525224;
        double r23525226 = r23525216 + r23525225;
        double r23525227 = r23525210 ? r23525215 : r23525226;
        double r23525228 = r23525195 ? r23525208 : r23525227;
        return r23525228;
}

Original	52.4
Target	44.9
Herbie	0.2

Derivation

Split input into 3 regimes
if x < -1.0577364498603914
1. Initial program 61.8
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Simplified61.0
  \[\leadsto \color{blue}{\log \left(x + \mathsf{hypot}\left(1, x\right)\right)}\]
3. Taylor expanded around -inf 0.2
  \[\leadsto \log \color{blue}{\left(\frac{1}{8} \cdot \frac{1}{{x}^{3}} - \left(\frac{1}{16} \cdot \frac{1}{{x}^{5}} + \frac{1}{2} \cdot \frac{1}{x}\right)\right)}\]
4. Simplified0.2
  \[\leadsto \log \color{blue}{\left(\frac{\frac{\frac{1}{8}}{x}}{x \cdot x} - \left(\frac{\frac{1}{16}}{{x}^{5}} + \frac{\frac{1}{2}}{x}\right)\right)}\]
if -1.0577364498603914 < x < 1.017737757509055
1. Initial program 58.6
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Simplified58.6
  \[\leadsto \color{blue}{\log \left(x + \mathsf{hypot}\left(1, x\right)\right)}\]
3. Taylor expanded around 0 0.2
  \[\leadsto \color{blue}{\left(x + \frac{3}{40} \cdot {x}^{5}\right) - \frac{1}{6} \cdot {x}^{3}}\]
4. Simplified0.2
  \[\leadsto \color{blue}{\mathsf{fma}\left(\left(x \cdot \frac{-1}{6}\right), \left(x \cdot x\right), \left(\mathsf{fma}\left(\frac{3}{40}, \left({x}^{5}\right), x\right)\right)\right)}\]
if 1.017737757509055 < x
1. Initial program 30.5
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Simplified0.2
  \[\leadsto \color{blue}{\log \left(x + \mathsf{hypot}\left(1, x\right)\right)}\]
3. Taylor expanded around inf 0.4
  \[\leadsto \color{blue}{\left(\log 2 + \frac{1}{4} \cdot \frac{1}{{x}^{2}}\right) - \left(\log \left(\frac{1}{x}\right) + \frac{3}{32} \cdot \frac{1}{{x}^{4}}\right)}\]
4. Simplified0.4
  \[\leadsto \color{blue}{\left(\left(\frac{\frac{1}{4}}{x \cdot x} + \log 2\right) + \frac{\frac{-3}{32}}{\left(x \cdot x\right) \cdot \left(x \cdot x\right)}\right) + \log x}\]
Recombined 3 regimes into one program.
Final simplification0.2
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -1.0577364498603914:\\ \;\;\;\;\log \left(\frac{\frac{\frac{1}{8}}{x}}{x \cdot x} - \left(\frac{\frac{1}{2}}{x} + \frac{\frac{1}{16}}{{x}^{5}}\right)\right)\\ \mathbf{elif}\;x \le 1.017737757509055:\\ \;\;\;\;\mathsf{fma}\left(\left(x \cdot \frac{-1}{6}\right), \left(x \cdot x\right), \left(\mathsf{fma}\left(\frac{3}{40}, \left({x}^{5}\right), x\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\log x + \left(\left(\frac{\frac{1}{4}}{x \cdot x} + \log 2\right) + \frac{\frac{-3}{32}}{\left(x \cdot x\right) \cdot \left(x \cdot x\right)}\right)\\ \end{array}\]

Error

Target

Derivation

`if x < -1.0577364498603914`

`if -1.0577364498603914 < x < 1.017737757509055`

`if 1.017737757509055 < x`

Reproduce