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

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

\end{array}

double f(double x, double y, double z, double t) {
        double r389465 = x;
        double r389466 = y;
        double r389467 = z;
        double r389468 = r389466 * r389467;
        double r389469 = t;
        double r389470 = r389469 / r389466;
        double r389471 = tanh(r389470);
        double r389472 = r389465 / r389466;
        double r389473 = tanh(r389472);
        double r389474 = r389471 - r389473;
        double r389475 = r389468 * r389474;
        double r389476 = r389465 + r389475;
        return r389476;
}

↓

double f(double x, double y, double z, double t) {
        double r389477 = y;
        double r389478 = -7.94401716664695e+198;
        bool r389479 = r389477 <= r389478;
        double r389480 = 4.7657315171304475e+204;
        bool r389481 = r389477 <= r389480;
        double r389482 = !r389481;
        bool r389483 = r389479 || r389482;
        double r389484 = x;
        double r389485 = t;
        double r389486 = z;
        double r389487 = r389485 * r389486;
        double r389488 = r389484 * r389486;
        double r389489 = -r389488;
        double r389490 = r389487 + r389489;
        double r389491 = r389484 + r389490;
        double r389492 = r389485 / r389477;
        double r389493 = tanh(r389492);
        double r389494 = r389484 / r389477;
        double r389495 = tanh(r389494);
        double r389496 = r389493 - r389495;
        double r389497 = r389486 * r389496;
        double r389498 = fma(r389477, r389497, r389484);
        double r389499 = r389483 ? r389491 : r389498;
        return r389499;
}

Original	4.8
Target	2.1
Herbie	1.2

Derivation

Split input into 2 regimes
if y < -7.94401716664695e+198 or 4.7657315171304475e+204 < y
1. Initial program 19.1
  \[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-neg19.1
  \[\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-in19.1
  \[\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. Taylor expanded around 0 20.3
  \[\leadsto x + \left(\color{blue}{t \cdot z} + \left(y \cdot z\right) \cdot \left(-\tanh \left(\frac{x}{y}\right)\right)\right)\]
6. Taylor expanded around 0 3.6
  \[\leadsto x + \left(t \cdot z + \color{blue}{-1 \cdot \left(x \cdot z\right)}\right)\]
7. Simplified3.6
  \[\leadsto x + \left(t \cdot z + \color{blue}{\left(-x \cdot z\right)}\right)\]
if -7.94401716664695e+198 < y < 4.7657315171304475e+204
1. Initial program 2.3
  \[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)}\]
Recombined 2 regimes into one program.
Final simplification1.2
\[\leadsto \begin{array}{l} \mathbf{if}\;y \le -7.94401716664694973 \cdot 10^{198} \lor \neg \left(y \le 4.7657315171304475 \cdot 10^{204}\right):\\ \;\;\;\;x + \left(t \cdot z + \left(-x \cdot z\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(y, z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right), x\right)\\ \end{array}\]

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

Error

Target

Derivation

`if y < -7.94401716664695e+198 or 4.7657315171304475e+204 < y`

`if -7.94401716664695e+198 < y < 4.7657315171304475e+204`

Reproduce