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

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

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

\end{array}

double f(double x, double y, double z, double t) {
        double r653144 = x;
        double r653145 = y;
        double r653146 = z;
        double r653147 = 3.0;
        double r653148 = r653146 * r653147;
        double r653149 = r653145 / r653148;
        double r653150 = r653144 - r653149;
        double r653151 = t;
        double r653152 = r653148 * r653145;
        double r653153 = r653151 / r653152;
        double r653154 = r653150 + r653153;
        return r653154;
}

↓

double f(double x, double y, double z, double t) {
        double r653155 = z;
        double r653156 = 3.0;
        double r653157 = r653155 * r653156;
        double r653158 = -7.356225768764254e+37;
        bool r653159 = r653157 <= r653158;
        double r653160 = x;
        double r653161 = 1.0;
        double r653162 = y;
        double r653163 = r653157 / r653162;
        double r653164 = r653161 / r653163;
        double r653165 = r653160 - r653164;
        double r653166 = t;
        double r653167 = r653157 * r653162;
        double r653168 = r653166 / r653167;
        double r653169 = r653165 + r653168;
        double r653170 = 2.357897429842403e+78;
        bool r653171 = r653157 <= r653170;
        double r653172 = r653162 / r653157;
        double r653173 = r653160 - r653172;
        double r653174 = r653166 / r653162;
        double r653175 = r653174 / r653157;
        double r653176 = r653173 + r653175;
        double r653177 = r653161 / r653155;
        double r653178 = r653162 / r653156;
        double r653179 = r653177 * r653178;
        double r653180 = r653160 - r653179;
        double r653181 = r653166 / r653156;
        double r653182 = r653177 * r653181;
        double r653183 = r653182 / r653162;
        double r653184 = r653180 + r653183;
        double r653185 = r653171 ? r653176 : r653184;
        double r653186 = r653159 ? r653169 : r653185;
        return r653186;
}

Original	3.6
Target	1.9
Herbie	0.7

Derivation

Split input into 3 regimes
if (* z 3.0) < -7.356225768764254e+37
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 clear-num0.4
  \[\leadsto \left(x - \color{blue}{\frac{1}{\frac{z \cdot 3}{y}}}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\]
if -7.356225768764254e+37 < (* z 3.0) < 2.357897429842403e+78
1. Initial program 7.8
  \[\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-cbrt8.0
  \[\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-frac0.9
  \[\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 associate-*l/0.9
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{\left(\sqrt[3]{t} \cdot \sqrt[3]{t}\right) \cdot \frac{\sqrt[3]{t}}{y}}{z \cdot 3}}\]
7. Simplified0.6
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\color{blue}{\frac{t}{y}}}{z \cdot 3}\]
if 2.357897429842403e+78 < (* z 3.0)
1. Initial program 0.5
  \[\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 *-un-lft-identity1.2
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{\color{blue}{1 \cdot t}}{z \cdot 3}}{y}\]
6. Applied times-frac1.2
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\color{blue}{\frac{1}{z} \cdot \frac{t}{3}}}{y}\]
7. Using strategy rm
8. Applied *-un-lft-identity1.2
  \[\leadsto \left(x - \frac{\color{blue}{1 \cdot y}}{z \cdot 3}\right) + \frac{\frac{1}{z} \cdot \frac{t}{3}}{y}\]
9. Applied times-frac1.2
  \[\leadsto \left(x - \color{blue}{\frac{1}{z} \cdot \frac{y}{3}}\right) + \frac{\frac{1}{z} \cdot \frac{t}{3}}{y}\]
Recombined 3 regimes into one program.
Final simplification0.7
\[\leadsto \begin{array}{l} \mathbf{if}\;z \cdot 3 \le -73562257687642543292240068825919258624:\\ \;\;\;\;\left(x - \frac{1}{\frac{z \cdot 3}{y}}\right) + \frac{t}{\left(z \cdot 3\right) \cdot y}\\ \mathbf{elif}\;z \cdot 3 \le 2.357897429842402930998768322142604435202 \cdot 10^{78}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{t}{y}}{z \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(x - \frac{1}{z} \cdot \frac{y}{3}\right) + \frac{\frac{1}{z} \cdot \frac{t}{3}}{y}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if (* z 3.0) < -7.356225768764254e+37`

`if -7.356225768764254e+37 < (* z 3.0) < 2.357897429842403e+78`

`if 2.357897429842403e+78 < (* z 3.0)`

Reproduce

In
Out