\[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 -2.16508962816249898 \cdot 10^{148}:\\ \;\;\;\;\mathsf{fma}\left(t, z, 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 -2.16508962816249898 \cdot 10^{148}:\\
\;\;\;\;\mathsf{fma}\left(t, z, 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 r290831 = x;
        double r290832 = y;
        double r290833 = z;
        double r290834 = r290832 * r290833;
        double r290835 = t;
        double r290836 = r290835 / r290832;
        double r290837 = tanh(r290836);
        double r290838 = r290831 / r290832;
        double r290839 = tanh(r290838);
        double r290840 = r290837 - r290839;
        double r290841 = r290834 * r290840;
        double r290842 = r290831 + r290841;
        return r290842;
}

↓

double f(double x, double y, double z, double t) {
        double r290843 = y;
        double r290844 = -2.165089628162499e+148;
        bool r290845 = r290843 <= r290844;
        double r290846 = t;
        double r290847 = z;
        double r290848 = x;
        double r290849 = r290848 * r290847;
        double r290850 = r290848 - r290849;
        double r290851 = fma(r290846, r290847, r290850);
        double r290852 = r290846 / r290843;
        double r290853 = tanh(r290852);
        double r290854 = r290847 * r290853;
        double r290855 = r290848 / r290843;
        double r290856 = tanh(r290855);
        double r290857 = -r290856;
        double r290858 = r290847 * r290857;
        double r290859 = r290854 + r290858;
        double r290860 = fma(r290843, r290859, r290848);
        double r290861 = r290845 ? r290851 : r290860;
        return r290861;
}

Original	4.5
Target	2.0
Herbie	2.0

Derivation

Split input into 2 regimes
if y < -2.165089628162499e+148
1. Initial program 15.9
  \[x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\]
2. Simplified7.2
  \[\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-neg7.2
  \[\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-in7.2
  \[\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)\]
6. Taylor expanded around inf 12.1
  \[\leadsto \mathsf{fma}\left(y, \color{blue}{\frac{t \cdot z}{y}} + z \cdot \left(-\tanh \left(\frac{x}{y}\right)\right), x\right)\]
7. Taylor expanded around inf 7.5
  \[\leadsto \color{blue}{\left(t \cdot z + x\right) - x \cdot z}\]
8. Simplified7.5
  \[\leadsto \color{blue}{\mathsf{fma}\left(t, z, x - x \cdot z\right)}\]
if -2.165089628162499e+148 < y
1. Initial program 3.1
  \[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 simplification2.0
\[\leadsto \begin{array}{l} \mathbf{if}\;y \le -2.16508962816249898 \cdot 10^{148}:\\ \;\;\;\;\mathsf{fma}\left(t, z, 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 < -2.165089628162499e+148`

`if -2.165089628162499e+148 < y`

Reproduce