\[\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 = -\infty \lor \neg \left(\left(y \cdot 9\right) \cdot z \le 3.5690048196050708 \cdot 10^{279}\right):\\ \;\;\;\;\left(x \cdot 2 - y \cdot \left(9 \cdot \left(z \cdot t\right)\right)\right) + 27 \cdot \left(a \cdot b\right)\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot x - 9 \cdot \left(t \cdot \left(z \cdot y\right)\right)\right) + a \cdot \left(27 \cdot b\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 = -\infty \lor \neg \left(\left(y \cdot 9\right) \cdot z \le 3.5690048196050708 \cdot 10^{279}\right):\\
\;\;\;\;\left(x \cdot 2 - y \cdot \left(9 \cdot \left(z \cdot t\right)\right)\right) + 27 \cdot \left(a \cdot b\right)\\

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

\end{array}

double f(double x, double y, double z, double t, double a, double b) {
        double r786101 = x;
        double r786102 = 2.0;
        double r786103 = r786101 * r786102;
        double r786104 = y;
        double r786105 = 9.0;
        double r786106 = r786104 * r786105;
        double r786107 = z;
        double r786108 = r786106 * r786107;
        double r786109 = t;
        double r786110 = r786108 * r786109;
        double r786111 = r786103 - r786110;
        double r786112 = a;
        double r786113 = 27.0;
        double r786114 = r786112 * r786113;
        double r786115 = b;
        double r786116 = r786114 * r786115;
        double r786117 = r786111 + r786116;
        return r786117;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r786118 = y;
        double r786119 = 9.0;
        double r786120 = r786118 * r786119;
        double r786121 = z;
        double r786122 = r786120 * r786121;
        double r786123 = -inf.0;
        bool r786124 = r786122 <= r786123;
        double r786125 = 3.569004819605071e+279;
        bool r786126 = r786122 <= r786125;
        double r786127 = !r786126;
        bool r786128 = r786124 || r786127;
        double r786129 = x;
        double r786130 = 2.0;
        double r786131 = r786129 * r786130;
        double r786132 = t;
        double r786133 = r786121 * r786132;
        double r786134 = r786119 * r786133;
        double r786135 = r786118 * r786134;
        double r786136 = r786131 - r786135;
        double r786137 = 27.0;
        double r786138 = a;
        double r786139 = b;
        double r786140 = r786138 * r786139;
        double r786141 = r786137 * r786140;
        double r786142 = r786136 + r786141;
        double r786143 = r786130 * r786129;
        double r786144 = r786121 * r786118;
        double r786145 = r786132 * r786144;
        double r786146 = r786119 * r786145;
        double r786147 = r786143 - r786146;
        double r786148 = r786137 * r786139;
        double r786149 = r786138 * r786148;
        double r786150 = r786147 + r786149;
        double r786151 = r786128 ? r786142 : r786150;
        return r786151;
}

Original	3.5
Target	2.3
Herbie	0.5

Derivation

Split input into 2 regimes
if (* (* y 9.0) z) < -inf.0 or 3.569004819605071e+279 < (* (* y 9.0) z)
1. Initial program 54.6
  \[\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 associate-*l*1.9
  \[\leadsto \left(x \cdot 2 - \color{blue}{\left(y \cdot 9\right) \cdot \left(z \cdot t\right)}\right) + \left(a \cdot 27\right) \cdot b\]
4. Using strategy rm
5. Applied associate-*l*1.9
  \[\leadsto \left(x \cdot 2 - \left(y \cdot 9\right) \cdot \left(z \cdot t\right)\right) + \color{blue}{a \cdot \left(27 \cdot b\right)}\]
6. Taylor expanded around 0 1.7
  \[\leadsto \left(x \cdot 2 - \left(y \cdot 9\right) \cdot \left(z \cdot t\right)\right) + \color{blue}{27 \cdot \left(a \cdot b\right)}\]
7. Using strategy rm
8. Applied associate-*l*0.2
  \[\leadsto \left(x \cdot 2 - \color{blue}{y \cdot \left(9 \cdot \left(z \cdot t\right)\right)}\right) + 27 \cdot \left(a \cdot b\right)\]
if -inf.0 < (* (* y 9.0) z) < 3.569004819605071e+279
1. Initial program 0.5
  \[\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 associate-*l*3.6
  \[\leadsto \left(x \cdot 2 - \color{blue}{\left(y \cdot 9\right) \cdot \left(z \cdot t\right)}\right) + \left(a \cdot 27\right) \cdot b\]
4. Using strategy rm
5. Applied associate-*l*3.6
  \[\leadsto \left(x \cdot 2 - \left(y \cdot 9\right) \cdot \left(z \cdot t\right)\right) + \color{blue}{a \cdot \left(27 \cdot b\right)}\]
6. Taylor expanded around inf 0.5
  \[\leadsto \color{blue}{\left(2 \cdot x - 9 \cdot \left(t \cdot \left(z \cdot y\right)\right)\right)} + a \cdot \left(27 \cdot b\right)\]
Recombined 2 regimes into one program.
Final simplification0.5
\[\leadsto \begin{array}{l} \mathbf{if}\;\left(y \cdot 9\right) \cdot z = -\infty \lor \neg \left(\left(y \cdot 9\right) \cdot z \le 3.5690048196050708 \cdot 10^{279}\right):\\ \;\;\;\;\left(x \cdot 2 - y \cdot \left(9 \cdot \left(z \cdot t\right)\right)\right) + 27 \cdot \left(a \cdot b\right)\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot x - 9 \cdot \left(t \cdot \left(z \cdot y\right)\right)\right) + a \cdot \left(27 \cdot b\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if (* (* y 9.0) z) < -inf.0 or 3.569004819605071e+279 < (* (* y 9.0) z)`

`if -inf.0 < (* (* y 9.0) z) < 3.569004819605071e+279`

Reproduce

In
Out