\[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}\;y \le -1.31950843774828536587285746565795386046 \cdot 10^{194}:\\ \;\;\;\;x + t \cdot z\\ \mathbf{elif}\;y \le 4.864775668665886217870966225595232577244 \cdot 10^{109}:\\ \;\;\;\;x + \left(\tanh \left(\frac{t}{y}\right) \cdot \left(y \cdot z\right) + \left(-\tanh \left(\frac{x}{y}\right)\right) \cdot \left(y \cdot z\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(y, z \cdot \left(\frac{\mathsf{expm1}\left(2 \cdot \frac{t}{y}\right)}{1 + e^{2 \cdot \frac{t}{y}}} - \tanh \left(\frac{x}{y}\right)\right), x\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}\;y \le -1.31950843774828536587285746565795386046 \cdot 10^{194}:\\
\;\;\;\;x + t \cdot z\\

\mathbf{elif}\;y \le 4.864775668665886217870966225595232577244 \cdot 10^{109}:\\
\;\;\;\;x + \left(\tanh \left(\frac{t}{y}\right) \cdot \left(y \cdot z\right) + \left(-\tanh \left(\frac{x}{y}\right)\right) \cdot \left(y \cdot z\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(y, z \cdot \left(\frac{\mathsf{expm1}\left(2 \cdot \frac{t}{y}\right)}{1 + e^{2 \cdot \frac{t}{y}}} - \tanh \left(\frac{x}{y}\right)\right), x\right)\\

\end{array}

double f(double x, double y, double z, double t) {
        double r185034 = x;
        double r185035 = y;
        double r185036 = z;
        double r185037 = r185035 * r185036;
        double r185038 = t;
        double r185039 = r185038 / r185035;
        double r185040 = tanh(r185039);
        double r185041 = r185034 / r185035;
        double r185042 = tanh(r185041);
        double r185043 = r185040 - r185042;
        double r185044 = r185037 * r185043;
        double r185045 = r185034 + r185044;
        return r185045;
}

↓

double f(double x, double y, double z, double t) {
        double r185046 = y;
        double r185047 = -1.3195084377482854e+194;
        bool r185048 = r185046 <= r185047;
        double r185049 = x;
        double r185050 = t;
        double r185051 = z;
        double r185052 = r185050 * r185051;
        double r185053 = r185049 + r185052;
        double r185054 = 4.864775668665886e+109;
        bool r185055 = r185046 <= r185054;
        double r185056 = r185050 / r185046;
        double r185057 = tanh(r185056);
        double r185058 = r185046 * r185051;
        double r185059 = r185057 * r185058;
        double r185060 = r185049 / r185046;
        double r185061 = tanh(r185060);
        double r185062 = -r185061;
        double r185063 = r185062 * r185058;
        double r185064 = r185059 + r185063;
        double r185065 = r185049 + r185064;
        double r185066 = 2.0;
        double r185067 = r185066 * r185056;
        double r185068 = expm1(r185067);
        double r185069 = 1.0;
        double r185070 = exp(r185067);
        double r185071 = r185069 + r185070;
        double r185072 = r185068 / r185071;
        double r185073 = r185072 - r185061;
        double r185074 = r185051 * r185073;
        double r185075 = fma(r185046, r185074, r185049);
        double r185076 = r185055 ? r185065 : r185075;
        double r185077 = r185048 ? r185053 : r185076;
        return r185077;
}

Original	4.2
Target	2.0
Herbie	3.6

Derivation

Split input into 3 regimes
if y < -1.3195084377482854e+194
1. Initial program 17.3
  \[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 sub-neg17.3
  \[\leadsto x + \left(y \cdot z\right) \cdot \color{blue}{\left(\tanh \left(\frac{t}{y}\right) + \left(-\tanh \left(\frac{x}{y}\right)\right)\right)}\]
4. Applied distribute-lft-in17.3
  \[\leadsto x + \color{blue}{\left(\left(y \cdot z\right) \cdot \tanh \left(\frac{t}{y}\right) + \left(y \cdot z\right) \cdot \left(-\tanh \left(\frac{x}{y}\right)\right)\right)}\]
5. Simplified17.3
  \[\leadsto x + \left(\color{blue}{\tanh \left(\frac{t}{y}\right) \cdot \left(y \cdot z\right)} + \left(y \cdot z\right) \cdot \left(-\tanh \left(\frac{x}{y}\right)\right)\right)\]
6. Simplified17.3
  \[\leadsto x + \left(\tanh \left(\frac{t}{y}\right) \cdot \left(y \cdot z\right) + \color{blue}{\left(-\tanh \left(\frac{x}{y}\right)\right) \cdot \left(y \cdot z\right)}\right)\]
7. Taylor expanded around 0 14.8
  \[\leadsto x + \color{blue}{t \cdot z}\]
if -1.3195084377482854e+194 < y < 4.864775668665886e+109
1. Initial program 1.3
  \[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 sub-neg1.3
  \[\leadsto x + \left(y \cdot z\right) \cdot \color{blue}{\left(\tanh \left(\frac{t}{y}\right) + \left(-\tanh \left(\frac{x}{y}\right)\right)\right)}\]
4. Applied distribute-lft-in1.3
  \[\leadsto x + \color{blue}{\left(\left(y \cdot z\right) \cdot \tanh \left(\frac{t}{y}\right) + \left(y \cdot z\right) \cdot \left(-\tanh \left(\frac{x}{y}\right)\right)\right)}\]
5. Simplified1.3
  \[\leadsto x + \left(\color{blue}{\tanh \left(\frac{t}{y}\right) \cdot \left(y \cdot z\right)} + \left(y \cdot z\right) \cdot \left(-\tanh \left(\frac{x}{y}\right)\right)\right)\]
6. Simplified1.3
  \[\leadsto x + \left(\tanh \left(\frac{t}{y}\right) \cdot \left(y \cdot z\right) + \color{blue}{\left(-\tanh \left(\frac{x}{y}\right)\right) \cdot \left(y \cdot z\right)}\right)\]
if 4.864775668665886e+109 < y
1. Initial program 13.5
  \[x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\]
2. Simplified6.6
  \[\leadsto \color{blue}{\mathsf{fma}\left(y, z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right), x\right)}\]
3. Using strategy rm
4. Applied tanh-def23.1
  \[\leadsto \mathsf{fma}\left(y, z \cdot \left(\color{blue}{\frac{e^{2 \cdot \frac{t}{y}} - 1}{e^{2 \cdot \frac{t}{y}} + 1}} - \tanh \left(\frac{x}{y}\right)\right), x\right)\]
5. Simplified10.3
  \[\leadsto \mathsf{fma}\left(y, z \cdot \left(\frac{\color{blue}{\mathsf{expm1}\left(2 \cdot \frac{t}{y}\right)}}{e^{2 \cdot \frac{t}{y}} + 1} - \tanh \left(\frac{x}{y}\right)\right), x\right)\]
6. Simplified10.3
  \[\leadsto \mathsf{fma}\left(y, z \cdot \left(\frac{\mathsf{expm1}\left(2 \cdot \frac{t}{y}\right)}{\color{blue}{1 + e^{2 \cdot \frac{t}{y}}}} - \tanh \left(\frac{x}{y}\right)\right), x\right)\]
Recombined 3 regimes into one program.
Final simplification3.6
\[\leadsto \begin{array}{l} \mathbf{if}\;y \le -1.31950843774828536587285746565795386046 \cdot 10^{194}:\\ \;\;\;\;x + t \cdot z\\ \mathbf{elif}\;y \le 4.864775668665886217870966225595232577244 \cdot 10^{109}:\\ \;\;\;\;x + \left(\tanh \left(\frac{t}{y}\right) \cdot \left(y \cdot z\right) + \left(-\tanh \left(\frac{x}{y}\right)\right) \cdot \left(y \cdot z\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(y, z \cdot \left(\frac{\mathsf{expm1}\left(2 \cdot \frac{t}{y}\right)}{1 + e^{2 \cdot \frac{t}{y}}} - \tanh \left(\frac{x}{y}\right)\right), x\right)\\ \end{array}\]

Error

Target

Derivation

`if y < -1.3195084377482854e+194`

`if -1.3195084377482854e+194 < y < 4.864775668665886e+109`

`if 4.864775668665886e+109 < y`

Reproduce