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

↓

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

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

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

\end{array}

double f(double x, double y, double z, double t) {
        double r832569 = x;
        double r832570 = y;
        double r832571 = z;
        double r832572 = 3.0;
        double r832573 = r832571 * r832572;
        double r832574 = r832570 / r832573;
        double r832575 = r832569 - r832574;
        double r832576 = t;
        double r832577 = r832573 * r832570;
        double r832578 = r832576 / r832577;
        double r832579 = r832575 + r832578;
        return r832579;
}

↓

double f(double x, double y, double z, double t) {
        double r832580 = z;
        double r832581 = -3.2147543878332805e+72;
        bool r832582 = r832580 <= r832581;
        double r832583 = x;
        double r832584 = y;
        double r832585 = r832584 / r832580;
        double r832586 = 3.0;
        double r832587 = r832585 / r832586;
        double r832588 = r832583 - r832587;
        double r832589 = t;
        double r832590 = r832580 * r832586;
        double r832591 = r832589 / r832590;
        double r832592 = r832591 / r832584;
        double r832593 = r832588 + r832592;
        double r832594 = 8.835356839411459e-17;
        bool r832595 = r832580 <= r832594;
        double r832596 = r832584 / r832590;
        double r832597 = r832583 - r832596;
        double r832598 = 1.0;
        double r832599 = r832598 / r832580;
        double r832600 = r832589 / r832586;
        double r832601 = r832600 / r832584;
        double r832602 = r832599 * r832601;
        double r832603 = r832597 + r832602;
        double r832604 = 0.3333333333333333;
        double r832605 = r832604 * r832585;
        double r832606 = r832583 - r832605;
        double r832607 = r832589 / r832580;
        double r832608 = r832607 / r832586;
        double r832609 = r832608 / r832584;
        double r832610 = r832606 + r832609;
        double r832611 = r832595 ? r832603 : r832610;
        double r832612 = r832582 ? r832593 : r832611;
        return r832612;
}

Original	3.4
Target	1.7
Herbie	0.9

Derivation

Split input into 3 regimes
if z < -3.2147543878332805e+72
1. Initial program 0.4
  \[\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.2
  \[\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.2
  \[\leadsto \left(x - \color{blue}{\frac{\frac{y}{z}}{3}}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
if -3.2147543878332805e+72 < z < 8.835356839411459e-17
1. Initial program 8.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*2.7
  \[\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-identity2.7
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{t}{z \cdot 3}}{\color{blue}{1 \cdot y}}\]
6. Applied *-un-lft-identity2.7
  \[\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-frac2.7
  \[\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.5
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{\frac{1}{z}}{1} \cdot \frac{\frac{t}{3}}{y}}\]
9. Simplified0.5
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{1}{z}} \cdot \frac{\frac{t}{3}}{y}\]
if 8.835356839411459e-17 < z
1. Initial program 0.4
  \[\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*0.9
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\color{blue}{\frac{\frac{t}{z}}{3}}}{y}\]
6. Taylor expanded around 0 1.0
  \[\leadsto \left(x - \color{blue}{0.3333333333333333148296162562473909929395 \cdot \frac{y}{z}}\right) + \frac{\frac{\frac{t}{z}}{3}}{y}\]
Recombined 3 regimes into one program.
Final simplification0.9
\[\leadsto \begin{array}{l} \mathbf{if}\;z \le -3.214754387833280487507853222414480503506 \cdot 10^{72}:\\ \;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\\ \mathbf{elif}\;z \le 8.835356839411459215600355025202658239957 \cdot 10^{-17}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{1}{z} \cdot \frac{\frac{t}{3}}{y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - 0.3333333333333333148296162562473909929395 \cdot \frac{y}{z}\right) + \frac{\frac{\frac{t}{z}}{3}}{y}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if z < -3.2147543878332805e+72`

`if -3.2147543878332805e+72 < z < 8.835356839411459e-17`

`if 8.835356839411459e-17 < z`

Reproduce

In
Out