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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -0.995295059253408442856425608624704182148:\\ \;\;\;\;\log \left(\left(\frac{0.125}{{x}^{3}} - \frac{0.0625}{{x}^{5}}\right) - \frac{0.5}{x}\right)\\ \mathbf{elif}\;x \le 0.8946210124348296099938693259900901466608:\\ \;\;\;\;\log \left(\sqrt{1}\right) + \left(x + \frac{{x}^{3}}{\frac{1}{\frac{-1}{6}}}\right) \cdot \frac{1}{\sqrt{1}}\\ \mathbf{else}:\\ \;\;\;\;\log \left(\left(\frac{0.5}{x} - \frac{0.125}{{x}^{3}}\right) + 2 \cdot x\right)\\ \end{array}\]

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

↓

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

\mathbf{elif}\;x \le 0.8946210124348296099938693259900901466608:\\
\;\;\;\;\log \left(\sqrt{1}\right) + \left(x + \frac{{x}^{3}}{\frac{1}{\frac{-1}{6}}}\right) \cdot \frac{1}{\sqrt{1}}\\

\mathbf{else}:\\
\;\;\;\;\log \left(\left(\frac{0.5}{x} - \frac{0.125}{{x}^{3}}\right) + 2 \cdot x\right)\\

\end{array}

double f(double x) {
        double r135281 = x;
        double r135282 = r135281 * r135281;
        double r135283 = 1.0;
        double r135284 = r135282 + r135283;
        double r135285 = sqrt(r135284);
        double r135286 = r135281 + r135285;
        double r135287 = log(r135286);
        return r135287;
}

↓

double f(double x) {
        double r135288 = x;
        double r135289 = -0.9952950592534084;
        bool r135290 = r135288 <= r135289;
        double r135291 = 0.125;
        double r135292 = 3.0;
        double r135293 = pow(r135288, r135292);
        double r135294 = r135291 / r135293;
        double r135295 = 0.0625;
        double r135296 = 5.0;
        double r135297 = pow(r135288, r135296);
        double r135298 = r135295 / r135297;
        double r135299 = r135294 - r135298;
        double r135300 = 0.5;
        double r135301 = r135300 / r135288;
        double r135302 = r135299 - r135301;
        double r135303 = log(r135302);
        double r135304 = 0.8946210124348296;
        bool r135305 = r135288 <= r135304;
        double r135306 = 1.0;
        double r135307 = sqrt(r135306);
        double r135308 = log(r135307);
        double r135309 = -0.16666666666666666;
        double r135310 = r135306 / r135309;
        double r135311 = r135293 / r135310;
        double r135312 = r135288 + r135311;
        double r135313 = 1.0;
        double r135314 = r135313 / r135307;
        double r135315 = r135312 * r135314;
        double r135316 = r135308 + r135315;
        double r135317 = r135301 - r135294;
        double r135318 = 2.0;
        double r135319 = r135318 * r135288;
        double r135320 = r135317 + r135319;
        double r135321 = log(r135320);
        double r135322 = r135305 ? r135316 : r135321;
        double r135323 = r135290 ? r135303 : r135322;
        return r135323;
}

Original	53.4
Target	45.4
Herbie	0.2

Derivation

Split input into 3 regimes
if x < -0.9952950592534084
1. Initial program 63.0
  \[\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(\left(\frac{0.125}{{x}^{3}} - \frac{0.0625}{{x}^{5}}\right) - \frac{0.5}{x}\right)}\]
if -0.9952950592534084 < x < 0.8946210124348296
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}}}\]
3. Simplified0.2
  \[\leadsto \color{blue}{\log \left(\sqrt{1}\right) + \left(\frac{-1}{6} \cdot \frac{x \cdot x}{1} + 1\right) \cdot \frac{x}{\sqrt{1}}}\]
4. Using strategy rm
5. Applied div-inv0.2
  \[\leadsto \log \left(\sqrt{1}\right) + \left(\frac{-1}{6} \cdot \frac{x \cdot x}{1} + 1\right) \cdot \color{blue}{\left(x \cdot \frac{1}{\sqrt{1}}\right)}\]
6. Applied associate-*r*0.2
  \[\leadsto \log \left(\sqrt{1}\right) + \color{blue}{\left(\left(\frac{-1}{6} \cdot \frac{x \cdot x}{1} + 1\right) \cdot x\right) \cdot \frac{1}{\sqrt{1}}}\]
7. Simplified0.2
  \[\leadsto \log \left(\sqrt{1}\right) + \color{blue}{\left(x + \frac{{x}^{3}}{\frac{1}{\frac{-1}{6}}}\right)} \cdot \frac{1}{\sqrt{1}}\]
if 0.8946210124348296 < x
1. Initial program 31.7
  \[\log \left(x + \sqrt{x \cdot x + 1}\right)\]
2. Taylor expanded around inf 0.2
  \[\leadsto \log \color{blue}{\left(\left(2 \cdot x + 0.5 \cdot \frac{1}{x}\right) - 0.125 \cdot \frac{1}{{x}^{3}}\right)}\]
3. Simplified0.2
  \[\leadsto \log \color{blue}{\left(\left(\frac{0.5}{x} - \frac{0.125}{{x}^{3}}\right) + 2 \cdot x\right)}\]
Recombined 3 regimes into one program.
Final simplification0.2
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -0.995295059253408442856425608624704182148:\\ \;\;\;\;\log \left(\left(\frac{0.125}{{x}^{3}} - \frac{0.0625}{{x}^{5}}\right) - \frac{0.5}{x}\right)\\ \mathbf{elif}\;x \le 0.8946210124348296099938693259900901466608:\\ \;\;\;\;\log \left(\sqrt{1}\right) + \left(x + \frac{{x}^{3}}{\frac{1}{\frac{-1}{6}}}\right) \cdot \frac{1}{\sqrt{1}}\\ \mathbf{else}:\\ \;\;\;\;\log \left(\left(\frac{0.5}{x} - \frac{0.125}{{x}^{3}}\right) + 2 \cdot x\right)\\ \end{array}\]

Falling back on racket egraph because egg-herbie package not installed (more)

Error

Try it out

Target

Derivation

`if x < -0.9952950592534084`

`if -0.9952950592534084 < x < 0.8946210124348296`

`if 0.8946210124348296 < x`

Reproduce

In
Out