\[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 r423614 = x;
        double r423615 = y;
        double r423616 = z;
        double r423617 = r423616 + r423615;
        double r423618 = r423615 / r423617;
        double r423619 = log(r423618);
        double r423620 = r423615 * r423619;
        double r423621 = exp(r423620);
        double r423622 = r423621 / r423615;
        double r423623 = r423614 + r423622;
        return r423623;
}

↓

double f(double x, double y, double z) {
        double r423624 = y;
        double r423625 = -8.861416360526609e+33;
        bool r423626 = r423624 <= r423625;
        double r423627 = x;
        double r423628 = -1.0;
        double r423629 = z;
        double r423630 = r423628 * r423629;
        double r423631 = exp(r423630);
        double r423632 = r423631 / r423624;
        double r423633 = r423627 + r423632;
        double r423634 = cbrt(r423624);
        double r423635 = r423634 * r423634;
        double r423636 = log(r423635);
        double r423637 = 1.0;
        double r423638 = cbrt(r423637);
        double r423639 = r423629 + r423624;
        double r423640 = cbrt(r423639);
        double r423641 = r423640 * r423640;
        double r423642 = r423638 / r423641;
        double r423643 = log(r423642);
        double r423644 = r423634 / r423640;
        double r423645 = log(r423644);
        double r423646 = r423643 + r423645;
        double r423647 = r423636 + r423646;
        double r423648 = r423624 * r423647;
        double r423649 = exp(r423648);
        double r423650 = r423649 / r423624;
        double r423651 = r423627 + r423650;
        double r423652 = r423626 ? r423633 : r423651;
        return r423652;
}

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