\[x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\]

↓

\[\begin{array}{l} \mathbf{if}\;z \le -9.4676289022626253 \cdot 10^{51} \lor \neg \left(z \le 1.15973460810036978 \cdot 10^{-120}\right):\\ \;\;\;\;x + y \cdot \left(z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - {\left(\tanh \left(\frac{x}{y}\right)\right)}^{1}\right)\\ \end{array}\]

x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)

↓

\begin{array}{l}
\mathbf{if}\;z \le -9.4676289022626253 \cdot 10^{51} \lor \neg \left(z \le 1.15973460810036978 \cdot 10^{-120}\right):\\
\;\;\;\;x + y \cdot \left(z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\right)\\

\mathbf{else}:\\
\;\;\;\;x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - {\left(\tanh \left(\frac{x}{y}\right)\right)}^{1}\right)\\

\end{array}

double f(double x, double y, double z, double t) {
        double r343370 = x;
        double r343371 = y;
        double r343372 = z;
        double r343373 = r343371 * r343372;
        double r343374 = t;
        double r343375 = r343374 / r343371;
        double r343376 = tanh(r343375);
        double r343377 = r343370 / r343371;
        double r343378 = tanh(r343377);
        double r343379 = r343376 - r343378;
        double r343380 = r343373 * r343379;
        double r343381 = r343370 + r343380;
        return r343381;
}

↓

double f(double x, double y, double z, double t) {
        double r343382 = z;
        double r343383 = -9.467628902262625e+51;
        bool r343384 = r343382 <= r343383;
        double r343385 = 1.1597346081003698e-120;
        bool r343386 = r343382 <= r343385;
        double r343387 = !r343386;
        bool r343388 = r343384 || r343387;
        double r343389 = x;
        double r343390 = y;
        double r343391 = t;
        double r343392 = r343391 / r343390;
        double r343393 = tanh(r343392);
        double r343394 = r343389 / r343390;
        double r343395 = tanh(r343394);
        double r343396 = r343393 - r343395;
        double r343397 = r343382 * r343396;
        double r343398 = r343390 * r343397;
        double r343399 = r343389 + r343398;
        double r343400 = r343390 * r343382;
        double r343401 = 1.0;
        double r343402 = pow(r343395, r343401);
        double r343403 = r343393 - r343402;
        double r343404 = r343400 * r343403;
        double r343405 = r343389 + r343404;
        double r343406 = r343388 ? r343399 : r343405;
        return r343406;
}

Original	4.7
Target	2.1
Herbie	1.7

Derivation

Split input into 2 regimes
if z < -9.467628902262625e+51 or 1.1597346081003698e-120 < z
1. Initial program 8.4
  \[x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\]
2. Using strategy rm
3. Applied associate-*l*2.7
  \[\leadsto x + \color{blue}{y \cdot \left(z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\right)}\]
if -9.467628902262625e+51 < z < 1.1597346081003698e-120
1. Initial program 0.5
  \[x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\]
2. Using strategy rm
3. Applied pow10.5
  \[\leadsto x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \color{blue}{{\left(\tanh \left(\frac{x}{y}\right)\right)}^{1}}\right)\]
Recombined 2 regimes into one program.
Final simplification1.7
\[\leadsto \begin{array}{l} \mathbf{if}\;z \le -9.4676289022626253 \cdot 10^{51} \lor \neg \left(z \le 1.15973460810036978 \cdot 10^{-120}\right):\\ \;\;\;\;x + y \cdot \left(z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - {\left(\tanh \left(\frac{x}{y}\right)\right)}^{1}\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if z < -9.467628902262625e+51 or 1.1597346081003698e-120 < z`

`if -9.467628902262625e+51 < z < 1.1597346081003698e-120`

Reproduce

In
Out