\[\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 -2.315641800986653731087017149548046290874:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + t \cdot \frac{1}{\left(z \cdot 3\right) \cdot y}\\ \mathbf{elif}\;z \cdot 3 \le 2.181965382420920083950531709255992849268 \cdot 10^{-43}:\\ \;\;\;\;\frac{\frac{t}{y}}{z \cdot 3} + \left(x - \frac{y}{z \cdot 3}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{1}{z} \cdot \frac{y}{3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot 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 -2.315641800986653731087017149548046290874:\\
\;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + t \cdot \frac{1}{\left(z \cdot 3\right) \cdot y}\\

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

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

\end{array}

double f(double x, double y, double z, double t) {
        double r492404 = x;
        double r492405 = y;
        double r492406 = z;
        double r492407 = 3.0;
        double r492408 = r492406 * r492407;
        double r492409 = r492405 / r492408;
        double r492410 = r492404 - r492409;
        double r492411 = t;
        double r492412 = r492408 * r492405;
        double r492413 = r492411 / r492412;
        double r492414 = r492410 + r492413;
        return r492414;
}

↓

double f(double x, double y, double z, double t) {
        double r492415 = z;
        double r492416 = 3.0;
        double r492417 = r492415 * r492416;
        double r492418 = -2.3156418009866537;
        bool r492419 = r492417 <= r492418;
        double r492420 = x;
        double r492421 = y;
        double r492422 = r492421 / r492417;
        double r492423 = r492420 - r492422;
        double r492424 = t;
        double r492425 = 1.0;
        double r492426 = r492417 * r492421;
        double r492427 = r492425 / r492426;
        double r492428 = r492424 * r492427;
        double r492429 = r492423 + r492428;
        double r492430 = 2.18196538242092e-43;
        bool r492431 = r492417 <= r492430;
        double r492432 = r492424 / r492421;
        double r492433 = r492432 / r492417;
        double r492434 = r492433 + r492423;
        double r492435 = r492425 / r492415;
        double r492436 = r492421 / r492416;
        double r492437 = r492435 * r492436;
        double r492438 = r492420 - r492437;
        double r492439 = r492424 / r492426;
        double r492440 = r492438 + r492439;
        double r492441 = r492431 ? r492434 : r492440;
        double r492442 = r492419 ? r492429 : r492441;
        return r492442;
}

Original	3.9
Target	1.9
Herbie	0.3

Derivation

Split input into 3 regimes
if (* z 3.0) < -2.3156418009866537
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 div-inv0.4
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{t \cdot \frac{1}{\left(z \cdot 3\right) \cdot y}}\]
if -2.3156418009866537 < (* z 3.0) < 2.18196538242092e-43
1. Initial program 12.1
  \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
2. Using strategy rm
3. Applied add-cube-cbrt12.3
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\color{blue}{\left(\sqrt[3]{t} \cdot \sqrt[3]{t}\right) \cdot \sqrt[3]{t}}}{\left(z \cdot 3\right) \cdot y}\]
4. Applied times-frac1.1
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{z \cdot 3} \cdot \frac{\sqrt[3]{t}}{y}}\]
5. Using strategy rm
6. Applied div-inv1.1
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{z \cdot 3} \cdot \color{blue}{\left(\sqrt[3]{t} \cdot \frac{1}{y}\right)}\]
7. Applied associate-*r*3.8
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\left(\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{z \cdot 3} \cdot \sqrt[3]{t}\right) \cdot \frac{1}{y}}\]
8. Simplified3.4
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{t}{z \cdot 3}} \cdot \frac{1}{y}\]
9. Using strategy rm
10. Applied *-un-lft-identity3.4
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\left(1 \cdot \frac{t}{z \cdot 3}\right)} \cdot \frac{1}{y}\]
11. Applied associate-*l*3.4
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{1 \cdot \left(\frac{t}{z \cdot 3} \cdot \frac{1}{y}\right)}\]
12. Simplified0.3
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + 1 \cdot \color{blue}{\frac{\frac{t}{y}}{z \cdot 3}}\]
if 2.18196538242092e-43 < (* z 3.0)
1. Initial program 0.3
  \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
2. Using strategy rm
3. Applied *-un-lft-identity0.3
  \[\leadsto \left(x - \frac{\color{blue}{1 \cdot y}}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
4. Applied times-frac0.4
  \[\leadsto \left(x - \color{blue}{\frac{1}{z} \cdot \frac{y}{3}}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
Recombined 3 regimes into one program.
Final simplification0.3
\[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot 3 \le -2.315641800986653731087017149548046290874:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + t \cdot \frac{1}{\left(z \cdot 3\right) \cdot y}\\ \mathbf{elif}\;z \cdot 3 \le 2.181965382420920083950531709255992849268 \cdot 10^{-43}:\\ \;\;\;\;\frac{\frac{t}{y}}{z \cdot 3} + \left(x - \frac{y}{z \cdot 3}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{1}{z} \cdot \frac{y}{3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if (* z 3.0) < -2.3156418009866537`

`if -2.3156418009866537 < (* z 3.0) < 2.18196538242092e-43`

`if 2.18196538242092e-43 < (* z 3.0)`

Reproduce

In
Out