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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -0.3115017031960372051457852649036794900894:\\ \;\;\;\;x - \sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)} \cdot \frac{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}{t}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{1}{\frac{t}{\mathsf{fma}\left(y, \mathsf{fma}\left(0.5, {z}^{2}, 1 \cdot z\right), \log 1\right)}}\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;z \le -0.3115017031960372051457852649036794900894:\\
\;\;\;\;x - \sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)} \cdot \frac{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}{t}\\

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

\end{array}

double f(double x, double y, double z, double t) {
        double r180456 = x;
        double r180457 = 1.0;
        double r180458 = y;
        double r180459 = r180457 - r180458;
        double r180460 = z;
        double r180461 = exp(r180460);
        double r180462 = r180458 * r180461;
        double r180463 = r180459 + r180462;
        double r180464 = log(r180463);
        double r180465 = t;
        double r180466 = r180464 / r180465;
        double r180467 = r180456 - r180466;
        return r180467;
}

↓

double f(double x, double y, double z, double t) {
        double r180468 = z;
        double r180469 = -0.3115017031960372;
        bool r180470 = r180468 <= r180469;
        double r180471 = x;
        double r180472 = expm1(r180468);
        double r180473 = y;
        double r180474 = 1.0;
        double r180475 = fma(r180472, r180473, r180474);
        double r180476 = log(r180475);
        double r180477 = sqrt(r180476);
        double r180478 = t;
        double r180479 = r180477 / r180478;
        double r180480 = r180477 * r180479;
        double r180481 = r180471 - r180480;
        double r180482 = 1.0;
        double r180483 = 0.5;
        double r180484 = 2.0;
        double r180485 = pow(r180468, r180484);
        double r180486 = r180474 * r180468;
        double r180487 = fma(r180483, r180485, r180486);
        double r180488 = log(r180474);
        double r180489 = fma(r180473, r180487, r180488);
        double r180490 = r180478 / r180489;
        double r180491 = r180482 / r180490;
        double r180492 = r180471 - r180491;
        double r180493 = r180470 ? r180481 : r180492;
        return r180493;
}

Original	25.4
Target	16.5
Herbie	8.8

Derivation

Split input into 2 regimes
if z < -0.3115017031960372
1. Initial program 10.9
  \[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]
2. Simplified10.9
  \[\leadsto \color{blue}{x - \frac{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}{t}}\]
3. Using strategy rm
4. Applied *-un-lft-identity10.9
  \[\leadsto x - \frac{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}{\color{blue}{1 \cdot t}}\]
5. Applied add-sqr-sqrt11.8
  \[\leadsto x - \frac{\color{blue}{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)} \cdot \sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}}{1 \cdot t}\]
6. Applied times-frac11.8
  \[\leadsto x - \color{blue}{\frac{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}{1} \cdot \frac{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}{t}}\]
7. Simplified11.8
  \[\leadsto x - \color{blue}{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}} \cdot \frac{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}{t}\]
if -0.3115017031960372 < z
1. Initial program 31.3
  \[x - \frac{\log \left(\left(1 - y\right) + y \cdot e^{z}\right)}{t}\]
2. Simplified11.9
  \[\leadsto \color{blue}{x - \frac{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}{t}}\]
3. Using strategy rm
4. Applied clear-num11.9
  \[\leadsto x - \color{blue}{\frac{1}{\frac{t}{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}}\]
5. Taylor expanded around 0 7.6
  \[\leadsto x - \frac{1}{\frac{t}{\color{blue}{0.5 \cdot \left({z}^{2} \cdot y\right) + \left(1 \cdot \left(z \cdot y\right) + \log 1\right)}}}\]
6. Simplified7.6
  \[\leadsto x - \frac{1}{\frac{t}{\color{blue}{\mathsf{fma}\left(y, \mathsf{fma}\left(0.5, {z}^{2}, 1 \cdot z\right), \log 1\right)}}}\]
Recombined 2 regimes into one program.
Final simplification8.8
\[\leadsto \begin{array}{l} \mathbf{if}\;z \le -0.3115017031960372051457852649036794900894:\\ \;\;\;\;x - \sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)} \cdot \frac{\sqrt{\log \left(\mathsf{fma}\left(\mathsf{expm1}\left(z\right), y, 1\right)\right)}}{t}\\ \mathbf{else}:\\ \;\;\;\;x - \frac{1}{\frac{t}{\mathsf{fma}\left(y, \mathsf{fma}\left(0.5, {z}^{2}, 1 \cdot z\right), \log 1\right)}}\\ \end{array}\]

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

Error

Target

Derivation

`if z < -0.3115017031960372`

`if -0.3115017031960372 < z`

Reproduce