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

↓

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

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

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

\end{array}

double f(double x, double y, double z, double t) {
        double r683963 = x;
        double r683964 = y;
        double r683965 = z;
        double r683966 = 3.0;
        double r683967 = r683965 * r683966;
        double r683968 = r683964 / r683967;
        double r683969 = r683963 - r683968;
        double r683970 = t;
        double r683971 = r683967 * r683964;
        double r683972 = r683970 / r683971;
        double r683973 = r683969 + r683972;
        return r683973;
}

↓

double f(double x, double y, double z, double t) {
        double r683974 = t;
        double r683975 = -2.217051937980128e+48;
        bool r683976 = r683974 <= r683975;
        double r683977 = 0.3333333333333333;
        double r683978 = z;
        double r683979 = y;
        double r683980 = r683978 * r683979;
        double r683981 = r683974 / r683980;
        double r683982 = r683977 * r683981;
        double r683983 = x;
        double r683984 = r683982 + r683983;
        double r683985 = r683979 / r683978;
        double r683986 = r683977 * r683985;
        double r683987 = r683984 - r683986;
        double r683988 = 1.3743927570433301e-73;
        bool r683989 = r683974 <= r683988;
        double r683990 = 3.0;
        double r683991 = r683985 / r683990;
        double r683992 = r683983 - r683991;
        double r683993 = 1.0;
        double r683994 = r683993 / r683978;
        double r683995 = r683974 / r683990;
        double r683996 = r683995 / r683979;
        double r683997 = r683994 * r683996;
        double r683998 = r683992 + r683997;
        double r683999 = r683978 * r683990;
        double r684000 = r683979 / r683999;
        double r684001 = r683983 - r684000;
        double r684002 = r683990 * r683980;
        double r684003 = r683974 / r684002;
        double r684004 = r684001 + r684003;
        double r684005 = r683989 ? r683998 : r684004;
        double r684006 = r683976 ? r683987 : r684005;
        return r684006;
}

Original	3.8
Target	1.9
Herbie	0.6

Derivation

Split input into 3 regimes
if t < -2.217051937980128e+48
1. Initial program 0.6
  \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
2. Taylor expanded around 0 0.8
  \[\leadsto \color{blue}{\left(0.3333333333333333148296162562473909929395 \cdot \frac{t}{z \cdot y} + x\right) - 0.3333333333333333148296162562473909929395 \cdot \frac{y}{z}}\]
if -2.217051937980128e+48 < t < 1.3743927570433301e-73
1. Initial program 6.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*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}\]
6. Using strategy rm
7. Applied *-un-lft-identity1.3
  \[\leadsto \left(x - \frac{\frac{y}{z}}{3}\right) + \frac{\frac{t}{z \cdot 3}}{\color{blue}{1 \cdot y}}\]
8. Applied *-un-lft-identity1.3
  \[\leadsto \left(x - \frac{\frac{y}{z}}{3}\right) + \frac{\frac{\color{blue}{1 \cdot t}}{z \cdot 3}}{1 \cdot y}\]
9. Applied times-frac1.3
  \[\leadsto \left(x - \frac{\frac{y}{z}}{3}\right) + \frac{\color{blue}{\frac{1}{z} \cdot \frac{t}{3}}}{1 \cdot y}\]
10. Applied times-frac0.3
  \[\leadsto \left(x - \frac{\frac{y}{z}}{3}\right) + \color{blue}{\frac{\frac{1}{z}}{1} \cdot \frac{\frac{t}{3}}{y}}\]
11. Simplified0.3
  \[\leadsto \left(x - \frac{\frac{y}{z}}{3}\right) + \color{blue}{\frac{1}{z}} \cdot \frac{\frac{t}{3}}{y}\]
if 1.3743927570433301e-73 < t
1. Initial program 1.0
  \[\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
2. Taylor expanded around 0 0.9
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\color{blue}{3 \cdot \left(z \cdot y\right)}}\]
Recombined 3 regimes into one program.
Final simplification0.6
\[\leadsto \begin{array}{l} \mathbf{if}\;t \le -2.217051937980127926982818674661840685718 \cdot 10^{48}:\\ \;\;\;\;\left(0.3333333333333333148296162562473909929395 \cdot \frac{t}{z \cdot y} + x\right) - 0.3333333333333333148296162562473909929395 \cdot \frac{y}{z}\\ \mathbf{elif}\;t \le 1.374392757043330110386267311148160852221 \cdot 10^{-73}:\\ \;\;\;\;\left(x - \frac{\frac{y}{z}}{3}\right) + \frac{1}{z} \cdot \frac{\frac{t}{3}}{y}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{3 \cdot \left(z \cdot y\right)}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if t < -2.217051937980128e+48`

`if -2.217051937980128e+48 < t < 1.3743927570433301e-73`

`if 1.3743927570433301e-73 < t`

Reproduce

In
Out