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

↓

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

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

↓

\begin{array}{l}
\mathbf{if}\;wj \le 2.32999755055536264 \cdot 10^{-7}:\\
\;\;\;\;\left(x + {wj}^{2}\right) - 2 \cdot \left(wj \cdot x\right)\\

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

\end{array}

double f(double wj, double x) {
        double r242661 = wj;
        double r242662 = exp(r242661);
        double r242663 = r242661 * r242662;
        double r242664 = x;
        double r242665 = r242663 - r242664;
        double r242666 = r242662 + r242663;
        double r242667 = r242665 / r242666;
        double r242668 = r242661 - r242667;
        return r242668;
}

↓

double f(double wj, double x) {
        double r242669 = wj;
        double r242670 = 2.3299975505553626e-07;
        bool r242671 = r242669 <= r242670;
        double r242672 = x;
        double r242673 = 2.0;
        double r242674 = pow(r242669, r242673);
        double r242675 = r242672 + r242674;
        double r242676 = r242669 * r242672;
        double r242677 = r242673 * r242676;
        double r242678 = r242675 - r242677;
        double r242679 = -r242669;
        double r242680 = r242669 + r242669;
        double r242681 = exp(r242680);
        double r242682 = r242672 / r242681;
        double r242683 = 1.0;
        double r242684 = r242669 + r242683;
        double r242685 = r242684 * r242684;
        double r242686 = r242672 / r242685;
        double r242687 = exp(r242669);
        double r242688 = r242687 * r242684;
        double r242689 = r242672 / r242688;
        double r242690 = r242669 - r242689;
        double r242691 = r242669 * r242690;
        double r242692 = fma(r242682, r242686, r242691);
        double r242693 = 3.0;
        double r242694 = pow(r242689, r242693);
        double r242695 = pow(r242669, r242693);
        double r242696 = r242694 + r242695;
        double r242697 = r242696 * r242684;
        double r242698 = fma(r242679, r242692, r242697);
        double r242699 = r242689 * r242689;
        double r242700 = fma(r242669, r242690, r242699);
        double r242701 = r242700 * r242684;
        double r242702 = r242698 / r242701;
        double r242703 = r242671 ? r242678 : r242702;
        return r242703;
}

Original	13.6
Target	13.0
Herbie	1.3

Derivation

Split input into 2 regimes
if wj < 2.3299975505553626e-07
1. Initial program 13.3
  \[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}\]
2. Simplified13.3
  \[\leadsto \color{blue}{\left(\frac{\frac{x}{wj + 1}}{e^{wj}} + wj\right) - \frac{wj}{wj + 1}}\]
3. Taylor expanded around 0 0.9
  \[\leadsto \color{blue}{\left(x + {wj}^{2}\right) - 2 \cdot \left(wj \cdot x\right)}\]
if 2.3299975505553626e-07 < wj
1. Initial program 25.7
  \[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}\]
2. Simplified2.2
  \[\leadsto \color{blue}{\left(\frac{\frac{x}{wj + 1}}{e^{wj}} + wj\right) - \frac{wj}{wj + 1}}\]
3. Using strategy rm
4. Applied div-inv2.2
  \[\leadsto \left(\frac{\color{blue}{x \cdot \frac{1}{wj + 1}}}{e^{wj}} + wj\right) - \frac{wj}{wj + 1}\]
5. Applied associate-/l*2.2
  \[\leadsto \left(\color{blue}{\frac{x}{\frac{e^{wj}}{\frac{1}{wj + 1}}}} + wj\right) - \frac{wj}{wj + 1}\]
6. Simplified2.2
  \[\leadsto \left(\frac{x}{\color{blue}{e^{wj} \cdot \left(wj + 1\right)}} + wj\right) - \frac{wj}{wj + 1}\]
7. Using strategy rm
8. Applied flip3-+16.9
  \[\leadsto \color{blue}{\frac{{\left(\frac{x}{e^{wj} \cdot \left(wj + 1\right)}\right)}^{3} + {wj}^{3}}{\frac{x}{e^{wj} \cdot \left(wj + 1\right)} \cdot \frac{x}{e^{wj} \cdot \left(wj + 1\right)} + \left(wj \cdot wj - \frac{x}{e^{wj} \cdot \left(wj + 1\right)} \cdot wj\right)}} - \frac{wj}{wj + 1}\]
9. Applied frac-sub17.0
  \[\leadsto \color{blue}{\frac{\left({\left(\frac{x}{e^{wj} \cdot \left(wj + 1\right)}\right)}^{3} + {wj}^{3}\right) \cdot \left(wj + 1\right) - \left(\frac{x}{e^{wj} \cdot \left(wj + 1\right)} \cdot \frac{x}{e^{wj} \cdot \left(wj + 1\right)} + \left(wj \cdot wj - \frac{x}{e^{wj} \cdot \left(wj + 1\right)} \cdot wj\right)\right) \cdot wj}{\left(\frac{x}{e^{wj} \cdot \left(wj + 1\right)} \cdot \frac{x}{e^{wj} \cdot \left(wj + 1\right)} + \left(wj \cdot wj - \frac{x}{e^{wj} \cdot \left(wj + 1\right)} \cdot wj\right)\right) \cdot \left(wj + 1\right)}}\]
10. Simplified16.9
  \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(-wj, \mathsf{fma}\left(\frac{x}{e^{wj + wj}}, \frac{x}{\left(wj + 1\right) \cdot \left(wj + 1\right)}, wj \cdot \left(wj - \frac{x}{e^{wj} \cdot \left(wj + 1\right)}\right)\right), \left({\left(\frac{x}{e^{wj} \cdot \left(wj + 1\right)}\right)}^{3} + {wj}^{3}\right) \cdot \left(wj + 1\right)\right)}}{\left(\frac{x}{e^{wj} \cdot \left(wj + 1\right)} \cdot \frac{x}{e^{wj} \cdot \left(wj + 1\right)} + \left(wj \cdot wj - \frac{x}{e^{wj} \cdot \left(wj + 1\right)} \cdot wj\right)\right) \cdot \left(wj + 1\right)}\]
11. Simplified16.9
  \[\leadsto \frac{\mathsf{fma}\left(-wj, \mathsf{fma}\left(\frac{x}{e^{wj + wj}}, \frac{x}{\left(wj + 1\right) \cdot \left(wj + 1\right)}, wj \cdot \left(wj - \frac{x}{e^{wj} \cdot \left(wj + 1\right)}\right)\right), \left({\left(\frac{x}{e^{wj} \cdot \left(wj + 1\right)}\right)}^{3} + {wj}^{3}\right) \cdot \left(wj + 1\right)\right)}{\color{blue}{\mathsf{fma}\left(wj, wj - \frac{x}{e^{wj} \cdot \left(wj + 1\right)}, \frac{x}{e^{wj} \cdot \left(wj + 1\right)} \cdot \frac{x}{e^{wj} \cdot \left(wj + 1\right)}\right) \cdot \left(wj + 1\right)}}\]
Recombined 2 regimes into one program.
Final simplification1.3
\[\leadsto \begin{array}{l} \mathbf{if}\;wj \le 2.32999755055536264 \cdot 10^{-7}:\\ \;\;\;\;\left(x + {wj}^{2}\right) - 2 \cdot \left(wj \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\mathsf{fma}\left(-wj, \mathsf{fma}\left(\frac{x}{e^{wj + wj}}, \frac{x}{\left(wj + 1\right) \cdot \left(wj + 1\right)}, wj \cdot \left(wj - \frac{x}{e^{wj} \cdot \left(wj + 1\right)}\right)\right), \left({\left(\frac{x}{e^{wj} \cdot \left(wj + 1\right)}\right)}^{3} + {wj}^{3}\right) \cdot \left(wj + 1\right)\right)}{\mathsf{fma}\left(wj, wj - \frac{x}{e^{wj} \cdot \left(wj + 1\right)}, \frac{x}{e^{wj} \cdot \left(wj + 1\right)} \cdot \frac{x}{e^{wj} \cdot \left(wj + 1\right)}\right) \cdot \left(wj + 1\right)}\\ \end{array}\]

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

Error

Target

Derivation

`if wj < 2.3299975505553626e-07`

`if 2.3299975505553626e-07 < wj`

Reproduce