\[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}\]

↓

\[\begin{array}{l} \mathbf{if}\;wj \le 2.7403440668061758 \cdot 10^{-12}:\\ \;\;\;\;\left(wj \cdot wj + \left(\left(wj \cdot wj\right) \cdot \left(wj \cdot wj\right) - \left(wj \cdot wj\right) \cdot wj\right)\right) + \frac{x}{e^{wj} \cdot wj + e^{wj}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(wj \cdot wj\right) \cdot wj - \left(\frac{wj}{1 + wj} \cdot \frac{wj}{1 + wj}\right) \cdot \frac{wj}{1 + wj}}{wj \cdot wj + \frac{wj}{1 + wj} \cdot \left(\frac{wj}{1 + wj} + wj\right)} + \frac{x}{e^{wj} \cdot wj + e^{wj}}\\ \end{array}\]

wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}

↓

\begin{array}{l}
\mathbf{if}\;wj \le 2.7403440668061758 \cdot 10^{-12}:\\
\;\;\;\;\left(wj \cdot wj + \left(\left(wj \cdot wj\right) \cdot \left(wj \cdot wj\right) - \left(wj \cdot wj\right) \cdot wj\right)\right) + \frac{x}{e^{wj} \cdot wj + e^{wj}}\\

\mathbf{else}:\\
\;\;\;\;\frac{\left(wj \cdot wj\right) \cdot wj - \left(\frac{wj}{1 + wj} \cdot \frac{wj}{1 + wj}\right) \cdot \frac{wj}{1 + wj}}{wj \cdot wj + \frac{wj}{1 + wj} \cdot \left(\frac{wj}{1 + wj} + wj\right)} + \frac{x}{e^{wj} \cdot wj + e^{wj}}\\

\end{array}

double f(double wj, double x) {
        double r8863416 = wj;
        double r8863417 = exp(r8863416);
        double r8863418 = r8863416 * r8863417;
        double r8863419 = x;
        double r8863420 = r8863418 - r8863419;
        double r8863421 = r8863417 + r8863418;
        double r8863422 = r8863420 / r8863421;
        double r8863423 = r8863416 - r8863422;
        return r8863423;
}

↓

double f(double wj, double x) {
        double r8863424 = wj;
        double r8863425 = 2.7403440668061758e-12;
        bool r8863426 = r8863424 <= r8863425;
        double r8863427 = r8863424 * r8863424;
        double r8863428 = r8863427 * r8863427;
        double r8863429 = r8863427 * r8863424;
        double r8863430 = r8863428 - r8863429;
        double r8863431 = r8863427 + r8863430;
        double r8863432 = x;
        double r8863433 = exp(r8863424);
        double r8863434 = r8863433 * r8863424;
        double r8863435 = r8863434 + r8863433;
        double r8863436 = r8863432 / r8863435;
        double r8863437 = r8863431 + r8863436;
        double r8863438 = 1.0;
        double r8863439 = r8863438 + r8863424;
        double r8863440 = r8863424 / r8863439;
        double r8863441 = r8863440 * r8863440;
        double r8863442 = r8863441 * r8863440;
        double r8863443 = r8863429 - r8863442;
        double r8863444 = r8863440 + r8863424;
        double r8863445 = r8863440 * r8863444;
        double r8863446 = r8863427 + r8863445;
        double r8863447 = r8863443 / r8863446;
        double r8863448 = r8863447 + r8863436;
        double r8863449 = r8863426 ? r8863437 : r8863448;
        return r8863449;
}

Original	13.5
Target	12.8
Herbie	0.4

Derivation

Split input into 2 regimes
if wj < 2.7403440668061758e-12
1. Initial program 13.1
  \[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}\]
2. Using strategy rm
3. Applied div-sub13.1
  \[\leadsto wj - \color{blue}{\left(\frac{wj \cdot e^{wj}}{e^{wj} + wj \cdot e^{wj}} - \frac{x}{e^{wj} + wj \cdot e^{wj}}\right)}\]
4. Applied associate--r-6.9
  \[\leadsto \color{blue}{\left(wj - \frac{wj \cdot e^{wj}}{e^{wj} + wj \cdot e^{wj}}\right) + \frac{x}{e^{wj} + wj \cdot e^{wj}}}\]
5. Taylor expanded around 0 0.2
  \[\leadsto \color{blue}{\left(\left({wj}^{2} + {wj}^{4}\right) - {wj}^{3}\right)} + \frac{x}{e^{wj} + wj \cdot e^{wj}}\]
6. Simplified0.2
  \[\leadsto \color{blue}{\left(\left(\left(wj \cdot wj\right) \cdot \left(wj \cdot wj\right) - \left(wj \cdot wj\right) \cdot wj\right) + wj \cdot wj\right)} + \frac{x}{e^{wj} + wj \cdot e^{wj}}\]
if 2.7403440668061758e-12 < wj
1. Initial program 23.9
  \[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}\]
2. Using strategy rm
3. Applied div-sub23.9
  \[\leadsto wj - \color{blue}{\left(\frac{wj \cdot e^{wj}}{e^{wj} + wj \cdot e^{wj}} - \frac{x}{e^{wj} + wj \cdot e^{wj}}\right)}\]
4. Applied associate--r-23.9
  \[\leadsto \color{blue}{\left(wj - \frac{wj \cdot e^{wj}}{e^{wj} + wj \cdot e^{wj}}\right) + \frac{x}{e^{wj} + wj \cdot e^{wj}}}\]
5. Using strategy rm
6. Applied flip3--23.9
  \[\leadsto \color{blue}{\frac{{wj}^{3} - {\left(\frac{wj \cdot e^{wj}}{e^{wj} + wj \cdot e^{wj}}\right)}^{3}}{wj \cdot wj + \left(\frac{wj \cdot e^{wj}}{e^{wj} + wj \cdot e^{wj}} \cdot \frac{wj \cdot e^{wj}}{e^{wj} + wj \cdot e^{wj}} + wj \cdot \frac{wj \cdot e^{wj}}{e^{wj} + wj \cdot e^{wj}}\right)}} + \frac{x}{e^{wj} + wj \cdot e^{wj}}\]
7. Simplified23.8
  \[\leadsto \frac{\color{blue}{\left(wj \cdot wj\right) \cdot wj - \frac{wj}{\frac{wj + 1}{1}} \cdot \left(\frac{wj}{\frac{wj + 1}{1}} \cdot \frac{wj}{\frac{wj + 1}{1}}\right)}}{wj \cdot wj + \left(\frac{wj \cdot e^{wj}}{e^{wj} + wj \cdot e^{wj}} \cdot \frac{wj \cdot e^{wj}}{e^{wj} + wj \cdot e^{wj}} + wj \cdot \frac{wj \cdot e^{wj}}{e^{wj} + wj \cdot e^{wj}}\right)} + \frac{x}{e^{wj} + wj \cdot e^{wj}}\]
8. Simplified5.5
  \[\leadsto \frac{\left(wj \cdot wj\right) \cdot wj - \frac{wj}{\frac{wj + 1}{1}} \cdot \left(\frac{wj}{\frac{wj + 1}{1}} \cdot \frac{wj}{\frac{wj + 1}{1}}\right)}{\color{blue}{\frac{wj}{\frac{wj + 1}{1}} \cdot \left(wj + \frac{wj}{\frac{wj + 1}{1}}\right) + wj \cdot wj}} + \frac{x}{e^{wj} + wj \cdot e^{wj}}\]
Recombined 2 regimes into one program.
Final simplification0.4
\[\leadsto \begin{array}{l} \mathbf{if}\;wj \le 2.7403440668061758 \cdot 10^{-12}:\\ \;\;\;\;\left(wj \cdot wj + \left(\left(wj \cdot wj\right) \cdot \left(wj \cdot wj\right) - \left(wj \cdot wj\right) \cdot wj\right)\right) + \frac{x}{e^{wj} \cdot wj + e^{wj}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\left(wj \cdot wj\right) \cdot wj - \left(\frac{wj}{1 + wj} \cdot \frac{wj}{1 + wj}\right) \cdot \frac{wj}{1 + wj}}{wj \cdot wj + \frac{wj}{1 + wj} \cdot \left(\frac{wj}{1 + wj} + wj\right)} + \frac{x}{e^{wj} \cdot wj + e^{wj}}\\ \end{array}\]

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

Error

Try it out

Target

Derivation

`if wj < 2.7403440668061758e-12`

`if 2.7403440668061758e-12 < wj`

Reproduce

In
Out