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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -1.5020866955626825 \cdot 10^{-30}:\\ \;\;\;\;\left(x - \frac{y}{3.0} \cdot \frac{1}{z}\right) + \frac{\frac{t}{3.0 \cdot z}}{y}\\ \mathbf{elif}\;z \le 2.750296502407607 \cdot 10^{+21}:\\ \;\;\;\;\frac{\frac{\frac{t}{y}}{z}}{3.0} + \left(x - \frac{y}{3.0 \cdot z}\right)\\ \mathbf{else}:\\ \;\;\;\;x + \left(\frac{t}{z \cdot y} - \frac{y}{z}\right) \cdot 0.3333333333333333\\ \end{array}\]

\left(x - \frac{y}{z \cdot 3.0}\right) + \frac{t}{\left(z \cdot 3.0\right) \cdot y}

↓

\begin{array}{l}
\mathbf{if}\;z \le -1.5020866955626825 \cdot 10^{-30}:\\
\;\;\;\;\left(x - \frac{y}{3.0} \cdot \frac{1}{z}\right) + \frac{\frac{t}{3.0 \cdot z}}{y}\\

\mathbf{elif}\;z \le 2.750296502407607 \cdot 10^{+21}:\\
\;\;\;\;\frac{\frac{\frac{t}{y}}{z}}{3.0} + \left(x - \frac{y}{3.0 \cdot z}\right)\\

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

\end{array}

double f(double x, double y, double z, double t) {
        double r31182166 = x;
        double r31182167 = y;
        double r31182168 = z;
        double r31182169 = 3.0;
        double r31182170 = r31182168 * r31182169;
        double r31182171 = r31182167 / r31182170;
        double r31182172 = r31182166 - r31182171;
        double r31182173 = t;
        double r31182174 = r31182170 * r31182167;
        double r31182175 = r31182173 / r31182174;
        double r31182176 = r31182172 + r31182175;
        return r31182176;
}

↓

double f(double x, double y, double z, double t) {
        double r31182177 = z;
        double r31182178 = -1.5020866955626825e-30;
        bool r31182179 = r31182177 <= r31182178;
        double r31182180 = x;
        double r31182181 = y;
        double r31182182 = 3.0;
        double r31182183 = r31182181 / r31182182;
        double r31182184 = 1.0;
        double r31182185 = r31182184 / r31182177;
        double r31182186 = r31182183 * r31182185;
        double r31182187 = r31182180 - r31182186;
        double r31182188 = t;
        double r31182189 = r31182182 * r31182177;
        double r31182190 = r31182188 / r31182189;
        double r31182191 = r31182190 / r31182181;
        double r31182192 = r31182187 + r31182191;
        double r31182193 = 2.750296502407607e+21;
        bool r31182194 = r31182177 <= r31182193;
        double r31182195 = r31182188 / r31182181;
        double r31182196 = r31182195 / r31182177;
        double r31182197 = r31182196 / r31182182;
        double r31182198 = r31182181 / r31182189;
        double r31182199 = r31182180 - r31182198;
        double r31182200 = r31182197 + r31182199;
        double r31182201 = r31182177 * r31182181;
        double r31182202 = r31182188 / r31182201;
        double r31182203 = r31182181 / r31182177;
        double r31182204 = r31182202 - r31182203;
        double r31182205 = 0.3333333333333333;
        double r31182206 = r31182204 * r31182205;
        double r31182207 = r31182180 + r31182206;
        double r31182208 = r31182194 ? r31182200 : r31182207;
        double r31182209 = r31182179 ? r31182192 : r31182208;
        return r31182209;
}

Original	3.4
Target	1.7
Herbie	0.6

Derivation

Split input into 3 regimes
if z < -1.5020866955626825e-30
1. Initial program 0.4
  \[\left(x - \frac{y}{z \cdot 3.0}\right) + \frac{t}{\left(z \cdot 3.0\right) \cdot y}\]
2. Using strategy rm
3. Applied associate-/r*0.9
  \[\leadsto \left(x - \frac{y}{z \cdot 3.0}\right) + \color{blue}{\frac{\frac{t}{z \cdot 3.0}}{y}}\]
4. Using strategy rm
5. Applied *-un-lft-identity0.9
  \[\leadsto \left(x - \frac{\color{blue}{1 \cdot y}}{z \cdot 3.0}\right) + \frac{\frac{t}{z \cdot 3.0}}{y}\]
6. Applied times-frac0.9
  \[\leadsto \left(x - \color{blue}{\frac{1}{z} \cdot \frac{y}{3.0}}\right) + \frac{\frac{t}{z \cdot 3.0}}{y}\]
if -1.5020866955626825e-30 < z < 2.750296502407607e+21
1. Initial program 9.8
  \[\left(x - \frac{y}{z \cdot 3.0}\right) + \frac{t}{\left(z \cdot 3.0\right) \cdot y}\]
2. Using strategy rm
3. Applied associate-/r*3.1
  \[\leadsto \left(x - \frac{y}{z \cdot 3.0}\right) + \color{blue}{\frac{\frac{t}{z \cdot 3.0}}{y}}\]
4. Using strategy rm
5. Applied div-inv3.2
  \[\leadsto \left(x - \frac{y}{z \cdot 3.0}\right) + \color{blue}{\frac{t}{z \cdot 3.0} \cdot \frac{1}{y}}\]
6. Using strategy rm
7. Applied associate-/r*3.2
  \[\leadsto \left(x - \frac{y}{z \cdot 3.0}\right) + \color{blue}{\frac{\frac{t}{z}}{3.0}} \cdot \frac{1}{y}\]
8. Using strategy rm
9. Applied associate-*l/3.2
  \[\leadsto \left(x - \frac{y}{z \cdot 3.0}\right) + \color{blue}{\frac{\frac{t}{z} \cdot \frac{1}{y}}{3.0}}\]
10. Simplified0.3
  \[\leadsto \left(x - \frac{y}{z \cdot 3.0}\right) + \frac{\color{blue}{\frac{\frac{t}{y}}{z}}}{3.0}\]
if 2.750296502407607e+21 < z
1. Initial program 0.4
  \[\left(x - \frac{y}{z \cdot 3.0}\right) + \frac{t}{\left(z \cdot 3.0\right) \cdot y}\]
2. Using strategy rm
3. Applied associate-/r*1.1
  \[\leadsto \left(x - \frac{y}{z \cdot 3.0}\right) + \color{blue}{\frac{\frac{t}{z \cdot 3.0}}{y}}\]
4. Taylor expanded around 0 0.4
  \[\leadsto \color{blue}{\left(x + 0.3333333333333333 \cdot \frac{t}{z \cdot y}\right) - 0.3333333333333333 \cdot \frac{y}{z}}\]
5. Simplified0.4
  \[\leadsto \color{blue}{x + 0.3333333333333333 \cdot \left(\frac{t}{y \cdot z} - \frac{y}{z}\right)}\]
Recombined 3 regimes into one program.
Final simplification0.6
\[\leadsto \begin{array}{l} \mathbf{if}\;z \le -1.5020866955626825 \cdot 10^{-30}:\\ \;\;\;\;\left(x - \frac{y}{3.0} \cdot \frac{1}{z}\right) + \frac{\frac{t}{3.0 \cdot z}}{y}\\ \mathbf{elif}\;z \le 2.750296502407607 \cdot 10^{+21}:\\ \;\;\;\;\frac{\frac{\frac{t}{y}}{z}}{3.0} + \left(x - \frac{y}{3.0 \cdot z}\right)\\ \mathbf{else}:\\ \;\;\;\;x + \left(\frac{t}{z \cdot y} - \frac{y}{z}\right) \cdot 0.3333333333333333\\ \end{array}\]

Error

Try it out

Target

Derivation

`if z < -1.5020866955626825e-30`

`if -1.5020866955626825e-30 < z < 2.750296502407607e+21`

`if 2.750296502407607e+21 < z`

Reproduce

In
Out