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

↓

\[\begin{array}{l} \mathbf{if}\;z \cdot 3 \le -1.716269219097667220680307842591492676446 \cdot 10^{-96}:\\ \;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\\ \mathbf{elif}\;z \cdot 3 \le 1.993322025506344519526479251727249467057 \cdot 10^{64}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{1}{z} \cdot \frac{\frac{t}{3}}{y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{\frac{t}{z}}{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}\;z \cdot 3 \le -1.716269219097667220680307842591492676446 \cdot 10^{-96}:\\
\;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\\

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

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

\end{array}

double f(double x, double y, double z, double t) {
        double r105423 = x;
        double r105424 = y;
        double r105425 = z;
        double r105426 = 3.0;
        double r105427 = r105425 * r105426;
        double r105428 = r105424 / r105427;
        double r105429 = r105423 - r105428;
        double r105430 = t;
        double r105431 = r105427 * r105424;
        double r105432 = r105430 / r105431;
        double r105433 = r105429 + r105432;
        return r105433;
}

↓

double f(double x, double y, double z, double t) {
        double r105434 = z;
        double r105435 = 3.0;
        double r105436 = r105434 * r105435;
        double r105437 = -1.7162692190976672e-96;
        bool r105438 = r105436 <= r105437;
        double r105439 = x;
        double r105440 = y;
        double r105441 = r105440 / r105434;
        double r105442 = r105441 / r105435;
        double r105443 = r105439 - r105442;
        double r105444 = t;
        double r105445 = r105444 / r105436;
        double r105446 = r105445 / r105440;
        double r105447 = r105443 + r105446;
        double r105448 = 1.9933220255063445e+64;
        bool r105449 = r105436 <= r105448;
        double r105450 = r105440 / r105436;
        double r105451 = r105439 - r105450;
        double r105452 = 1.0;
        double r105453 = r105452 / r105434;
        double r105454 = r105444 / r105435;
        double r105455 = r105454 / r105440;
        double r105456 = r105453 * r105455;
        double r105457 = r105451 + r105456;
        double r105458 = r105444 / r105434;
        double r105459 = r105458 / r105435;
        double r105460 = r105459 / r105440;
        double r105461 = r105451 + r105460;
        double r105462 = r105449 ? r105457 : r105461;
        double r105463 = r105438 ? r105447 : r105462;
        return r105463;
}

Original	3.6
Target	1.8
Herbie	1.0

Derivation

Split input into 3 regimes
if (* z 3.0) < -1.7162692190976672e-96
1. Initial program 1.0
  \[\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.3
  \[\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*1.3
  \[\leadsto \left(x - \color{blue}{\frac{\frac{y}{z}}{3}}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
if -1.7162692190976672e-96 < (* z 3.0) < 1.9933220255063445e+64
1. Initial program 9.5
  \[\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.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-identity3.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-identity3.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-frac3.0
  \[\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.6
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{\frac{1}{z}}{1} \cdot \frac{\frac{t}{3}}{y}}\]
9. Simplified0.6
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{1}{z}} \cdot \frac{\frac{t}{3}}{y}\]
if 1.9933220255063445e+64 < (* z 3.0)
1. Initial program 0.5
  \[\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 associate-/r*1.0
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\color{blue}{\frac{\frac{t}{z}}{3}}}{y}\]
Recombined 3 regimes into one program.
Final simplification1.0
\[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot 3 \le -1.716269219097667220680307842591492676446 \cdot 10^{-96}:\\ \;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\\ \mathbf{elif}\;z \cdot 3 \le 1.993322025506344519526479251727249467057 \cdot 10^{64}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{1}{z} \cdot \frac{\frac{t}{3}}{y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{\frac{t}{z}}{3}}{y}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if (* z 3.0) < -1.7162692190976672e-96`

`if -1.7162692190976672e-96 < (* z 3.0) < 1.9933220255063445e+64`

`if 1.9933220255063445e+64 < (* z 3.0)`

Reproduce

In
Out