\[\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 r457467 = x;
        double r457468 = y;
        double r457469 = z;
        double r457470 = 3.0;
        double r457471 = r457469 * r457470;
        double r457472 = r457468 / r457471;
        double r457473 = r457467 - r457472;
        double r457474 = t;
        double r457475 = r457471 * r457468;
        double r457476 = r457474 / r457475;
        double r457477 = r457473 + r457476;
        return r457477;
}

↓

double f(double x, double y, double z, double t) {
        double r457478 = z;
        double r457479 = 3.0;
        double r457480 = r457478 * r457479;
        double r457481 = -2.3156418009866537;
        bool r457482 = r457480 <= r457481;
        double r457483 = x;
        double r457484 = y;
        double r457485 = r457484 / r457480;
        double r457486 = r457483 - r457485;
        double r457487 = t;
        double r457488 = 1.0;
        double r457489 = r457480 * r457484;
        double r457490 = r457488 / r457489;
        double r457491 = r457487 * r457490;
        double r457492 = r457486 + r457491;
        double r457493 = 2.18196538242092e-43;
        bool r457494 = r457480 <= r457493;
        double r457495 = r457487 / r457484;
        double r457496 = r457495 / r457480;
        double r457497 = r457496 + r457486;
        double r457498 = r457488 / r457478;
        double r457499 = r457484 / r457479;
        double r457500 = r457498 * r457499;
        double r457501 = r457483 - r457500;
        double r457502 = r457487 / r457489;
        double r457503 = r457501 + r457502;
        double r457504 = r457494 ? r457497 : r457503;
        double r457505 = r457482 ? r457492 : r457504;
        return r457505;
}

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