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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.0666762070372178:\\ \;\;\;\;\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.008211186064708345:\\ \;\;\;\;(\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 r5849674 = x;
        double r5849675 = r5849674 * r5849674;
        double r5849676 = 1.0;
        double r5849677 = r5849675 + r5849676;
        double r5849678 = sqrt(r5849677);
        double r5849679 = r5849674 + r5849678;
        double r5849680 = log(r5849679);
        return r5849680;
}

↓

double f(double x) {
        double r5849681 = x;
        double r5849682 = -1.0666762070372178;
        bool r5849683 = r5849681 <= r5849682;
        double r5849684 = 0.125;
        double r5849685 = r5849684 / r5849681;
        double r5849686 = r5849681 * r5849681;
        double r5849687 = r5849685 / r5849686;
        double r5849688 = 0.5;
        double r5849689 = r5849688 / r5849681;
        double r5849690 = 0.0625;
        double r5849691 = 5.0;
        double r5849692 = pow(r5849681, r5849691);
        double r5849693 = r5849690 / r5849692;
        double r5849694 = r5849689 + r5849693;
        double r5849695 = r5849687 - r5849694;
        double r5849696 = log(r5849695);
        double r5849697 = 0.008211186064708345;
        bool r5849698 = r5849681 <= r5849697;
        double r5849699 = -0.16666666666666666;
        double r5849700 = r5849681 * r5849699;
        double r5849701 = 0.075;
        double r5849702 = fma(r5849701, r5849692, r5849681);
        double r5849703 = fma(r5849700, r5849686, r5849702);
        double r5849704 = 1.0;
        double r5849705 = hypot(r5849704, r5849681);
        double r5849706 = r5849705 + r5849681;
        double r5849707 = log(r5849706);
        double r5849708 = r5849698 ? r5849703 : r5849707;
        double r5849709 = r5849683 ? r5849696 : r5849708;
        return r5849709;
}

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

↓

\begin{array}{l}
\mathbf{if}\;x \le -1.0666762070372178:\\
\;\;\;\;\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.008211186064708345:\\
\;\;\;\;(\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.2
Target	44.0
Herbie	0.1

Derivation

Split input into 3 regimes
if x < -1.0666762070372178
1. Initial program 61.8
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Simplified61.0
  \[\leadsto \color{blue}{\log \left(x + \sqrt{1^2 + x^2}^*\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.0666762070372178 < x < 0.008211186064708345
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.008211186064708345 < x
1. Initial program 29.8
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Simplified0.1
  \[\leadsto \color{blue}{\log \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.0666762070372178:\\ \;\;\;\;\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.008211186064708345:\\ \;\;\;\;(\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.0666762070372178`

`if -1.0666762070372178 < x < 0.008211186064708345`

`if 0.008211186064708345 < x`

Reproduce