\[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 -3.414138778260208167560063771776478539909 \cdot 10^{225} \lor \neg \left(y \le 1.263167832907015626468203374323247722442 \cdot 10^{113}\right):\\ \;\;\;\;\mathsf{fma}\left(z, t, x - x \cdot z\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right) \cdot \left(y \cdot z\right) + x\\ \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 -3.414138778260208167560063771776478539909 \cdot 10^{225} \lor \neg \left(y \le 1.263167832907015626468203374323247722442 \cdot 10^{113}\right):\\
\;\;\;\;\mathsf{fma}\left(z, t, x - x \cdot z\right)\\

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

\end{array}

double f(double x, double y, double z, double t) {
        double r517742 = x;
        double r517743 = y;
        double r517744 = z;
        double r517745 = r517743 * r517744;
        double r517746 = t;
        double r517747 = r517746 / r517743;
        double r517748 = tanh(r517747);
        double r517749 = r517742 / r517743;
        double r517750 = tanh(r517749);
        double r517751 = r517748 - r517750;
        double r517752 = r517745 * r517751;
        double r517753 = r517742 + r517752;
        return r517753;
}

↓

double f(double x, double y, double z, double t) {
        double r517754 = y;
        double r517755 = -3.414138778260208e+225;
        bool r517756 = r517754 <= r517755;
        double r517757 = 1.2631678329070156e+113;
        bool r517758 = r517754 <= r517757;
        double r517759 = !r517758;
        bool r517760 = r517756 || r517759;
        double r517761 = z;
        double r517762 = t;
        double r517763 = x;
        double r517764 = r517763 * r517761;
        double r517765 = r517763 - r517764;
        double r517766 = fma(r517761, r517762, r517765);
        double r517767 = r517762 / r517754;
        double r517768 = tanh(r517767);
        double r517769 = r517763 / r517754;
        double r517770 = tanh(r517769);
        double r517771 = r517768 - r517770;
        double r517772 = r517754 * r517761;
        double r517773 = r517771 * r517772;
        double r517774 = r517773 + r517763;
        double r517775 = r517760 ? r517766 : r517774;
        return r517775;
}

Original	4.9
Target	2.2
Herbie	2.8

Derivation

Split input into 2 regimes
if y < -3.414138778260208e+225 or 1.2631678329070156e+113 < y
1. Initial program 17.8
  \[x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\]
2. Simplified8.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 add-cbrt-cube14.3
  \[\leadsto \mathsf{fma}\left(y, z \cdot \left(\tanh \left(\frac{t}{y}\right) - \color{blue}{\sqrt[3]{\left(\tanh \left(\frac{x}{y}\right) \cdot \tanh \left(\frac{x}{y}\right)\right) \cdot \tanh \left(\frac{x}{y}\right)}}\right), x\right)\]
5. Simplified14.3
  \[\leadsto \mathsf{fma}\left(y, z \cdot \left(\tanh \left(\frac{t}{y}\right) - \sqrt[3]{\color{blue}{{\left(\tanh \left(\frac{x}{y}\right)\right)}^{3}}}\right), x\right)\]
6. Using strategy rm
7. Applied fma-udef14.3
  \[\leadsto \color{blue}{y \cdot \left(z \cdot \left(\tanh \left(\frac{t}{y}\right) - \sqrt[3]{{\left(\tanh \left(\frac{x}{y}\right)\right)}^{3}}\right)\right) + x}\]
8. Simplified17.8
  \[\leadsto \color{blue}{\left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right) \cdot \left(y \cdot z\right)} + x\]
9. Taylor expanded around inf 7.0
  \[\leadsto \color{blue}{\left(t \cdot z + x\right) - x \cdot z}\]
10. Simplified7.0
  \[\leadsto \color{blue}{\mathsf{fma}\left(z, t, x - x \cdot z\right)}\]
if -3.414138778260208e+225 < y < 1.2631678329070156e+113
1. Initial program 1.8
  \[x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\]
2. Simplified0.7
  \[\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 add-cbrt-cube2.3
  \[\leadsto \mathsf{fma}\left(y, z \cdot \left(\tanh \left(\frac{t}{y}\right) - \color{blue}{\sqrt[3]{\left(\tanh \left(\frac{x}{y}\right) \cdot \tanh \left(\frac{x}{y}\right)\right) \cdot \tanh \left(\frac{x}{y}\right)}}\right), x\right)\]
5. Simplified2.3
  \[\leadsto \mathsf{fma}\left(y, z \cdot \left(\tanh \left(\frac{t}{y}\right) - \sqrt[3]{\color{blue}{{\left(\tanh \left(\frac{x}{y}\right)\right)}^{3}}}\right), x\right)\]
6. Using strategy rm
7. Applied fma-udef2.3
  \[\leadsto \color{blue}{y \cdot \left(z \cdot \left(\tanh \left(\frac{t}{y}\right) - \sqrt[3]{{\left(\tanh \left(\frac{x}{y}\right)\right)}^{3}}\right)\right) + x}\]
8. Simplified1.8
  \[\leadsto \color{blue}{\left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right) \cdot \left(y \cdot z\right)} + x\]
Recombined 2 regimes into one program.
Final simplification2.8
\[\leadsto \begin{array}{l} \mathbf{if}\;y \le -3.414138778260208167560063771776478539909 \cdot 10^{225} \lor \neg \left(y \le 1.263167832907015626468203374323247722442 \cdot 10^{113}\right):\\ \;\;\;\;\mathsf{fma}\left(z, t, x - x \cdot z\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right) \cdot \left(y \cdot z\right) + x\\ \end{array}\]

Error

Target

Derivation

`if y < -3.414138778260208e+225 or 1.2631678329070156e+113 < y`

`if -3.414138778260208e+225 < y < 1.2631678329070156e+113`

Reproduce