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

↓

\[\begin{array}{l} \mathbf{if}\;c \le -1402975549009292.5 \lor \neg \left(c \le 15766461.9554172419011592864990234375\right):\\ \;\;\;\;2 \cdot \mathsf{fma}\left(y, x, \mathsf{fma}\left(z, t, -\left(\mathsf{fma}\left(c, b, a\right) \cdot i\right) \cdot c\right) + \left(\mathsf{fma}\left(c, b, a\right) \cdot i\right) \cdot \left(\left(-c\right) + c\right)\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(y, x, z \cdot t - \left(c \cdot \mathsf{fma}\left(c, b, a\right)\right) \cdot i\right)\\ \end{array}\]

2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)

↓

\begin{array}{l}
\mathbf{if}\;c \le -1402975549009292.5 \lor \neg \left(c \le 15766461.9554172419011592864990234375\right):\\
\;\;\;\;2 \cdot \mathsf{fma}\left(y, x, \mathsf{fma}\left(z, t, -\left(\mathsf{fma}\left(c, b, a\right) \cdot i\right) \cdot c\right) + \left(\mathsf{fma}\left(c, b, a\right) \cdot i\right) \cdot \left(\left(-c\right) + c\right)\right)\\

\mathbf{else}:\\
\;\;\;\;2 \cdot \mathsf{fma}\left(y, x, z \cdot t - \left(c \cdot \mathsf{fma}\left(c, b, a\right)\right) \cdot i\right)\\

\end{array}

double f(double x, double y, double z, double t, double a, double b, double c, double i) {
        double r914125 = 2.0;
        double r914126 = x;
        double r914127 = y;
        double r914128 = r914126 * r914127;
        double r914129 = z;
        double r914130 = t;
        double r914131 = r914129 * r914130;
        double r914132 = r914128 + r914131;
        double r914133 = a;
        double r914134 = b;
        double r914135 = c;
        double r914136 = r914134 * r914135;
        double r914137 = r914133 + r914136;
        double r914138 = r914137 * r914135;
        double r914139 = i;
        double r914140 = r914138 * r914139;
        double r914141 = r914132 - r914140;
        double r914142 = r914125 * r914141;
        return r914142;
}

↓

double f(double x, double y, double z, double t, double a, double b, double c, double i) {
        double r914143 = c;
        double r914144 = -1402975549009292.5;
        bool r914145 = r914143 <= r914144;
        double r914146 = 15766461.955417242;
        bool r914147 = r914143 <= r914146;
        double r914148 = !r914147;
        bool r914149 = r914145 || r914148;
        double r914150 = 2.0;
        double r914151 = y;
        double r914152 = x;
        double r914153 = z;
        double r914154 = t;
        double r914155 = b;
        double r914156 = a;
        double r914157 = fma(r914143, r914155, r914156);
        double r914158 = i;
        double r914159 = r914157 * r914158;
        double r914160 = r914159 * r914143;
        double r914161 = -r914160;
        double r914162 = fma(r914153, r914154, r914161);
        double r914163 = -r914143;
        double r914164 = r914163 + r914143;
        double r914165 = r914159 * r914164;
        double r914166 = r914162 + r914165;
        double r914167 = fma(r914151, r914152, r914166);
        double r914168 = r914150 * r914167;
        double r914169 = r914153 * r914154;
        double r914170 = r914143 * r914157;
        double r914171 = r914170 * r914158;
        double r914172 = r914169 - r914171;
        double r914173 = fma(r914151, r914152, r914172);
        double r914174 = r914150 * r914173;
        double r914175 = r914149 ? r914168 : r914174;
        return r914175;
}

Original	6.6
Target	2.0
Herbie	1.5

Derivation

Split input into 2 regimes
if c < -1402975549009292.5 or 15766461.955417242 < c
1. Initial program 21.0
  \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\]
2. Simplified21.0
  \[\leadsto \color{blue}{2 \cdot \mathsf{fma}\left(y, x, z \cdot t - \left(c \cdot \mathsf{fma}\left(c, b, a\right)\right) \cdot i\right)}\]
3. Using strategy rm
4. Applied associate-*l*3.9
  \[\leadsto 2 \cdot \mathsf{fma}\left(y, x, z \cdot t - \color{blue}{c \cdot \left(\mathsf{fma}\left(c, b, a\right) \cdot i\right)}\right)\]
5. Using strategy rm
6. Applied prod-diff3.9
  \[\leadsto 2 \cdot \mathsf{fma}\left(y, x, \color{blue}{\mathsf{fma}\left(z, t, -\left(\mathsf{fma}\left(c, b, a\right) \cdot i\right) \cdot c\right) + \mathsf{fma}\left(-\mathsf{fma}\left(c, b, a\right) \cdot i, c, \left(\mathsf{fma}\left(c, b, a\right) \cdot i\right) \cdot c\right)}\right)\]
7. Simplified3.9
  \[\leadsto 2 \cdot \mathsf{fma}\left(y, x, \mathsf{fma}\left(z, t, -\left(\mathsf{fma}\left(c, b, a\right) \cdot i\right) \cdot c\right) + \color{blue}{\left(\mathsf{fma}\left(c, b, a\right) \cdot i\right) \cdot \left(\left(-c\right) + c\right)}\right)\]
if -1402975549009292.5 < c < 15766461.955417242
1. Initial program 0.5
  \[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\]
2. Simplified0.5
  \[\leadsto \color{blue}{2 \cdot \mathsf{fma}\left(y, x, z \cdot t - \left(c \cdot \mathsf{fma}\left(c, b, a\right)\right) \cdot i\right)}\]
Recombined 2 regimes into one program.
Final simplification1.5
\[\leadsto \begin{array}{l} \mathbf{if}\;c \le -1402975549009292.5 \lor \neg \left(c \le 15766461.9554172419011592864990234375\right):\\ \;\;\;\;2 \cdot \mathsf{fma}\left(y, x, \mathsf{fma}\left(z, t, -\left(\mathsf{fma}\left(c, b, a\right) \cdot i\right) \cdot c\right) + \left(\mathsf{fma}\left(c, b, a\right) \cdot i\right) \cdot \left(\left(-c\right) + c\right)\right)\\ \mathbf{else}:\\ \;\;\;\;2 \cdot \mathsf{fma}\left(y, x, z \cdot t - \left(c \cdot \mathsf{fma}\left(c, b, a\right)\right) \cdot i\right)\\ \end{array}\]

Error

Target

Derivation

`if c < -1402975549009292.5 or 15766461.955417242 < c`

`if -1402975549009292.5 < c < 15766461.955417242`

Reproduce