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

↓

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

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

↓

\begin{array}{l}
\mathbf{if}\;\frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y} \le -10910987967306.1348 \lor \neg \left(\frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y} \le -7.71869811703901377 \cdot 10^{-252}\right):\\
\;\;\;\;x + \frac{e^{y \cdot \left(2 \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)\right) + y \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)}}{y}\\

\mathbf{else}:\\
\;\;\;\;x + \frac{1}{y \cdot e^{z}}\\

\end{array}

double f(double x, double y, double z) {
        double r351269 = x;
        double r351270 = y;
        double r351271 = z;
        double r351272 = r351271 + r351270;
        double r351273 = r351270 / r351272;
        double r351274 = log(r351273);
        double r351275 = r351270 * r351274;
        double r351276 = exp(r351275);
        double r351277 = r351276 / r351270;
        double r351278 = r351269 + r351277;
        return r351278;
}

↓

double f(double x, double y, double z) {
        double r351279 = y;
        double r351280 = z;
        double r351281 = r351280 + r351279;
        double r351282 = r351279 / r351281;
        double r351283 = log(r351282);
        double r351284 = r351279 * r351283;
        double r351285 = exp(r351284);
        double r351286 = r351285 / r351279;
        double r351287 = -10910987967306.135;
        bool r351288 = r351286 <= r351287;
        double r351289 = -7.718698117039014e-252;
        bool r351290 = r351286 <= r351289;
        double r351291 = !r351290;
        bool r351292 = r351288 || r351291;
        double r351293 = x;
        double r351294 = 2.0;
        double r351295 = cbrt(r351279);
        double r351296 = cbrt(r351281);
        double r351297 = r351295 / r351296;
        double r351298 = log(r351297);
        double r351299 = r351294 * r351298;
        double r351300 = r351279 * r351299;
        double r351301 = r351279 * r351298;
        double r351302 = r351300 + r351301;
        double r351303 = exp(r351302);
        double r351304 = r351303 / r351279;
        double r351305 = r351293 + r351304;
        double r351306 = 1.0;
        double r351307 = exp(r351280);
        double r351308 = r351279 * r351307;
        double r351309 = r351306 / r351308;
        double r351310 = r351293 + r351309;
        double r351311 = r351292 ? r351305 : r351310;
        return r351311;
}

Original	6.3
Target	1.3
Herbie	0.9

Derivation

Split input into 2 regimes
if (/ (exp (* y (log (/ y (+ z y))))) y) < -10910987967306.135 or -7.718698117039014e-252 < (/ (exp (* y (log (/ y (+ z y))))) y)
1. Initial program 7.1
  \[x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y}\]
2. Using strategy rm
3. Applied add-cube-cbrt15.8
  \[\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-cbrt7.1
  \[\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-frac7.1
  \[\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-prod2.2
  \[\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-in2.2
  \[\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.8
  \[\leadsto x + \frac{e^{\color{blue}{y \cdot \left(2 \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)\right)} + y \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)}}{y}\]
if -10910987967306.135 < (/ (exp (* y (log (/ y (+ z y))))) y) < -7.718698117039014e-252
1. Initial program 3.0
  \[x + \frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y}\]
2. Taylor expanded around inf 1.1
  \[\leadsto \color{blue}{x + \frac{e^{-1 \cdot z}}{y}}\]
3. Using strategy rm
4. Applied clear-num1.1
  \[\leadsto x + \color{blue}{\frac{1}{\frac{y}{e^{-1 \cdot z}}}}\]
5. Simplified1.1
  \[\leadsto x + \frac{1}{\color{blue}{y \cdot e^{z}}}\]
Recombined 2 regimes into one program.
Final simplification0.9
\[\leadsto \begin{array}{l} \mathbf{if}\;\frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y} \le -10910987967306.1348 \lor \neg \left(\frac{e^{y \cdot \log \left(\frac{y}{z + y}\right)}}{y} \le -7.71869811703901377 \cdot 10^{-252}\right):\\ \;\;\;\;x + \frac{e^{y \cdot \left(2 \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)\right) + y \cdot \log \left(\frac{\sqrt[3]{y}}{\sqrt[3]{z + y}}\right)}}{y}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{1}{y \cdot e^{z}}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if (/ (exp (* y (log (/ y (+ z y))))) y) < -10910987967306.135 or -7.718698117039014e-252 < (/ (exp (* y (log (/ y (+ z y))))) y)`

`if -10910987967306.135 < (/ (exp (* y (log (/ y (+ z y))))) y) < -7.718698117039014e-252`

Reproduce

In
Out