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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -0.0155597802650863076:\\ \;\;\;\;x - \frac{\log \left(\sqrt{\left(1 - y\right) + y \cdot e^{z}}\right) + \log \left(\sqrt{\left(1 - y\right) + y \cdot e^{z}}\right)}{t}\\ \mathbf{elif}\;z \le 4.93108439134458235 \cdot 10^{-25}:\\ \;\;\;\;x - \left(1 \cdot \left(\left(z \cdot y\right) \cdot \frac{1}{t}\right) + \frac{\log 1}{t}\right)\\ \mathbf{else}:\\ \;\;\;\;x - \frac{\log \left(1 + y \cdot \left(\frac{1}{2} \cdot {z}^{2} + z\right)\right)}{t}\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;z \le -0.0155597802650863076:\\
\;\;\;\;x - \frac{\log \left(\sqrt{\left(1 - y\right) + y \cdot e^{z}}\right) + \log \left(\sqrt{\left(1 - y\right) + y \cdot e^{z}}\right)}{t}\\

\mathbf{elif}\;z \le 4.93108439134458235 \cdot 10^{-25}:\\
\;\;\;\;x - \left(1 \cdot \left(\left(z \cdot y\right) \cdot \frac{1}{t}\right) + \frac{\log 1}{t}\right)\\

\mathbf{else}:\\
\;\;\;\;x - \frac{\log \left(1 + y \cdot \left(\frac{1}{2} \cdot {z}^{2} + z\right)\right)}{t}\\

\end{array}

double f(double x, double y, double z, double t) {
        double r312441 = x;
        double r312442 = 1.0;
        double r312443 = y;
        double r312444 = r312442 - r312443;
        double r312445 = z;
        double r312446 = exp(r312445);
        double r312447 = r312443 * r312446;
        double r312448 = r312444 + r312447;
        double r312449 = log(r312448);
        double r312450 = t;
        double r312451 = r312449 / r312450;
        double r312452 = r312441 - r312451;
        return r312452;
}

↓

double f(double x, double y, double z, double t) {
        double r312453 = z;
        double r312454 = -0.015559780265086308;
        bool r312455 = r312453 <= r312454;
        double r312456 = x;
        double r312457 = 1.0;
        double r312458 = y;
        double r312459 = r312457 - r312458;
        double r312460 = exp(r312453);
        double r312461 = r312458 * r312460;
        double r312462 = r312459 + r312461;
        double r312463 = sqrt(r312462);
        double r312464 = log(r312463);
        double r312465 = r312464 + r312464;
        double r312466 = t;
        double r312467 = r312465 / r312466;
        double r312468 = r312456 - r312467;
        double r312469 = 4.931084391344582e-25;
        bool r312470 = r312453 <= r312469;
        double r312471 = r312453 * r312458;
        double r312472 = 1.0;
        double r312473 = r312472 / r312466;
        double r312474 = r312471 * r312473;
        double r312475 = r312457 * r312474;
        double r312476 = log(r312457);
        double r312477 = r312476 / r312466;
        double r312478 = r312475 + r312477;
        double r312479 = r312456 - r312478;
        double r312480 = 0.5;
        double r312481 = 2.0;
        double r312482 = pow(r312453, r312481);
        double r312483 = r312480 * r312482;
        double r312484 = r312483 + r312453;
        double r312485 = r312458 * r312484;
        double r312486 = r312457 + r312485;
        double r312487 = log(r312486);
        double r312488 = r312487 / r312466;
        double r312489 = r312456 - r312488;
        double r312490 = r312470 ? r312479 : r312489;
        double r312491 = r312455 ? r312468 : r312490;
        return r312491;
}

Original	24.7
Target	15.9
Herbie	8.1

Derivation

Split input into 3 regimes
if z < -0.015559780265086308
1. Initial program 10.8
  \[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]
2. Using strategy rm
3. Applied add-sqr-sqrt10.8
  \[\leadsto x - \frac{\log \color{blue}{\left(\sqrt{\left(1 - y\right) + y \cdot e^{z}} \cdot \sqrt{\left(1 - y\right) + y \cdot e^{z}}\right)}}{t}\]
4. Applied log-prod10.8
  \[\leadsto x - \frac{\color{blue}{\log \left(\sqrt{\left(1 - y\right) + y \cdot e^{z}}\right) + \log \left(\sqrt{\left(1 - y\right) + y \cdot e^{z}}\right)}}{t}\]
if -0.015559780265086308 < z < 4.931084391344582e-25
1. Initial program 30.9
  \[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]
2. Taylor expanded around 0 6.5
  \[\leadsto x - \frac{\color{blue}{0.5 \cdot \left({z}^{2} \cdot y\right) + \left(1 \cdot \left(z \cdot y\right) + \log 1\right)}}{t}\]
3. Simplified6.5
  \[\leadsto x - \frac{\color{blue}{\log 1 + y \cdot \left(z \cdot \left(0.5 \cdot z + 1\right)\right)}}{t}\]
4. Taylor expanded around 0 6.6
  \[\leadsto \color{blue}{x - \left(1 \cdot \frac{z \cdot y}{t} + \frac{\log 1}{t}\right)}\]
5. Using strategy rm
6. Applied div-inv6.6
  \[\leadsto x - \left(1 \cdot \color{blue}{\left(\left(z \cdot y\right) \cdot \frac{1}{t}\right)} + \frac{\log 1}{t}\right)\]
if 4.931084391344582e-25 < z
1. Initial program 26.6
  \[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]
2. Taylor expanded around 0 14.5
  \[\leadsto x - \frac{\log \color{blue}{\left(\frac{1}{2} \cdot \left({z}^{2} \cdot y\right) + \left(z \cdot y + 1\right)\right)}}{t}\]
3. Simplified14.5
  \[\leadsto x - \frac{\log \color{blue}{\left(1 + y \cdot \left(\frac{1}{2} \cdot {z}^{2} + z\right)\right)}}{t}\]
Recombined 3 regimes into one program.
Final simplification8.1
\[\leadsto \begin{array}{l} \mathbf{if}\;z \le -0.0155597802650863076:\\ \;\;\;\;x - \frac{\log \left(\sqrt{\left(1 - y\right) + y \cdot e^{z}}\right) + \log \left(\sqrt{\left(1 - y\right) + y \cdot e^{z}}\right)}{t}\\ \mathbf{elif}\;z \le 4.93108439134458235 \cdot 10^{-25}:\\ \;\;\;\;x - \left(1 \cdot \left(\left(z \cdot y\right) \cdot \frac{1}{t}\right) + \frac{\log 1}{t}\right)\\ \mathbf{else}:\\ \;\;\;\;x - \frac{\log \left(1 + y \cdot \left(\frac{1}{2} \cdot {z}^{2} + z\right)\right)}{t}\\ \end{array}\]

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

could not determine a ground truth for program body (more)

Error

Try it out

Target

Derivation

`if z < -0.015559780265086308`

`if -0.015559780265086308 < z < 4.931084391344582e-25`

`if 4.931084391344582e-25 < z`

Reproduce

In
Out