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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.0301407998346479:\\ \;\;\;\;\log \left(\sqrt{\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)}\right) + \log \left(\sqrt{\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)}\right)\\ \mathbf{elif}\;x \le 0.89162235529366485:\\ \;\;\;\;\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 + \left(\left(x + \frac{0.5}{x}\right) - \frac{0.125}{{x}^{3}}\right)\right)\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;x \le -1.0301407998346479:\\
\;\;\;\;\log \left(\sqrt{\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)}\right) + \log \left(\sqrt{\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)}\right)\\

\mathbf{elif}\;x \le 0.89162235529366485:\\
\;\;\;\;\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 + \left(\left(x + \frac{0.5}{x}\right) - \frac{0.125}{{x}^{3}}\right)\right)\\

\end{array}

double f(double x) {
        double r217597 = x;
        double r217598 = r217597 * r217597;
        double r217599 = 1.0;
        double r217600 = r217598 + r217599;
        double r217601 = sqrt(r217600);
        double r217602 = r217597 + r217601;
        double r217603 = log(r217602);
        return r217603;
}

↓

double f(double x) {
        double r217604 = x;
        double r217605 = -1.030140799834648;
        bool r217606 = r217604 <= r217605;
        double r217607 = 0.125;
        double r217608 = 3.0;
        double r217609 = pow(r217604, r217608);
        double r217610 = r217607 / r217609;
        double r217611 = 0.5;
        double r217612 = r217611 / r217604;
        double r217613 = 0.0625;
        double r217614 = -r217613;
        double r217615 = 5.0;
        double r217616 = pow(r217604, r217615);
        double r217617 = r217614 / r217616;
        double r217618 = r217612 - r217617;
        double r217619 = r217610 - r217618;
        double r217620 = sqrt(r217619);
        double r217621 = log(r217620);
        double r217622 = r217621 + r217621;
        double r217623 = 0.8916223552936648;
        bool r217624 = r217604 <= r217623;
        double r217625 = 1.0;
        double r217626 = sqrt(r217625);
        double r217627 = log(r217626);
        double r217628 = r217604 / r217626;
        double r217629 = r217627 + r217628;
        double r217630 = 0.16666666666666666;
        double r217631 = pow(r217626, r217608);
        double r217632 = r217609 / r217631;
        double r217633 = r217630 * r217632;
        double r217634 = r217629 - r217633;
        double r217635 = r217604 + r217612;
        double r217636 = r217635 - r217610;
        double r217637 = r217604 + r217636;
        double r217638 = log(r217637);
        double r217639 = r217624 ? r217634 : r217638;
        double r217640 = r217606 ? r217622 : r217639;
        return r217640;
}

Original	52.5
Target	44.7
Herbie	0.2

Derivation

Split input into 3 regimes
if x < -1.030140799834648
1. Initial program 62.8
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around -inf 0.2
  \[\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.2
  \[\leadsto \log \color{blue}{\left(\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)\right)}\]
4. Using strategy rm
5. Applied add-sqr-sqrt0.2
  \[\leadsto \log \color{blue}{\left(\sqrt{\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)} \cdot \sqrt{\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)}\right)}\]
6. Applied log-prod0.2
  \[\leadsto \color{blue}{\log \left(\sqrt{\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)}\right) + \log \left(\sqrt{\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)}\right)}\]
if -1.030140799834648 < x < 0.8916223552936648
1. Initial program 58.7
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around 0 0.3
  \[\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.8916223552936648 < x
1. Initial program 30.6
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around inf 0.2
  \[\leadsto \log \left(x + \color{blue}{\left(\left(x + 0.5 \cdot \frac{1}{x}\right) - 0.125 \cdot \frac{1}{{x}^{3}}\right)}\right)\]
3. Simplified0.2
  \[\leadsto \log \left(x + \color{blue}{\left(\left(x + \frac{0.5}{x}\right) - \frac{0.125}{{x}^{3}}\right)}\right)\]
Recombined 3 regimes into one program.
Final simplification0.2
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -1.0301407998346479:\\ \;\;\;\;\log \left(\sqrt{\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)}\right) + \log \left(\sqrt{\frac{0.125}{{x}^{3}} - \left(\frac{0.5}{x} - \frac{-0.0625}{{x}^{5}}\right)}\right)\\ \mathbf{elif}\;x \le 0.89162235529366485:\\ \;\;\;\;\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 + \left(\left(x + \frac{0.5}{x}\right) - \frac{0.125}{{x}^{3}}\right)\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if x < -1.030140799834648`

`if -1.030140799834648 < x < 0.8916223552936648`

`if 0.8916223552936648 < x`

Reproduce

In
Out