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

↓

\[\begin{array}{l} \mathbf{if}\;y \le -8.86141636052660879 \cdot 10^{33}:\\ \;\;\;\;x + \frac{e^{-1 \cdot z}}{y}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{e^{y \cdot \left(\log \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) + \left(\log \left(\frac{\sqrt[3]{1}}{\sqrt[3]{z + y} \cdot \sqrt[3]{z + y}}\right) + \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)\right)\right)}}{y}\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;y \le -8.86141636052660879 \cdot 10^{33}:\\
\;\;\;\;x + \frac{e^{-1 \cdot z}}{y}\\

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

\end{array}

double f(double x, double y, double z) {
        double r504244 = x;
        double r504245 = y;
        double r504246 = z;
        double r504247 = r504246 + r504245;
        double r504248 = r504245 / r504247;
        double r504249 = log(r504248);
        double r504250 = r504245 * r504249;
        double r504251 = exp(r504250);
        double r504252 = r504251 / r504245;
        double r504253 = r504244 + r504252;
        return r504253;
}

↓

double f(double x, double y, double z) {
        double r504254 = y;
        double r504255 = -8.861416360526609e+33;
        bool r504256 = r504254 <= r504255;
        double r504257 = x;
        double r504258 = -1.0;
        double r504259 = z;
        double r504260 = r504258 * r504259;
        double r504261 = exp(r504260);
        double r504262 = r504261 / r504254;
        double r504263 = r504257 + r504262;
        double r504264 = cbrt(r504254);
        double r504265 = r504264 * r504264;
        double r504266 = log(r504265);
        double r504267 = 1.0;
        double r504268 = cbrt(r504267);
        double r504269 = r504259 + r504254;
        double r504270 = cbrt(r504269);
        double r504271 = r504270 * r504270;
        double r504272 = r504268 / r504271;
        double r504273 = log(r504272);
        double r504274 = r504264 / r504270;
        double r504275 = log(r504274);
        double r504276 = r504273 + r504275;
        double r504277 = r504266 + r504276;
        double r504278 = r504254 * r504277;
        double r504279 = exp(r504278);
        double r504280 = r504279 / r504254;
        double r504281 = r504257 + r504280;
        double r504282 = r504256 ? r504263 : r504281;
        return r504282;
}

Original	6.1
Target	1.1
Herbie	0.6

Derivation

Split input into 2 regimes
if y < -8.861416360526609e+33
1. Initial program 2.6
  \[x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y}\]
2. Taylor expanded around inf 0.0
  \[\leadsto \color{blue}{x + \frac{e^{-1 \cdot z}}{y}}\]
if -8.861416360526609e+33 < y
1. Initial program 7.0
  \[x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y}\]
2. Using strategy rm
3. Applied *-un-lft-identity7.0
  \[\leadsto x + \frac{e^{y \cdot \log \left(\frac{y}{\color{blue}{1 \cdot \left(z + y\right)}}\right)}}{y}\]
4. Applied add-cube-cbrt17.8
  \[\leadsto x + \frac{e^{y \cdot \log \left(\frac{\color{blue}{\left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) \cdot \sqrt[3]{y}}}{1 \cdot \left(z + y\right)}\right)}}{y}\]
5. Applied times-frac17.4
  \[\leadsto x + \frac{e^{y \cdot \log \color{blue}{\left(\frac{\sqrt[3]{y} \cdot \sqrt[3]{y}}{1} \cdot \frac{\sqrt[3]{y}}{z + y}\right)}}}{y}\]
6. Applied log-prod2.7
  \[\leadsto x + \frac{e^{y \cdot \color{blue}{\left(\log \left(\frac{\sqrt[3]{y} \cdot \sqrt[3]{y}}{1}\right) + \log \left(\frac{\sqrt[3]{y}}{z + y}\right)\right)}}}{y}\]
7. Simplified2.7
  \[\leadsto x + \frac{e^{y \cdot \left(\color{blue}{\log \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right)} + \log \left(\frac{\sqrt[3]{y}}{z + y}\right)\right)}}{y}\]
8. Using strategy rm
9. Applied add-cube-cbrt2.5
  \[\leadsto x + \frac{e^{y \cdot \left(\log \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) + \log \left(\frac{\sqrt[3]{y}}{\color{blue}{\left(\sqrt[3]{z + y} \cdot \sqrt[3]{z + y}\right) \cdot \sqrt[3]{z + y}}}\right)\right)}}{y}\]
10. Applied *-un-lft-identity2.5
  \[\leadsto x + \frac{e^{y \cdot \left(\log \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) + \log \left(\frac{\sqrt[3]{\color{blue}{1 \cdot y}}}{\left(\sqrt[3]{z + y} \cdot \sqrt[3]{z + y}\right) \cdot \sqrt[3]{z + y}}\right)\right)}}{y}\]
11. Applied cbrt-prod2.5
  \[\leadsto x + \frac{e^{y \cdot \left(\log \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) + \log \left(\frac{\color{blue}{\sqrt[3]{1} \cdot \sqrt[3]{y}}}{\left(\sqrt[3]{z + y} \cdot \sqrt[3]{z + y}\right) \cdot \sqrt[3]{z + y}}\right)\right)}}{y}\]
12. Applied times-frac2.5
  \[\leadsto x + \frac{e^{y \cdot \left(\log \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) + \log \color{blue}{\left(\frac{\sqrt[3]{1}}{\sqrt[3]{z + y} \cdot \sqrt[3]{z + y}} \cdot \frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)}\right)}}{y}\]
13. Applied log-prod0.7
  \[\leadsto x + \frac{e^{y \cdot \left(\log \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) + \color{blue}{\left(\log \left(\frac{\sqrt[3]{1}}{\sqrt[3]{z + y} \cdot \sqrt[3]{z + y}}\right) + \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)\right)}\right)}}{y}\]
Recombined 2 regimes into one program.
Final simplification0.6
\[\leadsto \begin{array}{l} \mathbf{if}\;y \le -8.86141636052660879 \cdot 10^{33}:\\ \;\;\;\;x + \frac{e^{-1 \cdot z}}{y}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{e^{y \cdot \left(\log \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) + \left(\log \left(\frac{\sqrt[3]{1}}{\sqrt[3]{z + y} \cdot \sqrt[3]{z + y}}\right) + \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)\right)\right)}}{y}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if y < -8.861416360526609e+33`

`if -8.861416360526609e+33 < y`

Reproduce

In
Out