\[x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y}\]

↓

\[\begin{array}{l} \mathbf{if}\;y \le -6.13689162563550475538429628460746343967 \cdot 10^{60}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\sqrt{e^{-z}}}{\sqrt[3]{y} \cdot \sqrt[3]{y}}, \frac{\sqrt{e^{-z}}}{\sqrt[3]{y}}, x\right)\\ \mathbf{else}:\\ \;\;\;\;x + \frac{e^{\left(2 \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)\right) \cdot y + y \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)}}{y}\\ \end{array}\]

x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y}

↓

\begin{array}{l}
\mathbf{if}\;y \le -6.13689162563550475538429628460746343967 \cdot 10^{60}:\\
\;\;\;\;\mathsf{fma}\left(\frac{\sqrt{e^{-z}}}{\sqrt[3]{y} \cdot \sqrt[3]{y}}, \frac{\sqrt{e^{-z}}}{\sqrt[3]{y}}, x\right)\\

\mathbf{else}:\\
\;\;\;\;x + \frac{e^{\left(2 \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)\right) \cdot y + y \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)}}{y}\\

\end{array}

double f(double x, double y, double z) {
        double r247358 = x;
        double r247359 = y;
        double r247360 = z;
        double r247361 = r247360 + r247359;
        double r247362 = r247359 / r247361;
        double r247363 = log(r247362);
        double r247364 = r247359 * r247363;
        double r247365 = exp(r247364);
        double r247366 = r247365 / r247359;
        double r247367 = r247358 + r247366;
        return r247367;
}

↓

double f(double x, double y, double z) {
        double r247368 = y;
        double r247369 = -6.136891625635505e+60;
        bool r247370 = r247368 <= r247369;
        double r247371 = z;
        double r247372 = -r247371;
        double r247373 = exp(r247372);
        double r247374 = sqrt(r247373);
        double r247375 = cbrt(r247368);
        double r247376 = r247375 * r247375;
        double r247377 = r247374 / r247376;
        double r247378 = r247374 / r247375;
        double r247379 = x;
        double r247380 = fma(r247377, r247378, r247379);
        double r247381 = 2.0;
        double r247382 = r247371 + r247368;
        double r247383 = cbrt(r247382);
        double r247384 = r247375 / r247383;
        double r247385 = log(r247384);
        double r247386 = r247381 * r247385;
        double r247387 = r247386 * r247368;
        double r247388 = r247368 * r247385;
        double r247389 = r247387 + r247388;
        double r247390 = exp(r247389);
        double r247391 = r247390 / r247368;
        double r247392 = r247379 + r247391;
        double r247393 = r247370 ? r247380 : r247392;
        return r247393;
}

Original	6.0
Target	1.0
Herbie	0.6

Derivation

Split input into 2 regimes
if y < -6.136891625635505e+60
1. Initial program 2.4
  \[x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y}\]
2. Taylor expanded around inf 0.1
  \[\leadsto \color{blue}{x + \frac{e^{-1 \cdot z}}{y}}\]
3. Simplified0.1
  \[\leadsto \color{blue}{\frac{e^{-z}}{y} + x}\]
4. Using strategy rm
5. Applied add-cube-cbrt0.3
  \[\leadsto \frac{e^{-z}}{\color{blue}{\left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) \cdot \sqrt[3]{y}}} + x\]
6. Applied add-sqr-sqrt0.3
  \[\leadsto \frac{\color{blue}{\sqrt{e^{-z}} \cdot \sqrt{e^{-z}}}}{\left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) \cdot \sqrt[3]{y}} + x\]
7. Applied times-frac0.3
  \[\leadsto \color{blue}{\frac{\sqrt{e^{-z}}}{\sqrt[3]{y} \cdot \sqrt[3]{y}} \cdot \frac{\sqrt{e^{-z}}}{\sqrt[3]{y}}} + x\]
8. Applied fma-def0.3
  \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\sqrt{e^{-z}}}{\sqrt[3]{y} \cdot \sqrt[3]{y}}, \frac{\sqrt{e^{-z}}}{\sqrt[3]{y}}, x\right)}\]
if -6.136891625635505e+60 < y
1. Initial program 6.9
  \[x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y}\]
2. Using strategy rm
3. Applied add-cube-cbrt15.0
  \[\leadsto x + \frac{e^{y \cdot \log \left(\frac{y}{\color{blue}{\left(\sqrt[3]{z + y} \cdot \sqrt[3]{z + y}\right) \cdot \sqrt[3]{z + y}}}\right)}}{y}\]
4. Applied add-cube-cbrt6.9
  \[\leadsto x + \frac{e^{y \cdot \log \left(\frac{\color{blue}{\left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) \cdot \sqrt[3]{y}}}{\left(\sqrt[3]{z + y} \cdot \sqrt[3]{z + y}\right) \cdot \sqrt[3]{z + y}}\right)}}{y}\]
5. Applied times-frac6.9
  \[\leadsto x + \frac{e^{y \cdot \log \color{blue}{\left(\frac{\sqrt[3]{y} \cdot \sqrt[3]{y}}{\sqrt[3]{z + y} \cdot \sqrt[3]{z + y}} \cdot \frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)}}}{y}\]
6. Applied log-prod1.9
  \[\leadsto x + \frac{e^{y \cdot \color{blue}{\left(\log \left(\frac{\sqrt[3]{y} \cdot \sqrt[3]{y}}{\sqrt[3]{z + y} \cdot \sqrt[3]{z + y}}\right) + \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)\right)}}}{y}\]
7. Applied distribute-lft-in1.9
  \[\leadsto x + \frac{e^{\color{blue}{y \cdot \log \left(\frac{\sqrt[3]{y} \cdot \sqrt[3]{y}}{\sqrt[3]{z + y} \cdot \sqrt[3]{z + y}}\right) + y \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)}}}{y}\]
8. Simplified0.7
  \[\leadsto x + \frac{e^{\color{blue}{\left(2 \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)\right) \cdot y} + y \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)}}{y}\]
Recombined 2 regimes into one program.
Final simplification0.6
\[\leadsto \begin{array}{l} \mathbf{if}\;y \le -6.13689162563550475538429628460746343967 \cdot 10^{60}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\sqrt{e^{-z}}}{\sqrt[3]{y} \cdot \sqrt[3]{y}}, \frac{\sqrt{e^{-z}}}{\sqrt[3]{y}}, x\right)\\ \mathbf{else}:\\ \;\;\;\;x + \frac{e^{\left(2 \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)\right) \cdot y + y \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)}}{y}\\ \end{array}\]

Error

Target

Derivation

`if y < -6.136891625635505e+60`

`if -6.136891625635505e+60 < y`

Reproduce