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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.0563392067882509:\\ \;\;\;\;\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 0.007387095680401754:\\ \;\;\;\;(\left(x \cdot \frac{-1}{6}\right) \cdot \left(x \cdot x\right) + \left((\frac{3}{40} \cdot \left({x}^{5}\right) + x)_*\right))_*\\ \mathbf{else}:\\ \;\;\;\;\log \left(\sqrt{1^2 + x^2}^* + x\right)\\ \end{array}\]

double f(double x) {
        double r21910041 = x;
        double r21910042 = r21910041 * r21910041;
        double r21910043 = 1.0;
        double r21910044 = r21910042 + r21910043;
        double r21910045 = sqrt(r21910044);
        double r21910046 = r21910041 + r21910045;
        double r21910047 = log(r21910046);
        return r21910047;
}

↓

double f(double x) {
        double r21910048 = x;
        double r21910049 = -1.0563392067882509;
        bool r21910050 = r21910048 <= r21910049;
        double r21910051 = 0.125;
        double r21910052 = r21910051 / r21910048;
        double r21910053 = r21910048 * r21910048;
        double r21910054 = r21910052 / r21910053;
        double r21910055 = 0.5;
        double r21910056 = r21910055 / r21910048;
        double r21910057 = 0.0625;
        double r21910058 = 5.0;
        double r21910059 = pow(r21910048, r21910058);
        double r21910060 = r21910057 / r21910059;
        double r21910061 = r21910056 + r21910060;
        double r21910062 = r21910054 - r21910061;
        double r21910063 = log(r21910062);
        double r21910064 = 0.007387095680401754;
        bool r21910065 = r21910048 <= r21910064;
        double r21910066 = -0.16666666666666666;
        double r21910067 = r21910048 * r21910066;
        double r21910068 = 0.075;
        double r21910069 = fma(r21910068, r21910059, r21910048);
        double r21910070 = fma(r21910067, r21910053, r21910069);
        double r21910071 = 1.0;
        double r21910072 = hypot(r21910071, r21910048);
        double r21910073 = r21910072 + r21910048;
        double r21910074 = log(r21910073);
        double r21910075 = r21910065 ? r21910070 : r21910074;
        double r21910076 = r21910050 ? r21910063 : r21910075;
        return r21910076;
}

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

↓

\begin{array}{l}
\mathbf{if}\;x \le -1.0563392067882509:\\
\;\;\;\;\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 0.007387095680401754:\\
\;\;\;\;(\left(x \cdot \frac{-1}{6}\right) \cdot \left(x \cdot x\right) + \left((\frac{3}{40} \cdot \left({x}^{5}\right) + x)_*\right))_*\\

\mathbf{else}:\\
\;\;\;\;\log \left(\sqrt{1^2 + x^2}^* + x\right)\\

\end{array}

Original	52.5
Target	44.6
Herbie	0.1

Derivation

Split input into 3 regimes
if x < -1.0563392067882509
1. Initial program 62.0
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Simplified61.2
  \[\leadsto \color{blue}{\log \left(x + \sqrt{1^2 + x^2}^*\right)}\]
3. Using strategy rm
4. Applied add-cube-cbrt61.2
  \[\leadsto \log \color{blue}{\left(\left(\sqrt[3]{x + \sqrt{1^2 + x^2}^*} \cdot \sqrt[3]{x + \sqrt{1^2 + x^2}^*}\right) \cdot \sqrt[3]{x + \sqrt{1^2 + x^2}^*}\right)}\]
5. Using strategy rm
6. Applied add-exp-log61.2
  \[\leadsto \log \color{blue}{\left(e^{\log \left(\left(\sqrt[3]{x + \sqrt{1^2 + x^2}^*} \cdot \sqrt[3]{x + \sqrt{1^2 + x^2}^*}\right) \cdot \sqrt[3]{x + \sqrt{1^2 + x^2}^*}\right)}\right)}\]
7. Applied rem-log-exp61.2
  \[\leadsto \color{blue}{\log \left(\left(\sqrt[3]{x + \sqrt{1^2 + x^2}^*} \cdot \sqrt[3]{x + \sqrt{1^2 + x^2}^*}\right) \cdot \sqrt[3]{x + \sqrt{1^2 + x^2}^*}\right)}\]
8. Simplified61.2
  \[\leadsto \log \color{blue}{\left(x + \sqrt{1^2 + x^2}^*\right)}\]
9. 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)}\]
10. 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.0563392067882509 < x < 0.007387095680401754
1. Initial program 58.8
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Simplified58.8
  \[\leadsto \color{blue}{\log \left(x + \sqrt{1^2 + x^2}^*\right)}\]
3. Taylor expanded around 0 0.1
  \[\leadsto \color{blue}{\left(x + \frac{3}{40} \cdot {x}^{5}\right) - \frac{1}{6} \cdot {x}^{3}}\]
4. Simplified0.1
  \[\leadsto \color{blue}{(\left(x \cdot \frac{-1}{6}\right) \cdot \left(x \cdot x\right) + \left((\frac{3}{40} \cdot \left({x}^{5}\right) + x)_*\right))_*}\]
if 0.007387095680401754 < x
1. Initial program 30.8
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Simplified0.0
  \[\leadsto \color{blue}{\log \left(x + \sqrt{1^2 + x^2}^*\right)}\]
3. Using strategy rm
4. Applied add-cube-cbrt0.0
  \[\leadsto \log \color{blue}{\left(\left(\sqrt[3]{x + \sqrt{1^2 + x^2}^*} \cdot \sqrt[3]{x + \sqrt{1^2 + x^2}^*}\right) \cdot \sqrt[3]{x + \sqrt{1^2 + x^2}^*}\right)}\]
5. Using strategy rm
6. Applied add-exp-log0.0
  \[\leadsto \log \color{blue}{\left(e^{\log \left(\left(\sqrt[3]{x + \sqrt{1^2 + x^2}^*} \cdot \sqrt[3]{x + \sqrt{1^2 + x^2}^*}\right) \cdot \sqrt[3]{x + \sqrt{1^2 + x^2}^*}\right)}\right)}\]
7. Applied rem-log-exp0.0
  \[\leadsto \color{blue}{\log \left(\left(\sqrt[3]{x + \sqrt{1^2 + x^2}^*} \cdot \sqrt[3]{x + \sqrt{1^2 + x^2}^*}\right) \cdot \sqrt[3]{x + \sqrt{1^2 + x^2}^*}\right)}\]
8. Simplified0.0
  \[\leadsto \log \color{blue}{\left(x + \sqrt{1^2 + x^2}^*\right)}\]
Recombined 3 regimes into one program.
Final simplification0.1
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -1.0563392067882509:\\ \;\;\;\;\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 0.007387095680401754:\\ \;\;\;\;(\left(x \cdot \frac{-1}{6}\right) \cdot \left(x \cdot x\right) + \left((\frac{3}{40} \cdot \left({x}^{5}\right) + x)_*\right))_*\\ \mathbf{else}:\\ \;\;\;\;\log \left(\sqrt{1^2 + x^2}^* + x\right)\\ \end{array}\]

Error

Target

Derivation

`if x < -1.0563392067882509`

`if -1.0563392067882509 < x < 0.007387095680401754`

`if 0.007387095680401754 < x`

Reproduce