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

↓

\[\begin{array}{l} \mathbf{if}\;t \le \frac{-506273689798637}{32}:\\ \;\;\;\;\left(x - \frac{1}{z} \cdot \frac{y}{3}\right) + \frac{6004799503160661}{18014398509481984} \cdot \frac{t}{z \cdot y}\\ \mathbf{elif}\;t \le \frac{1256220062599297}{549755813888}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{1}{z \cdot 3} \cdot \frac{t}{y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{z \cdot \left(3 \cdot y\right)}\\ \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 \frac{-506273689798637}{32}:\\
\;\;\;\;\left(x - \frac{1}{z} \cdot \frac{y}{3}\right) + \frac{6004799503160661}{18014398509481984} \cdot \frac{t}{z \cdot y}\\

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

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

\end{array}

double f(double x, double y, double z, double t) {
        double r435289 = x;
        double r435290 = y;
        double r435291 = z;
        double r435292 = 3.0;
        double r435293 = r435291 * r435292;
        double r435294 = r435290 / r435293;
        double r435295 = r435289 - r435294;
        double r435296 = t;
        double r435297 = r435293 * r435290;
        double r435298 = r435296 / r435297;
        double r435299 = r435295 + r435298;
        return r435299;
}

↓

double f(double x, double y, double z, double t) {
        double r435300 = t;
        double r435301 = -506273689798637.0;
        double r435302 = 32.0;
        double r435303 = r435301 / r435302;
        bool r435304 = r435300 <= r435303;
        double r435305 = x;
        double r435306 = 1.0;
        double r435307 = z;
        double r435308 = r435306 / r435307;
        double r435309 = y;
        double r435310 = 3.0;
        double r435311 = r435309 / r435310;
        double r435312 = r435308 * r435311;
        double r435313 = r435305 - r435312;
        double r435314 = 6004799503160661.0;
        double r435315 = 18014398509481984.0;
        double r435316 = r435314 / r435315;
        double r435317 = r435307 * r435309;
        double r435318 = r435300 / r435317;
        double r435319 = r435316 * r435318;
        double r435320 = r435313 + r435319;
        double r435321 = 1256220062599297.0;
        double r435322 = 549755813888.0;
        double r435323 = r435321 / r435322;
        bool r435324 = r435300 <= r435323;
        double r435325 = r435307 * r435310;
        double r435326 = r435309 / r435325;
        double r435327 = r435305 - r435326;
        double r435328 = r435306 / r435325;
        double r435329 = r435300 / r435309;
        double r435330 = r435328 * r435329;
        double r435331 = r435327 + r435330;
        double r435332 = r435310 * r435309;
        double r435333 = r435307 * r435332;
        double r435334 = r435300 / r435333;
        double r435335 = r435327 + r435334;
        double r435336 = r435324 ? r435331 : r435335;
        double r435337 = r435304 ? r435320 : r435336;
        return r435337;
}

Original	3.7
Target	1.6
Herbie	0.4

Derivation

Split input into 3 regimes
if t < -15821052806207.406
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.6
  \[\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.6
  \[\leadsto \left(x - \frac{\color{blue}{1 \cdot y}}{z \cdot 3}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
6. Applied times-frac2.7
  \[\leadsto \left(x - \color{blue}{\frac{1}{z} \cdot \frac{y}{3}}\right) + \frac{\frac{t}{z \cdot 3}}{y}\]
7. Taylor expanded around 0 0.9
  \[\leadsto \left(x - \frac{1}{z} \cdot \frac{y}{3}\right) + \color{blue}{0.3333333333333333148296162562473909929395 \cdot \frac{t}{z \cdot y}}\]
8. Simplified0.9
  \[\leadsto \left(x - \frac{1}{z} \cdot \frac{y}{3}\right) + \color{blue}{\frac{6004799503160661}{18014398509481984} \cdot \frac{t}{z \cdot y}}\]
if -15821052806207.406 < t < 2285.0509823898337
1. Initial program 5.7
  \[\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-identity5.7
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\color{blue}{1 \cdot t}}{\left(z \cdot 3\right) \cdot y}\]
4. Applied times-frac0.2
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{1}{z \cdot 3} \cdot \frac{t}{y}}\]
if 2285.0509823898337 < t
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-*l*0.6
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\color{blue}{z \cdot \left(3 \cdot y\right)}}\]
Recombined 3 regimes into one program.
Final simplification0.4
\[\leadsto \begin{array}{l} \mathbf{if}\;t \le \frac{-506273689798637}{32}:\\ \;\;\;\;\left(x - \frac{1}{z} \cdot \frac{y}{3}\right) + \frac{6004799503160661}{18014398509481984} \cdot \frac{t}{z \cdot y}\\ \mathbf{elif}\;t \le \frac{1256220062599297}{549755813888}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{1}{z \cdot 3} \cdot \frac{t}{y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{z \cdot \left(3 \cdot y\right)}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if t < -15821052806207.406`

`if -15821052806207.406 < t < 2285.0509823898337`

`if 2285.0509823898337 < t`

Reproduce

In
Out