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

↓

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

double f(double wj, double x) {
        double r28399293 = wj;
        double r28399294 = exp(r28399293);
        double r28399295 = r28399293 * r28399294;
        double r28399296 = x;
        double r28399297 = r28399295 - r28399296;
        double r28399298 = r28399294 + r28399295;
        double r28399299 = r28399297 / r28399298;
        double r28399300 = r28399293 - r28399299;
        return r28399300;
}

↓

double f(double wj, double x) {
        double r28399301 = wj;
        double r28399302 = 6.5296151305606205e-09;
        bool r28399303 = r28399301 <= r28399302;
        double r28399304 = x;
        double r28399305 = -2.0;
        double r28399306 = r28399304 * r28399305;
        double r28399307 = r28399306 + r28399301;
        double r28399308 = r28399301 * r28399307;
        double r28399309 = r28399304 + r28399308;
        double r28399310 = exp(r28399301);
        double r28399311 = r28399304 / r28399310;
        double r28399312 = r28399301 - r28399311;
        double r28399313 = 1.0;
        double r28399314 = r28399301 + r28399313;
        double r28399315 = r28399313 / r28399314;
        double r28399316 = r28399312 * r28399315;
        double r28399317 = r28399301 - r28399316;
        double r28399318 = r28399303 ? r28399309 : r28399317;
        return r28399318;
}

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

↓

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

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

\end{array}

Original	13.4
Target	12.8
Herbie	1.0

Derivation

Split input into 2 regimes
if wj < 6.5296151305606205e-09
1. Initial program 13.1
  \[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}\]
2. Taylor expanded around 0 0.9
  \[\leadsto \color{blue}{\left({wj}^{2} + x\right) - 2 \cdot \left(x \cdot wj\right)}\]
3. Simplified0.9
  \[\leadsto \color{blue}{x + \left(wj + -2 \cdot x\right) \cdot wj}\]
if 6.5296151305606205e-09 < wj
1. Initial program 24.8
  \[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}\]
2. Using strategy rm
3. Applied distribute-rgt1-in25.0
  \[\leadsto wj - \frac{wj \cdot e^{wj} - x}{\color{blue}{\left(wj + 1\right) \cdot e^{wj}}}\]
4. Applied *-un-lft-identity25.0
  \[\leadsto wj - \frac{\color{blue}{1 \cdot \left(wj \cdot e^{wj} - x\right)}}{\left(wj + 1\right) \cdot e^{wj}}\]
5. Applied times-frac24.9
  \[\leadsto wj - \color{blue}{\frac{1}{wj + 1} \cdot \frac{wj \cdot e^{wj} - x}{e^{wj}}}\]
6. Simplified3.1
  \[\leadsto wj - \frac{1}{wj + 1} \cdot \color{blue}{\left(wj - \frac{x}{e^{wj}}\right)}\]
Recombined 2 regimes into one program.
Final simplification1.0
\[\leadsto \begin{array}{l} \mathbf{if}\;wj \le 6.5296151305606205 \cdot 10^{-09}:\\ \;\;\;\;x + wj \cdot \left(x \cdot -2 + wj\right)\\ \mathbf{else}:\\ \;\;\;\;wj - \left(wj - \frac{x}{e^{wj}}\right) \cdot \frac{1}{wj + 1}\\ \end{array}\]

Reproduce

herbie shell --seed 2019102 
(FPCore (wj x)
  :name "Jmat.Real.lambertw, newton loop step"

  :herbie-target
  (- wj (- (/ wj (+ wj 1)) (/ x (+ (exp wj) (* wj (exp wj))))))

  (- wj (/ (- (* wj (exp wj)) x) (+ (exp wj) (* wj (exp wj))))))

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

Error

Target

Derivation

`if wj < 6.5296151305606205e-09`

`if 6.5296151305606205e-09 < wj`

Reproduce