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

↓

\[\begin{array}{l} \mathbf{if}\;wj \le 5.3258678519809691 \cdot 10^{-17}:\\ \;\;\;\;\left(x + {wj}^{2}\right) - 2 \cdot \left(wj \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{wj \cdot \left(\frac{\frac{x}{wj + 1}}{e^{wj}} \cdot \frac{\frac{x}{wj + 1}}{e^{wj}} - wj \cdot wj\right) + \left(1 \cdot \left(\frac{\frac{x}{wj + 1}}{e^{wj}} \cdot \frac{\frac{x}{wj + 1}}{e^{wj}} - wj \cdot wj\right) - \left(\frac{\frac{x}{wj + 1}}{e^{wj}} - wj\right) \cdot wj\right)}{\left(\frac{\frac{x}{wj + 1}}{e^{wj}} - wj\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 5.3258678519809691 \cdot 10^{-17}:\\
\;\;\;\;\left(x + {wj}^{2}\right) - 2 \cdot \left(wj \cdot x\right)\\

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

\end{array}

double f(double wj, double x) {
        double r391143 = wj;
        double r391144 = exp(r391143);
        double r391145 = r391143 * r391144;
        double r391146 = x;
        double r391147 = r391145 - r391146;
        double r391148 = r391144 + r391145;
        double r391149 = r391147 / r391148;
        double r391150 = r391143 - r391149;
        return r391150;
}

↓

double f(double wj, double x) {
        double r391151 = wj;
        double r391152 = 5.325867851980969e-17;
        bool r391153 = r391151 <= r391152;
        double r391154 = x;
        double r391155 = 2.0;
        double r391156 = pow(r391151, r391155);
        double r391157 = r391154 + r391156;
        double r391158 = r391151 * r391154;
        double r391159 = r391155 * r391158;
        double r391160 = r391157 - r391159;
        double r391161 = 1.0;
        double r391162 = r391151 + r391161;
        double r391163 = r391154 / r391162;
        double r391164 = exp(r391151);
        double r391165 = r391163 / r391164;
        double r391166 = r391165 * r391165;
        double r391167 = r391151 * r391151;
        double r391168 = r391166 - r391167;
        double r391169 = r391151 * r391168;
        double r391170 = r391161 * r391168;
        double r391171 = r391165 - r391151;
        double r391172 = r391171 * r391151;
        double r391173 = r391170 - r391172;
        double r391174 = r391169 + r391173;
        double r391175 = r391171 * r391162;
        double r391176 = r391174 / r391175;
        double r391177 = r391153 ? r391160 : r391176;
        return r391177;
}

Original	13.7
Target	13.1
Herbie	1.2

Derivation

Split input into 2 regimes
if wj < 5.325867851980969e-17
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.8
  \[\leadsto \color{blue}{\left(x + {wj}^{2}\right) - 2 \cdot \left(wj \cdot x\right)}\]
if 5.325867851980969e-17 < wj
1. Initial program 24.5
  \[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}\]
2. Simplified7.3
  \[\leadsto \color{blue}{\left(\frac{\frac{x}{wj + 1}}{e^{wj}} + wj\right) - \frac{wj}{wj + 1}}\]
3. Using strategy rm
4. Applied flip-+16.8
  \[\leadsto \color{blue}{\frac{\frac{\frac{x}{wj + 1}}{e^{wj}} \cdot \frac{\frac{x}{wj + 1}}{e^{wj}} - wj \cdot wj}{\frac{\frac{x}{wj + 1}}{e^{wj}} - wj}} - \frac{wj}{wj + 1}\]
5. Applied frac-sub17.0
  \[\leadsto \color{blue}{\frac{\left(\frac{\frac{x}{wj + 1}}{e^{wj}} \cdot \frac{\frac{x}{wj + 1}}{e^{wj}} - wj \cdot wj\right) \cdot \left(wj + 1\right) - \left(\frac{\frac{x}{wj + 1}}{e^{wj}} - wj\right) \cdot wj}{\left(\frac{\frac{x}{wj + 1}}{e^{wj}} - wj\right) \cdot \left(wj + 1\right)}}\]
6. Using strategy rm
7. Applied distribute-rgt-in16.8
  \[\leadsto \frac{\color{blue}{\left(wj \cdot \left(\frac{\frac{x}{wj + 1}}{e^{wj}} \cdot \frac{\frac{x}{wj + 1}}{e^{wj}} - wj \cdot wj\right) + 1 \cdot \left(\frac{\frac{x}{wj + 1}}{e^{wj}} \cdot \frac{\frac{x}{wj + 1}}{e^{wj}} - wj \cdot wj\right)\right)} - \left(\frac{\frac{x}{wj + 1}}{e^{wj}} - wj\right) \cdot wj}{\left(\frac{\frac{x}{wj + 1}}{e^{wj}} - wj\right) \cdot \left(wj + 1\right)}\]
8. Applied associate--l+10.7
  \[\leadsto \frac{\color{blue}{wj \cdot \left(\frac{\frac{x}{wj + 1}}{e^{wj}} \cdot \frac{\frac{x}{wj + 1}}{e^{wj}} - wj \cdot wj\right) + \left(1 \cdot \left(\frac{\frac{x}{wj + 1}}{e^{wj}} \cdot \frac{\frac{x}{wj + 1}}{e^{wj}} - wj \cdot wj\right) - \left(\frac{\frac{x}{wj + 1}}{e^{wj}} - wj\right) \cdot wj\right)}}{\left(\frac{\frac{x}{wj + 1}}{e^{wj}} - wj\right) \cdot \left(wj + 1\right)}\]
Recombined 2 regimes into one program.
Final simplification1.2
\[\leadsto \begin{array}{l} \mathbf{if}\;wj \le 5.3258678519809691 \cdot 10^{-17}:\\ \;\;\;\;\left(x + {wj}^{2}\right) - 2 \cdot \left(wj \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{wj \cdot \left(\frac{\frac{x}{wj + 1}}{e^{wj}} \cdot \frac{\frac{x}{wj + 1}}{e^{wj}} - wj \cdot wj\right) + \left(1 \cdot \left(\frac{\frac{x}{wj + 1}}{e^{wj}} \cdot \frac{\frac{x}{wj + 1}}{e^{wj}} - wj \cdot wj\right) - \left(\frac{\frac{x}{wj + 1}}{e^{wj}} - wj\right) \cdot wj\right)}{\left(\frac{\frac{x}{wj + 1}}{e^{wj}} - wj\right) \cdot \left(wj + 1\right)}\\ \end{array}\]

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

Error

Try it out

Target

Derivation

`if wj < 5.325867851980969e-17`

`if 5.325867851980969e-17 < wj`

Reproduce

In
Out