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

↓

\[\begin{array}{l} \mathbf{if}\;t \le -1.178114486330545953870810697215483144145 \cdot 10^{-42}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{z \cdot \left(3 \cdot y\right)}\\ \mathbf{elif}\;t \le 1.222827059619427139614541167245800131032 \cdot 10^{-23}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{1}{z}}{\frac{y}{\frac{t}{3}}}\\ \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 -1.178114486330545953870810697215483144145 \cdot 10^{-42}:\\
\;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{z \cdot \left(3 \cdot y\right)}\\

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

\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 r128348165 = x;
        double r128348166 = y;
        double r128348167 = z;
        double r128348168 = 3.0;
        double r128348169 = r128348167 * r128348168;
        double r128348170 = r128348166 / r128348169;
        double r128348171 = r128348165 - r128348170;
        double r128348172 = t;
        double r128348173 = r128348169 * r128348166;
        double r128348174 = r128348172 / r128348173;
        double r128348175 = r128348171 + r128348174;
        return r128348175;
}

↓

double f(double x, double y, double z, double t) {
        double r128348176 = t;
        double r128348177 = -1.178114486330546e-42;
        bool r128348178 = r128348176 <= r128348177;
        double r128348179 = x;
        double r128348180 = y;
        double r128348181 = z;
        double r128348182 = 3.0;
        double r128348183 = r128348181 * r128348182;
        double r128348184 = r128348180 / r128348183;
        double r128348185 = r128348179 - r128348184;
        double r128348186 = r128348182 * r128348180;
        double r128348187 = r128348181 * r128348186;
        double r128348188 = r128348176 / r128348187;
        double r128348189 = r128348185 + r128348188;
        double r128348190 = 1.2228270596194271e-23;
        bool r128348191 = r128348176 <= r128348190;
        double r128348192 = 1.0;
        double r128348193 = r128348192 / r128348181;
        double r128348194 = r128348176 / r128348182;
        double r128348195 = r128348180 / r128348194;
        double r128348196 = r128348193 / r128348195;
        double r128348197 = r128348185 + r128348196;
        double r128348198 = r128348191 ? r128348197 : r128348189;
        double r128348199 = r128348178 ? r128348189 : r128348198;
        return r128348199;
}

Original	3.5
Target	1.7
Herbie	0.4

Derivation

Split input into 2 regimes
if t < -1.178114486330546e-42 or 1.2228270596194271e-23 < 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.7
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{\color{blue}{z \cdot \left(3 \cdot y\right)}}\]
if -1.178114486330546e-42 < t < 1.2228270596194271e-23
1. Initial program 6.0
  \[\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.4
  \[\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.4
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{\color{blue}{1 \cdot t}}{z \cdot 3}}{y}\]
6. Applied times-frac1.4
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \frac{\color{blue}{\frac{1}{z} \cdot \frac{t}{3}}}{y}\]
7. Applied associate-/l*0.2
  \[\leadsto \left(x - \frac{y}{z \cdot 3}\right) + \color{blue}{\frac{\frac{1}{z}}{\frac{y}{\frac{t}{3}}}}\]
Recombined 2 regimes into one program.
Final simplification0.4
\[\leadsto \begin{array}{l} \mathbf{if}\;t \le -1.178114486330545953870810697215483144145 \cdot 10^{-42}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{t}{z \cdot \left(3 \cdot y\right)}\\ \mathbf{elif}\;t \le 1.222827059619427139614541167245800131032 \cdot 10^{-23}:\\ \;\;\;\;\left(x - \frac{y}{z \cdot 3}\right) + \frac{\frac{1}{z}}{\frac{y}{\frac{t}{3}}}\\ \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 < -1.178114486330546e-42 or 1.2228270596194271e-23 < t`

`if -1.178114486330546e-42 < t < 1.2228270596194271e-23`

Reproduce

In
Out