\[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 r168862 = x;
        double r168863 = y;
        double r168864 = z;
        double r168865 = r168863 * r168864;
        double r168866 = t;
        double r168867 = r168866 / r168863;
        double r168868 = tanh(r168867);
        double r168869 = r168862 / r168863;
        double r168870 = tanh(r168869);
        double r168871 = r168868 - r168870;
        double r168872 = r168865 * r168871;
        double r168873 = r168862 + r168872;
        return r168873;
}

↓

double f(double x, double y, double z, double t) {
        double r168874 = y;
        double r168875 = -1.3195084377482854e+194;
        bool r168876 = r168874 <= r168875;
        double r168877 = x;
        double r168878 = t;
        double r168879 = z;
        double r168880 = r168878 * r168879;
        double r168881 = r168877 + r168880;
        double r168882 = 4.864775668665886e+109;
        bool r168883 = r168874 <= r168882;
        double r168884 = r168878 / r168874;
        double r168885 = tanh(r168884);
        double r168886 = r168874 * r168879;
        double r168887 = r168885 * r168886;
        double r168888 = r168877 / r168874;
        double r168889 = tanh(r168888);
        double r168890 = -r168889;
        double r168891 = r168890 * r168886;
        double r168892 = r168887 + r168891;
        double r168893 = r168877 + r168892;
        double r168894 = 2.0;
        double r168895 = r168894 * r168884;
        double r168896 = expm1(r168895);
        double r168897 = 1.0;
        double r168898 = exp(r168895);
        double r168899 = r168897 + r168898;
        double r168900 = r168896 / r168899;
        double r168901 = r168900 - r168889;
        double r168902 = r168879 * r168901;
        double r168903 = fma(r168874, r168902, r168877);
        double r168904 = r168883 ? r168893 : r168903;
        double r168905 = r168876 ? r168881 : r168904;
        return r168905;
}

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