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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -2.434590503365394746264295962158752554615 \cdot 10^{-105} \lor \neg \left(x \le 7.260560867012781601958578499631114620962 \cdot 10^{-116}\right):\\ \;\;\;\;\left(wj - \frac{wj - \frac{x}{e^{wj}}}{{wj}^{3} + 1}\right) - \left(wj \cdot wj - wj\right) \cdot \frac{wj - \frac{x}{e^{wj}}}{1 + {wj}^{3}}\\ \mathbf{else}:\\ \;\;\;\;\left(x + {wj}^{2}\right) - \log \left(e^{2 \cdot \left(wj \cdot x\right)}\right)\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;x \le -2.434590503365394746264295962158752554615 \cdot 10^{-105} \lor \neg \left(x \le 7.260560867012781601958578499631114620962 \cdot 10^{-116}\right):\\
\;\;\;\;\left(wj - \frac{wj - \frac{x}{e^{wj}}}{{wj}^{3} + 1}\right) - \left(wj \cdot wj - wj\right) \cdot \frac{wj - \frac{x}{e^{wj}}}{1 + {wj}^{3}}\\

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

\end{array}

double f(double wj, double x) {
        double r127831 = wj;
        double r127832 = exp(r127831);
        double r127833 = r127831 * r127832;
        double r127834 = x;
        double r127835 = r127833 - r127834;
        double r127836 = r127832 + r127833;
        double r127837 = r127835 / r127836;
        double r127838 = r127831 - r127837;
        return r127838;
}

↓

double f(double wj, double x) {
        double r127839 = x;
        double r127840 = -2.4345905033653947e-105;
        bool r127841 = r127839 <= r127840;
        double r127842 = 7.260560867012782e-116;
        bool r127843 = r127839 <= r127842;
        double r127844 = !r127843;
        bool r127845 = r127841 || r127844;
        double r127846 = wj;
        double r127847 = exp(r127846);
        double r127848 = r127839 / r127847;
        double r127849 = r127846 - r127848;
        double r127850 = 3.0;
        double r127851 = pow(r127846, r127850);
        double r127852 = 1.0;
        double r127853 = r127851 + r127852;
        double r127854 = r127849 / r127853;
        double r127855 = r127846 - r127854;
        double r127856 = r127846 * r127846;
        double r127857 = r127856 - r127846;
        double r127858 = r127852 + r127851;
        double r127859 = r127849 / r127858;
        double r127860 = r127857 * r127859;
        double r127861 = r127855 - r127860;
        double r127862 = 2.0;
        double r127863 = pow(r127846, r127862);
        double r127864 = r127839 + r127863;
        double r127865 = r127846 * r127839;
        double r127866 = r127862 * r127865;
        double r127867 = exp(r127866);
        double r127868 = log(r127867);
        double r127869 = r127864 - r127868;
        double r127870 = r127845 ? r127861 : r127869;
        return r127870;
}

Original	13.6
Target	13.1
Herbie	1.7

Derivation

Split input into 2 regimes
if x < -2.4345905033653947e-105 or 7.260560867012782e-116 < x
1. Initial program 2.5
  \[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}\]
2. Simplified1.9
  \[\leadsto \color{blue}{wj - \frac{\frac{wj}{1} - \frac{x}{e^{wj}}}{1 + wj}}\]
3. Using strategy rm
4. Applied flip3-+1.9
  \[\leadsto wj - \frac{\frac{wj}{1} - \frac{x}{e^{wj}}}{\color{blue}{\frac{{1}^{3} + {wj}^{3}}{1 \cdot 1 + \left(wj \cdot wj - 1 \cdot wj\right)}}}\]
5. Applied associate-/r/1.9
  \[\leadsto wj - \color{blue}{\frac{\frac{wj}{1} - \frac{x}{e^{wj}}}{{1}^{3} + {wj}^{3}} \cdot \left(1 \cdot 1 + \left(wj \cdot wj - 1 \cdot wj\right)\right)}\]
6. Simplified1.9
  \[\leadsto wj - \color{blue}{\frac{wj - \frac{x}{e^{wj}}}{1 + {wj}^{3}}} \cdot \left(1 \cdot 1 + \left(wj \cdot wj - 1 \cdot wj\right)\right)\]
7. Using strategy rm
8. Applied distribute-rgt-in1.9
  \[\leadsto wj - \color{blue}{\left(\left(1 \cdot 1\right) \cdot \frac{wj - \frac{x}{e^{wj}}}{1 + {wj}^{3}} + \left(wj \cdot wj - 1 \cdot wj\right) \cdot \frac{wj - \frac{x}{e^{wj}}}{1 + {wj}^{3}}\right)}\]
9. Applied associate--r+1.2
  \[\leadsto \color{blue}{\left(wj - \left(1 \cdot 1\right) \cdot \frac{wj - \frac{x}{e^{wj}}}{1 + {wj}^{3}}\right) - \left(wj \cdot wj - 1 \cdot wj\right) \cdot \frac{wj - \frac{x}{e^{wj}}}{1 + {wj}^{3}}}\]
10. Simplified1.2
  \[\leadsto \color{blue}{\left(wj - \frac{wj - \frac{x}{e^{wj}}}{{wj}^{3} + 1}\right)} - \left(wj \cdot wj - 1 \cdot wj\right) \cdot \frac{wj - \frac{x}{e^{wj}}}{1 + {wj}^{3}}\]
if -2.4345905033653947e-105 < x < 7.260560867012782e-116
1. Initial program 37.5
  \[wj - \frac{wj \cdot e^{wj} - x}{e^{wj} + wj \cdot e^{wj}}\]
2. Simplified37.0
  \[\leadsto \color{blue}{wj - \frac{\frac{wj}{1} - \frac{x}{e^{wj}}}{1 + wj}}\]
3. Taylor expanded around 0 2.6
  \[\leadsto \color{blue}{\left(x + {wj}^{2}\right) - 2 \cdot \left(wj \cdot x\right)}\]
4. Using strategy rm
5. Applied add-log-exp2.6
  \[\leadsto \left(x + {wj}^{2}\right) - \color{blue}{\log \left(e^{2 \cdot \left(wj \cdot x\right)}\right)}\]
Recombined 2 regimes into one program.
Final simplification1.7
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -2.434590503365394746264295962158752554615 \cdot 10^{-105} \lor \neg \left(x \le 7.260560867012781601958578499631114620962 \cdot 10^{-116}\right):\\ \;\;\;\;\left(wj - \frac{wj - \frac{x}{e^{wj}}}{{wj}^{3} + 1}\right) - \left(wj \cdot wj - wj\right) \cdot \frac{wj - \frac{x}{e^{wj}}}{1 + {wj}^{3}}\\ \mathbf{else}:\\ \;\;\;\;\left(x + {wj}^{2}\right) - \log \left(e^{2 \cdot \left(wj \cdot x\right)}\right)\\ \end{array}\]

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

Error

Try it out

Target

Derivation

`if x < -2.4345905033653947e-105 or 7.260560867012782e-116 < x`

`if -2.4345905033653947e-105 < x < 7.260560867012782e-116`

Reproduce

In
Out