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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.0715992056992538:\\ \;\;\;\;\log \left(\frac{\frac{-1}{2}}{x} - \left(\frac{\frac{1}{16}}{{x}^{5}} - \frac{\frac{1}{8}}{x \cdot \left(x \cdot x\right)}\right)\right)\\ \mathbf{elif}\;x \le 0.0077107299968686566:\\ \;\;\;\;\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 \left(\sqrt{\mathsf{hypot}\left(1, x\right) + x}\right) + \log \left(\sqrt{\mathsf{hypot}\left(1, x\right) + x}\right)\\ \end{array}\]

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

↓

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

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

\end{array}

double f(double x) {
        double r33996801 = x;
        double r33996802 = r33996801 * r33996801;
        double r33996803 = 1.0;
        double r33996804 = r33996802 + r33996803;
        double r33996805 = sqrt(r33996804);
        double r33996806 = r33996801 + r33996805;
        double r33996807 = log(r33996806);
        return r33996807;
}

↓

double f(double x) {
        double r33996808 = x;
        double r33996809 = -1.0715992056992538;
        bool r33996810 = r33996808 <= r33996809;
        double r33996811 = -0.5;
        double r33996812 = r33996811 / r33996808;
        double r33996813 = 0.0625;
        double r33996814 = 5.0;
        double r33996815 = pow(r33996808, r33996814);
        double r33996816 = r33996813 / r33996815;
        double r33996817 = 0.125;
        double r33996818 = r33996808 * r33996808;
        double r33996819 = r33996808 * r33996818;
        double r33996820 = r33996817 / r33996819;
        double r33996821 = r33996816 - r33996820;
        double r33996822 = r33996812 - r33996821;
        double r33996823 = log(r33996822);
        double r33996824 = 0.0077107299968686566;
        bool r33996825 = r33996808 <= r33996824;
        double r33996826 = -0.16666666666666666;
        double r33996827 = r33996808 * r33996826;
        double r33996828 = 0.075;
        double r33996829 = fma(r33996828, r33996815, r33996808);
        double r33996830 = fma(r33996827, r33996818, r33996829);
        double r33996831 = 1.0;
        double r33996832 = hypot(r33996831, r33996808);
        double r33996833 = r33996832 + r33996808;
        double r33996834 = sqrt(r33996833);
        double r33996835 = log(r33996834);
        double r33996836 = r33996835 + r33996835;
        double r33996837 = r33996825 ? r33996830 : r33996836;
        double r33996838 = r33996810 ? r33996823 : r33996837;
        return r33996838;
}

Original	52.5
Target	44.8
Herbie	0.1

Derivation

Split input into 3 regimes
if x < -1.0715992056992538
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.1
  \[\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.1
  \[\leadsto \log \color{blue}{\left(\frac{\frac{-1}{2}}{x} - \left(\frac{\frac{1}{16}}{{x}^{5}} - \frac{\frac{1}{8}}{x \cdot \left(x \cdot x\right)}\right)\right)}\]
if -1.0715992056992538 < x < 0.0077107299968686566
1. Initial program 58.9
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Simplified58.9
  \[\leadsto \color{blue}{\log \left(x + \mathsf{hypot}\left(1, x\right)\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}{\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 0.0077107299968686566 < x
1. Initial program 30.6
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Simplified0.0
  \[\leadsto \color{blue}{\log \left(x + \mathsf{hypot}\left(1, x\right)\right)}\]
3. Using strategy rm
4. Applied add-sqr-sqrt0.0
  \[\leadsto \log \color{blue}{\left(\sqrt{x + \mathsf{hypot}\left(1, x\right)} \cdot \sqrt{x + \mathsf{hypot}\left(1, x\right)}\right)}\]
5. Applied log-prod0.0
  \[\leadsto \color{blue}{\log \left(\sqrt{x + \mathsf{hypot}\left(1, x\right)}\right) + \log \left(\sqrt{x + \mathsf{hypot}\left(1, x\right)}\right)}\]
Recombined 3 regimes into one program.
Final simplification0.1
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -1.0715992056992538:\\ \;\;\;\;\log \left(\frac{\frac{-1}{2}}{x} - \left(\frac{\frac{1}{16}}{{x}^{5}} - \frac{\frac{1}{8}}{x \cdot \left(x \cdot x\right)}\right)\right)\\ \mathbf{elif}\;x \le 0.0077107299968686566:\\ \;\;\;\;\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 \left(\sqrt{\mathsf{hypot}\left(1, x\right) + x}\right) + \log \left(\sqrt{\mathsf{hypot}\left(1, x\right) + x}\right)\\ \end{array}\]

Error

Target

Derivation

`if x < -1.0715992056992538`

`if -1.0715992056992538 < x < 0.0077107299968686566`

`if 0.0077107299968686566 < x`

Reproduce