\[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 -6.6977993073618858 \cdot 10^{216}:\\ \;\;\;\;\mathsf{fma}\left(z, t, x - x \cdot z\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(y, z \cdot \tanh \left(\frac{t}{y}\right) + z \cdot \left(-\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 -6.6977993073618858 \cdot 10^{216}:\\
\;\;\;\;\mathsf{fma}\left(z, t, x - x \cdot z\right)\\

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

\end{array}

double f(double x, double y, double z, double t) {
        double r255166 = x;
        double r255167 = y;
        double r255168 = z;
        double r255169 = r255167 * r255168;
        double r255170 = t;
        double r255171 = r255170 / r255167;
        double r255172 = tanh(r255171);
        double r255173 = r255166 / r255167;
        double r255174 = tanh(r255173);
        double r255175 = r255172 - r255174;
        double r255176 = r255169 * r255175;
        double r255177 = r255166 + r255176;
        return r255177;
}

↓

double f(double x, double y, double z, double t) {
        double r255178 = y;
        double r255179 = -6.697799307361886e+216;
        bool r255180 = r255178 <= r255179;
        double r255181 = z;
        double r255182 = t;
        double r255183 = x;
        double r255184 = r255183 * r255181;
        double r255185 = r255183 - r255184;
        double r255186 = fma(r255181, r255182, r255185);
        double r255187 = r255182 / r255178;
        double r255188 = tanh(r255187);
        double r255189 = r255181 * r255188;
        double r255190 = r255183 / r255178;
        double r255191 = tanh(r255190);
        double r255192 = -r255191;
        double r255193 = r255181 * r255192;
        double r255194 = r255189 + r255193;
        double r255195 = fma(r255178, r255194, r255183);
        double r255196 = r255180 ? r255186 : r255195;
        return r255196;
}

Original	4.7
Target	2.0
Herbie	1.5

Derivation

Split input into 2 regimes
if y < -6.697799307361886e+216
1. Initial program 20.0
  \[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-neg20.0
  \[\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-in20.0
  \[\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. Applied associate-+r+20.0
  \[\leadsto \color{blue}{\left(x + \left(y \cdot z\right) \cdot \tanh \left(\frac{t}{y}\right)\right) + \left(y \cdot z\right) \cdot \left(-\tanh \left(\frac{x}{y}\right)\right)}\]
6. Simplified20.0
  \[\leadsto \color{blue}{\mathsf{fma}\left(\tanh \left(\frac{t}{y}\right) \cdot y, z, x\right)} + \left(y \cdot z\right) \cdot \left(-\tanh \left(\frac{x}{y}\right)\right)\]
7. Taylor expanded around inf 3.3
  \[\leadsto \color{blue}{\left(t \cdot z + x\right) - x \cdot z}\]
8. Simplified3.3
  \[\leadsto \color{blue}{\mathsf{fma}\left(z, t, x - x \cdot z\right)}\]
if -6.697799307361886e+216 < y
1. Initial program 3.6
  \[x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\]
2. Simplified1.4
  \[\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 sub-neg1.4
  \[\leadsto \mathsf{fma}\left(y, z \cdot \color{blue}{\left(\tanh \left(\frac{t}{y}\right) + \left(-\tanh \left(\frac{x}{y}\right)\right)\right)}, x\right)\]
5. Applied distribute-lft-in1.4
  \[\leadsto \mathsf{fma}\left(y, \color{blue}{z \cdot \tanh \left(\frac{t}{y}\right) + z \cdot \left(-\tanh \left(\frac{x}{y}\right)\right)}, x\right)\]
Recombined 2 regimes into one program.
Final simplification1.5
\[\leadsto \begin{array}{l} \mathbf{if}\;y \le -6.6977993073618858 \cdot 10^{216}:\\ \;\;\;\;\mathsf{fma}\left(z, t, x - x \cdot z\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(y, z \cdot \tanh \left(\frac{t}{y}\right) + z \cdot \left(-\tanh \left(\frac{x}{y}\right)\right), x\right)\\ \end{array}\]

Error

Target

Derivation

`if y < -6.697799307361886e+216`

`if -6.697799307361886e+216 < y`

Reproduce