\[\left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \left(a \cdot 27\right) \cdot b\]

↓

\[\begin{array}{l} \mathbf{if}\;\left(y \cdot 9\right) \cdot z \le -3.8672592931070556 \cdot 10^{204} \lor \neg \left(\left(y \cdot 9\right) \cdot z \le 1.4897412691355755 \cdot 10^{307}\right):\\ \;\;\;\;x \cdot 2 + \left(27 \cdot \left(a \cdot b\right) - \left(y \cdot 9\right) \cdot \left(z \cdot t\right)\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot 2 + \left(27 \cdot \left(a \cdot b\right) - 9 \cdot \left(t \cdot \left(z \cdot y\right)\right)\right)\\ \end{array}\]

\left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \left(a \cdot 27\right) \cdot b

↓

\begin{array}{l}
\mathbf{if}\;\left(y \cdot 9\right) \cdot z \le -3.8672592931070556 \cdot 10^{204} \lor \neg \left(\left(y \cdot 9\right) \cdot z \le 1.4897412691355755 \cdot 10^{307}\right):\\
\;\;\;\;x \cdot 2 + \left(27 \cdot \left(a \cdot b\right) - \left(y \cdot 9\right) \cdot \left(z \cdot t\right)\right)\\

\mathbf{else}:\\
\;\;\;\;x \cdot 2 + \left(27 \cdot \left(a \cdot b\right) - 9 \cdot \left(t \cdot \left(z \cdot y\right)\right)\right)\\

\end{array}

double f(double x, double y, double z, double t, double a, double b) {
        double r864160 = x;
        double r864161 = 2.0;
        double r864162 = r864160 * r864161;
        double r864163 = y;
        double r864164 = 9.0;
        double r864165 = r864163 * r864164;
        double r864166 = z;
        double r864167 = r864165 * r864166;
        double r864168 = t;
        double r864169 = r864167 * r864168;
        double r864170 = r864162 - r864169;
        double r864171 = a;
        double r864172 = 27.0;
        double r864173 = r864171 * r864172;
        double r864174 = b;
        double r864175 = r864173 * r864174;
        double r864176 = r864170 + r864175;
        return r864176;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r864177 = y;
        double r864178 = 9.0;
        double r864179 = r864177 * r864178;
        double r864180 = z;
        double r864181 = r864179 * r864180;
        double r864182 = -3.8672592931070556e+204;
        bool r864183 = r864181 <= r864182;
        double r864184 = 1.4897412691355755e+307;
        bool r864185 = r864181 <= r864184;
        double r864186 = !r864185;
        bool r864187 = r864183 || r864186;
        double r864188 = x;
        double r864189 = 2.0;
        double r864190 = r864188 * r864189;
        double r864191 = 27.0;
        double r864192 = a;
        double r864193 = b;
        double r864194 = r864192 * r864193;
        double r864195 = r864191 * r864194;
        double r864196 = t;
        double r864197 = r864180 * r864196;
        double r864198 = r864179 * r864197;
        double r864199 = r864195 - r864198;
        double r864200 = r864190 + r864199;
        double r864201 = r864180 * r864177;
        double r864202 = r864196 * r864201;
        double r864203 = r864178 * r864202;
        double r864204 = r864195 - r864203;
        double r864205 = r864190 + r864204;
        double r864206 = r864187 ? r864200 : r864205;
        return r864206;
}

Original	3.4
Target	2.4
Herbie	0.4

Derivation

Split input into 2 regimes
if (* (* y 9.0) z) < -3.8672592931070556e+204 or 1.4897412691355755e+307 < (* (* y 9.0) z)
1. Initial program 36.2
  \[\left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \left(a \cdot 27\right) \cdot b\]
2. Using strategy rm
3. Applied sub-neg36.2
  \[\leadsto \color{blue}{\left(x \cdot 2 + \left(-\left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right)\right)} + \left(a \cdot 27\right) \cdot b\]
4. Applied associate-+l+36.2
  \[\leadsto \color{blue}{x \cdot 2 + \left(\left(-\left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \left(a \cdot 27\right) \cdot b\right)}\]
5. Simplified36.0
  \[\leadsto x \cdot 2 + \color{blue}{\left(27 \cdot \left(a \cdot b\right) - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right)}\]
6. Using strategy rm
7. Applied associate-*l*1.8
  \[\leadsto x \cdot 2 + \left(27 \cdot \left(a \cdot b\right) - \color{blue}{\left(y \cdot 9\right) \cdot \left(z \cdot t\right)}\right)\]
if -3.8672592931070556e+204 < (* (* y 9.0) z) < 1.4897412691355755e+307
1. Initial program 0.4
  \[\left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \left(a \cdot 27\right) \cdot b\]
2. Using strategy rm
3. Applied sub-neg0.4
  \[\leadsto \color{blue}{\left(x \cdot 2 + \left(-\left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right)\right)} + \left(a \cdot 27\right) \cdot b\]
4. Applied associate-+l+0.4
  \[\leadsto \color{blue}{x \cdot 2 + \left(\left(-\left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \left(a \cdot 27\right) \cdot b\right)}\]
5. Simplified0.3
  \[\leadsto x \cdot 2 + \color{blue}{\left(27 \cdot \left(a \cdot b\right) - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right)}\]
6. Taylor expanded around inf 0.3
  \[\leadsto x \cdot 2 + \color{blue}{\left(27 \cdot \left(a \cdot b\right) - 9 \cdot \left(t \cdot \left(z \cdot y\right)\right)\right)}\]
Recombined 2 regimes into one program.
Final simplification0.4
\[\leadsto \begin{array}{l} \mathbf{if}\;\left(y \cdot 9\right) \cdot z \le -3.8672592931070556 \cdot 10^{204} \lor \neg \left(\left(y \cdot 9\right) \cdot z \le 1.4897412691355755 \cdot 10^{307}\right):\\ \;\;\;\;x \cdot 2 + \left(27 \cdot \left(a \cdot b\right) - \left(y \cdot 9\right) \cdot \left(z \cdot t\right)\right)\\ \mathbf{else}:\\ \;\;\;\;x \cdot 2 + \left(27 \cdot \left(a \cdot b\right) - 9 \cdot \left(t \cdot \left(z \cdot y\right)\right)\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if (* (* y 9.0) z) < -3.8672592931070556e+204 or 1.4897412691355755e+307 < (* (* y 9.0) z)`

`if -3.8672592931070556e+204 < (* (* y 9.0) z) < 1.4897412691355755e+307`

Reproduce

In
Out