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

↓

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

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

↓

\begin{array}{l}
\mathbf{if}\;wj \le 5.490304900382047 \cdot 10^{-09}:\\
\;\;\;\;\mathsf{fma}\left(wj, wj, x\right) - x \cdot \left(wj + wj\right)\\

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

\end{array}

double f(double wj, double x) {
        double r3975564 = wj;
        double r3975565 = exp(r3975564);
        double r3975566 = r3975564 * r3975565;
        double r3975567 = x;
        double r3975568 = r3975566 - r3975567;
        double r3975569 = r3975565 + r3975566;
        double r3975570 = r3975568 / r3975569;
        double r3975571 = r3975564 - r3975570;
        return r3975571;
}

↓

double f(double wj, double x) {
        double r3975572 = wj;
        double r3975573 = 5.490304900382047e-09;
        bool r3975574 = r3975572 <= r3975573;
        double r3975575 = x;
        double r3975576 = fma(r3975572, r3975572, r3975575);
        double r3975577 = r3975572 + r3975572;
        double r3975578 = r3975575 * r3975577;
        double r3975579 = r3975576 - r3975578;
        double r3975580 = 1.0;
        double r3975581 = r3975572 + r3975580;
        double r3975582 = r3975580 / r3975581;
        double r3975583 = exp(r3975572);
        double r3975584 = r3975583 * r3975572;
        double r3975585 = r3975584 - r3975575;
        double r3975586 = r3975583 / r3975585;
        double r3975587 = r3975580 / r3975586;
        double r3975588 = r3975582 * r3975587;
        double r3975589 = r3975572 - r3975588;
        double r3975590 = r3975574 ? r3975579 : r3975589;
        return r3975590;
}

Original	13.9
Target	13.2
Herbie	1.6

Derivation

Split input into 2 regimes
if wj < 5.490304900382047e-09
1. Initial program 13.6
  \[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}\]
2. Taylor expanded around 0 0.8
  \[\leadsto \color{blue}{\left({wj}^{2} + x\right) - 2 \cdot \left(x \cdot wj\right)}\]
3. Simplified0.8
  \[\leadsto \color{blue}{\mathsf{fma}\left(wj, wj, x\right) - \left(wj + wj\right) \cdot x}\]
if 5.490304900382047e-09 < wj
1. Initial program 25.5
  \[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}\]
2. Using strategy rm
3. Applied clear-num25.6
  \[\leadsto wj - \color{blue}{\frac{1}{\frac{e^{wj} + wj \cdot e^{wj}}{wj \cdot e^{wj} - x}}}\]
4. Using strategy rm
5. Applied *-un-lft-identity25.6
  \[\leadsto wj - \frac{1}{\frac{e^{wj} + wj \cdot e^{wj}}{\color{blue}{1 \cdot \left(wj \cdot e^{wj} - x\right)}}}\]
6. Applied distribute-rgt1-in25.7
  \[\leadsto wj - \frac{1}{\frac{\color{blue}{\left(wj + 1\right) \cdot e^{wj}}}{1 \cdot \left(wj \cdot e^{wj} - x\right)}}\]
7. Applied times-frac25.6
  \[\leadsto wj - \frac{1}{\color{blue}{\frac{wj + 1}{1} \cdot \frac{e^{wj}}{wj \cdot e^{wj} - x}}}\]
8. Applied *-un-lft-identity25.6
  \[\leadsto wj - \frac{\color{blue}{1 \cdot 1}}{\frac{wj + 1}{1} \cdot \frac{e^{wj}}{wj \cdot e^{wj} - x}}\]
9. Applied times-frac25.8
  \[\leadsto wj - \color{blue}{\frac{1}{\frac{wj + 1}{1}} \cdot \frac{1}{\frac{e^{wj}}{wj \cdot e^{wj} - x}}}\]
10. Simplified25.8
  \[\leadsto wj - \color{blue}{\frac{1}{wj + 1}} \cdot \frac{1}{\frac{e^{wj}}{wj \cdot e^{wj} - x}}\]
Recombined 2 regimes into one program.
Final simplification1.6
\[\leadsto \begin{array}{l} \mathbf{if}\;wj \le 5.490304900382047 \cdot 10^{-09}:\\ \;\;\;\;\mathsf{fma}\left(wj, wj, x\right) - x \cdot \left(wj + wj\right)\\ \mathbf{else}:\\ \;\;\;\;wj - \frac{1}{wj + 1} \cdot \frac{1}{\frac{e^{wj}}{e^{wj} \cdot wj - x}}\\ \end{array}\]

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

Error

Target

Derivation

`if wj < 5.490304900382047e-09`

`if 5.490304900382047e-09 < wj`

Reproduce