\[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]

↓

\[\begin{array}{l} \mathbf{if}\;t \le -6.04040118693943595803771657159403407899 \cdot 10^{54}:\\ \;\;\;\;\frac{t}{z \cdot \left(3 \cdot y\right)} + \left(x - \frac{y}{z \cdot 3}\right)\\ \mathbf{elif}\;t \le 17403769.191135458648204803466796875:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{1}{z} \cdot \frac{\frac{t}{3}}{y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\\ \end{array}\]

\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}

↓

\begin{array}{l}
\mathbf{if}\;t \le -6.04040118693943595803771657159403407899 \cdot 10^{54}:\\
\;\;\;\;\frac{t}{z \cdot \left(3 \cdot y\right)} + \left(x - \frac{y}{z \cdot 3}\right)\\

\mathbf{elif}\;t \le 17403769.191135458648204803466796875:\\
\;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{1}{z} \cdot \frac{\frac{t}{3}}{y}\\

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

\end{array}

double f(double x, double y, double z, double t) {
        double r34296472 = x;
        double r34296473 = y;
        double r34296474 = z;
        double r34296475 = 3.0;
        double r34296476 = r34296474 * r34296475;
        double r34296477 = r34296473 / r34296476;
        double r34296478 = r34296472 - r34296477;
        double r34296479 = t;
        double r34296480 = r34296476 * r34296473;
        double r34296481 = r34296479 / r34296480;
        double r34296482 = r34296478 + r34296481;
        return r34296482;
}

↓

double f(double x, double y, double z, double t) {
        double r34296483 = t;
        double r34296484 = -6.040401186939436e+54;
        bool r34296485 = r34296483 <= r34296484;
        double r34296486 = z;
        double r34296487 = 3.0;
        double r34296488 = y;
        double r34296489 = r34296487 * r34296488;
        double r34296490 = r34296486 * r34296489;
        double r34296491 = r34296483 / r34296490;
        double r34296492 = x;
        double r34296493 = r34296486 * r34296487;
        double r34296494 = r34296488 / r34296493;
        double r34296495 = r34296492 - r34296494;
        double r34296496 = r34296491 + r34296495;
        double r34296497 = 17403769.19113546;
        bool r34296498 = r34296483 <= r34296497;
        double r34296499 = 1.0;
        double r34296500 = r34296499 / r34296486;
        double r34296501 = r34296483 / r34296487;
        double r34296502 = r34296501 / r34296488;
        double r34296503 = r34296500 * r34296502;
        double r34296504 = r34296495 + r34296503;
        double r34296505 = r34296488 / r34296486;
        double r34296506 = r34296505 / r34296487;
        double r34296507 = r34296492 - r34296506;
        double r34296508 = r34296483 / r34296493;
        double r34296509 = r34296508 / r34296488;
        double r34296510 = r34296507 + r34296509;
        double r34296511 = r34296498 ? r34296504 : r34296510;
        double r34296512 = r34296485 ? r34296496 : r34296511;
        return r34296512;
}

Original	3.6
Target	1.6
Herbie	0.8

Derivation

Split input into 3 regimes
if t < -6.040401186939436e+54
1. Initial program 0.7
  \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
2. Using strategy rm
3. Applied associate-/r*3.4
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{\frac{t}{z \cdot 3}}{y}}\]
4. Using strategy rm
5. Applied div-inv3.4
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\color{blue}{t \cdot \frac{1}{z \cdot 3}}}{y}\]
6. Applied associate-/l*0.7
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{t}{\frac{y}{\frac{1}{z \cdot 3}}}}\]
7. Simplified0.6
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\color{blue}{\left(y \cdot 3\right) \cdot z}}\]
if -6.040401186939436e+54 < t < 17403769.19113546
1. Initial program 5.3
  \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
2. Using strategy rm
3. Applied associate-/r*1.0
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{\frac{t}{z \cdot 3}}{y}}\]
4. Using strategy rm
5. Applied *-un-lft-identity1.0
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{t}{z \cdot 3}}{\color{blue}{1 \cdot y}}\]
6. Applied *-un-lft-identity1.0
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{\color{blue}{1 \cdot t}}{z \cdot 3}}{1 \cdot y}\]
7. Applied times-frac1.1
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\color{blue}{\frac{1}{z} \cdot \frac{t}{3}}}{1 \cdot y}\]
8. Applied times-frac0.3
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{\frac{1}{z}}{1} \cdot \frac{\frac{t}{3}}{y}}\]
9. Simplified0.3
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{1}{z}} \cdot \frac{\frac{t}{3}}{y}\]
if 17403769.19113546 < t
1. Initial program 0.8
  \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
2. Using strategy rm
3. Applied associate-/r*2.1
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{\frac{t}{z \cdot 3}}{y}}\]
4. Using strategy rm
5. Applied associate-/r*2.1
  \[\leadsto \left(x - \color{blue}{\frac{\frac{y}{z}}{3}}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
Recombined 3 regimes into one program.
Final simplification0.8
\[\leadsto \begin{array}{l} \mathbf{if}\;t \le -6.04040118693943595803771657159403407899 \cdot 10^{54}:\\ \;\;\;\;\frac{t}{z \cdot \left(3 \cdot y\right)} + \left(x - \frac{y}{z \cdot 3}\right)\\ \mathbf{elif}\;t \le 17403769.191135458648204803466796875:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{1}{z} \cdot \frac{\frac{t}{3}}{y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if t < -6.040401186939436e+54`

`if -6.040401186939436e+54 < t < 17403769.19113546`

`if 17403769.19113546 < t`

Reproduce

In
Out