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

↓

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

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

\end{array}

double f(double x) {
        double r150046 = x;
        double r150047 = r150046 * r150046;
        double r150048 = 1.0;
        double r150049 = r150047 + r150048;
        double r150050 = sqrt(r150049);
        double r150051 = r150046 + r150050;
        double r150052 = log(r150051);
        return r150052;
}

↓

double f(double x) {
        double r150053 = x;
        double r150054 = -1.0118201374548368;
        bool r150055 = r150053 <= r150054;
        double r150056 = 0.125;
        double r150057 = 3.0;
        double r150058 = pow(r150053, r150057);
        double r150059 = r150056 / r150058;
        double r150060 = 0.5;
        double r150061 = r150060 / r150053;
        double r150062 = 0.0625;
        double r150063 = -r150062;
        double r150064 = 5.0;
        double r150065 = pow(r150053, r150064);
        double r150066 = r150063 / r150065;
        double r150067 = r150061 - r150066;
        double r150068 = r150059 - r150067;
        double r150069 = log(r150068);
        double r150070 = 0.00101459111765151;
        bool r150071 = r150053 <= r150070;
        double r150072 = 1.0;
        double r150073 = sqrt(r150072);
        double r150074 = log(r150073);
        double r150075 = r150053 / r150073;
        double r150076 = r150074 + r150075;
        double r150077 = 0.16666666666666666;
        double r150078 = pow(r150073, r150057);
        double r150079 = r150058 / r150078;
        double r150080 = r150077 * r150079;
        double r150081 = r150076 - r150080;
        double r150082 = 1.0;
        double r150083 = sqrt(r150082);
        double r150084 = hypot(r150053, r150073);
        double r150085 = r150083 * r150084;
        double r150086 = r150053 + r150085;
        double r150087 = sqrt(r150086);
        double r150088 = log(r150087);
        double r150089 = r150088 + r150088;
        double r150090 = r150071 ? r150081 : r150089;
        double r150091 = r150055 ? r150069 : r150090;
        return r150091;
}

Original	53.1
Target	45.4
Herbie	0.2

Derivation

Split input into 3 regimes
if x < -1.0118201374548368
1. Initial program 63.0
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around -inf 0.3
  \[\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.3
  \[\leadsto \log \color{blue}{\left(\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)\right)}\]
if -1.0118201374548368 < x < 0.00101459111765151
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.00101459111765151 < x
1. Initial program 31.8
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Using strategy rm
3. Applied *-un-lft-identity31.8
  \[\leadsto \log \left(x + \sqrt{\color{blue}{1 \cdot \left(x \cdot x + 1\right)}}\right)\]
4. Applied sqrt-prod31.8
  \[\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)\]
6. Using strategy rm
7. Applied add-sqr-sqrt0.1
  \[\leadsto \log \color{blue}{\left(\sqrt{x + \sqrt{1} \cdot \mathsf{hypot}\left(x, \sqrt{1}\right)} \cdot \sqrt{x + \sqrt{1} \cdot \mathsf{hypot}\left(x, \sqrt{1}\right)}\right)}\]
8. Applied log-prod0.1
  \[\leadsto \color{blue}{\log \left(\sqrt{x + \sqrt{1} \cdot \mathsf{hypot}\left(x, \sqrt{1}\right)}\right) + \log \left(\sqrt{x + \sqrt{1} \cdot \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.01182013745483679:\\ \;\;\;\;\log \left(\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)\right)\\ \mathbf{elif}\;x \le 0.0010145911176515101:\\ \;\;\;\;\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(\sqrt{x + \sqrt{1} \cdot \mathsf{hypot}\left(x, \sqrt{1}\right)}\right) + \log \left(\sqrt{x + \sqrt{1} \cdot \mathsf{hypot}\left(x, \sqrt{1}\right)}\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if x < -1.0118201374548368`

`if -1.0118201374548368 < x < 0.00101459111765151`

`if 0.00101459111765151 < x`

Reproduce

In
Out