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

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

\end{array}

double f(double x, double y, double z, double t) {
        double r347632 = x;
        double r347633 = y;
        double r347634 = z;
        double r347635 = r347633 * r347634;
        double r347636 = t;
        double r347637 = r347636 / r347633;
        double r347638 = tanh(r347637);
        double r347639 = r347632 / r347633;
        double r347640 = tanh(r347639);
        double r347641 = r347638 - r347640;
        double r347642 = r347635 * r347641;
        double r347643 = r347632 + r347642;
        return r347643;
}

↓

double f(double x, double y, double z, double t) {
        double r347644 = y;
        double r347645 = 5.880629389853999e+126;
        bool r347646 = r347644 <= r347645;
        double r347647 = z;
        double r347648 = t;
        double r347649 = r347648 / r347644;
        double r347650 = tanh(r347649);
        double r347651 = x;
        double r347652 = r347651 / r347644;
        double r347653 = tanh(r347652);
        double r347654 = r347650 - r347653;
        double r347655 = r347647 * r347654;
        double r347656 = cbrt(r347655);
        double r347657 = r347656 * r347656;
        double r347658 = r347657 * r347656;
        double r347659 = fma(r347644, r347658, r347651);
        double r347660 = r347648 - r347651;
        double r347661 = r347660 * r347647;
        double r347662 = r347651 + r347661;
        double r347663 = r347646 ? r347659 : r347662;
        return r347663;
}

Original	4.9
Target	2.3
Herbie	2.6

Derivation

Split input into 2 regimes
if y < 5.880629389853999e+126
1. Initial program 3.0
  \[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 add-cube-cbrt1.7
  \[\leadsto \mathsf{fma}\left(y, \color{blue}{\left(\sqrt[3]{z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)} \cdot \sqrt[3]{z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)}\right) \cdot \sqrt[3]{z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)}}, x\right)\]
if 5.880629389853999e+126 < y
1. Initial program 17.7
  \[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 pow117.7
  \[\leadsto x + \left(y \cdot z\right) \cdot \color{blue}{{\left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)}^{1}}\]
4. Applied pow117.7
  \[\leadsto x + \left(y \cdot \color{blue}{{z}^{1}}\right) \cdot {\left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)}^{1}\]
5. Applied pow117.7
  \[\leadsto x + \left(\color{blue}{{y}^{1}} \cdot {z}^{1}\right) \cdot {\left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)}^{1}\]
6. Applied pow-prod-down17.7
  \[\leadsto x + \color{blue}{{\left(y \cdot z\right)}^{1}} \cdot {\left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)}^{1}\]
7. Applied pow-prod-down17.7
  \[\leadsto x + \color{blue}{{\left(\left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\right)}^{1}}\]
8. Simplified7.0
  \[\leadsto x + {\color{blue}{\left(\left(y \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\right) \cdot z\right)}}^{1}\]
9. Taylor expanded around 0 8.2
  \[\leadsto x + {\left(\color{blue}{\left(t - x\right)} \cdot z\right)}^{1}\]
Recombined 2 regimes into one program.
Final simplification2.6
\[\leadsto \begin{array}{l} \mathbf{if}\;y \le 5.880629389853998622248271363708750096354 \cdot 10^{126}:\\ \;\;\;\;\mathsf{fma}\left(y, \left(\sqrt[3]{z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)} \cdot \sqrt[3]{z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)}\right) \cdot \sqrt[3]{z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)}, x\right)\\ \mathbf{else}:\\ \;\;\;\;x + \left(t - x\right) \cdot z\\ \end{array}\]

Falling back on racket egraph because egg-herbie package not installed (more)

Error

Target

Derivation

`if y < 5.880629389853999e+126`

`if 5.880629389853999e+126 < y`

Reproduce