\[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.196870900503116440575985645136412622031 \cdot 10^{200} \lor \neg \left(y \le 2.663304700721715703254650879660201780204 \cdot 10^{57}\right):\\ \;\;\;\;x + \left(t \cdot z - x \cdot z\right)\\ \mathbf{else}:\\ \;\;\;\;x + \frac{y \cdot \left(z \cdot \left({\left(\tanh \left(\frac{t}{y}\right)\right)}^{3} - {\left(\tanh \left(\frac{x}{y}\right)\right)}^{3}\right)\right)}{\tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{t}{y}\right) + \left(\tanh \left(\frac{x}{y}\right) \cdot \tanh \left(\frac{x}{y}\right) + \tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{x}{y}\right)\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.196870900503116440575985645136412622031 \cdot 10^{200} \lor \neg \left(y \le 2.663304700721715703254650879660201780204 \cdot 10^{57}\right):\\
\;\;\;\;x + \left(t \cdot z - x \cdot z\right)\\

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

\end{array}

double f(double x, double y, double z, double t) {
        double r460816 = x;
        double r460817 = y;
        double r460818 = z;
        double r460819 = r460817 * r460818;
        double r460820 = t;
        double r460821 = r460820 / r460817;
        double r460822 = tanh(r460821);
        double r460823 = r460816 / r460817;
        double r460824 = tanh(r460823);
        double r460825 = r460822 - r460824;
        double r460826 = r460819 * r460825;
        double r460827 = r460816 + r460826;
        return r460827;
}

↓

double f(double x, double y, double z, double t) {
        double r460828 = y;
        double r460829 = -1.1968709005031164e+200;
        bool r460830 = r460828 <= r460829;
        double r460831 = 2.6633047007217157e+57;
        bool r460832 = r460828 <= r460831;
        double r460833 = !r460832;
        bool r460834 = r460830 || r460833;
        double r460835 = x;
        double r460836 = t;
        double r460837 = z;
        double r460838 = r460836 * r460837;
        double r460839 = r460835 * r460837;
        double r460840 = r460838 - r460839;
        double r460841 = r460835 + r460840;
        double r460842 = r460836 / r460828;
        double r460843 = tanh(r460842);
        double r460844 = 3.0;
        double r460845 = pow(r460843, r460844);
        double r460846 = r460835 / r460828;
        double r460847 = tanh(r460846);
        double r460848 = pow(r460847, r460844);
        double r460849 = r460845 - r460848;
        double r460850 = r460837 * r460849;
        double r460851 = r460828 * r460850;
        double r460852 = r460843 * r460843;
        double r460853 = r460847 * r460847;
        double r460854 = r460843 * r460847;
        double r460855 = r460853 + r460854;
        double r460856 = r460852 + r460855;
        double r460857 = r460851 / r460856;
        double r460858 = r460835 + r460857;
        double r460859 = r460834 ? r460841 : r460858;
        return r460859;
}

Original	4.8
Target	2.0
Herbie	6.2

Derivation

Split input into 2 regimes
if y < -1.1968709005031164e+200 or 2.6633047007217157e+57 < y
1. Initial program 14.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 associate-*l*6.6
  \[\leadsto x + \color{blue}{y \cdot \left(z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\right)}\]
4. Using strategy rm
5. Applied flip3--29.8
  \[\leadsto x + y \cdot \left(z \cdot \color{blue}{\frac{{\left(\tanh \left(\frac{t}{y}\right)\right)}^{3} - {\left(\tanh \left(\frac{x}{y}\right)\right)}^{3}}{\tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{t}{y}\right) + \left(\tanh \left(\frac{x}{y}\right) \cdot \tanh \left(\frac{x}{y}\right) + \tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{x}{y}\right)\right)}}\right)\]
6. Applied associate-*r/30.9
  \[\leadsto x + y \cdot \color{blue}{\frac{z \cdot \left({\left(\tanh \left(\frac{t}{y}\right)\right)}^{3} - {\left(\tanh \left(\frac{x}{y}\right)\right)}^{3}\right)}{\tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{t}{y}\right) + \left(\tanh \left(\frac{x}{y}\right) \cdot \tanh \left(\frac{x}{y}\right) + \tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{x}{y}\right)\right)}}\]
7. Applied associate-*r/30.9
  \[\leadsto x + \color{blue}{\frac{y \cdot \left(z \cdot \left({\left(\tanh \left(\frac{t}{y}\right)\right)}^{3} - {\left(\tanh \left(\frac{x}{y}\right)\right)}^{3}\right)\right)}{\tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{t}{y}\right) + \left(\tanh \left(\frac{x}{y}\right) \cdot \tanh \left(\frac{x}{y}\right) + \tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{x}{y}\right)\right)}}\]
8. Taylor expanded around 0 9.9
  \[\leadsto x + \color{blue}{\left(t \cdot z - x \cdot z\right)}\]
if -1.1968709005031164e+200 < y < 2.6633047007217157e+57
1. Initial program 1.4
  \[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 associate-*l*0.4
  \[\leadsto x + \color{blue}{y \cdot \left(z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\right)}\]
4. Using strategy rm
5. Applied flip3--4.7
  \[\leadsto x + y \cdot \left(z \cdot \color{blue}{\frac{{\left(\tanh \left(\frac{t}{y}\right)\right)}^{3} - {\left(\tanh \left(\frac{x}{y}\right)\right)}^{3}}{\tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{t}{y}\right) + \left(\tanh \left(\frac{x}{y}\right) \cdot \tanh \left(\frac{x}{y}\right) + \tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{x}{y}\right)\right)}}\right)\]
6. Applied associate-*r/4.8
  \[\leadsto x + y \cdot \color{blue}{\frac{z \cdot \left({\left(\tanh \left(\frac{t}{y}\right)\right)}^{3} - {\left(\tanh \left(\frac{x}{y}\right)\right)}^{3}\right)}{\tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{t}{y}\right) + \left(\tanh \left(\frac{x}{y}\right) \cdot \tanh \left(\frac{x}{y}\right) + \tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{x}{y}\right)\right)}}\]
7. Applied associate-*r/4.9
  \[\leadsto x + \color{blue}{\frac{y \cdot \left(z \cdot \left({\left(\tanh \left(\frac{t}{y}\right)\right)}^{3} - {\left(\tanh \left(\frac{x}{y}\right)\right)}^{3}\right)\right)}{\tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{t}{y}\right) + \left(\tanh \left(\frac{x}{y}\right) \cdot \tanh \left(\frac{x}{y}\right) + \tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{x}{y}\right)\right)}}\]
Recombined 2 regimes into one program.
Final simplification6.2
\[\leadsto \begin{array}{l} \mathbf{if}\;y \le -1.196870900503116440575985645136412622031 \cdot 10^{200} \lor \neg \left(y \le 2.663304700721715703254650879660201780204 \cdot 10^{57}\right):\\ \;\;\;\;x + \left(t \cdot z - x \cdot z\right)\\ \mathbf{else}:\\ \;\;\;\;x + \frac{y \cdot \left(z \cdot \left({\left(\tanh \left(\frac{t}{y}\right)\right)}^{3} - {\left(\tanh \left(\frac{x}{y}\right)\right)}^{3}\right)\right)}{\tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{t}{y}\right) + \left(\tanh \left(\frac{x}{y}\right) \cdot \tanh \left(\frac{x}{y}\right) + \tanh \left(\frac{t}{y}\right) \cdot \tanh \left(\frac{x}{y}\right)\right)}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if y < -1.1968709005031164e+200 or 2.6633047007217157e+57 < y`

`if -1.1968709005031164e+200 < y < 2.6633047007217157e+57`

Reproduce

In
Out