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

↓

\[\begin{array}{l} \mathbf{if}\;b \le -4.342962072183161763686249274375685878126 \cdot 10^{90}:\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + \left(t \cdot \left(j \cdot c\right) + \left(-i \cdot \left(j \cdot y\right)\right)\right)\\ \mathbf{elif}\;b \le 1.234552070064316728666303086170435366235 \cdot 10^{-278}:\\ \;\;\;\;\left(\left(y \cdot \left(z \cdot x\right) + \left(-a \cdot \left(x \cdot t\right)\right)\right) - \left(z \cdot \left(b \cdot c\right) + \left(-a \cdot \left(i \cdot b\right)\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\ \mathbf{elif}\;b \le 2.847169551403341668887341056609846141356 \cdot 10^{-224}:\\ \;\;\;\;\left(\left(\left(y \cdot z\right) \cdot x + \left(-t \cdot \left(x \cdot a\right)\right)\right) - \left(z \cdot \left(b \cdot c\right) + b \cdot \left(-i \cdot a\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\ \mathbf{elif}\;b \le 5.528046101523884974127325839682326929048 \cdot 10^{-20}:\\ \;\;\;\;\left(\left(y \cdot \left(z \cdot x\right) + \left(-a \cdot \left(x \cdot t\right)\right)\right) - \left(z \cdot \left(b \cdot c\right) + \left(-a \cdot \left(i \cdot b\right)\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, i \cdot a - c \cdot z, j \cdot \left(c \cdot t - i \cdot y\right)\right)\right)\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;b \le -4.342962072183161763686249274375685878126 \cdot 10^{90}:\\
\;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + \left(t \cdot \left(j \cdot c\right) + \left(-i \cdot \left(j \cdot y\right)\right)\right)\\

\mathbf{elif}\;b \le 1.234552070064316728666303086170435366235 \cdot 10^{-278}:\\
\;\;\;\;\left(\left(y \cdot \left(z \cdot x\right) + \left(-a \cdot \left(x \cdot t\right)\right)\right) - \left(z \cdot \left(b \cdot c\right) + \left(-a \cdot \left(i \cdot b\right)\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\

\mathbf{elif}\;b \le 2.847169551403341668887341056609846141356 \cdot 10^{-224}:\\
\;\;\;\;\left(\left(\left(y \cdot z\right) \cdot x + \left(-t \cdot \left(x \cdot a\right)\right)\right) - \left(z \cdot \left(b \cdot c\right) + b \cdot \left(-i \cdot a\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\

\mathbf{elif}\;b \le 5.528046101523884974127325839682326929048 \cdot 10^{-20}:\\
\;\;\;\;\left(\left(y \cdot \left(z \cdot x\right) + \left(-a \cdot \left(x \cdot t\right)\right)\right) - \left(z \cdot \left(b \cdot c\right) + \left(-a \cdot \left(i \cdot b\right)\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\

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

\end{array}

double f(double x, double y, double z, double t, double a, double b, double c, double i, double j) {
        double r370092 = x;
        double r370093 = y;
        double r370094 = z;
        double r370095 = r370093 * r370094;
        double r370096 = t;
        double r370097 = a;
        double r370098 = r370096 * r370097;
        double r370099 = r370095 - r370098;
        double r370100 = r370092 * r370099;
        double r370101 = b;
        double r370102 = c;
        double r370103 = r370102 * r370094;
        double r370104 = i;
        double r370105 = r370104 * r370097;
        double r370106 = r370103 - r370105;
        double r370107 = r370101 * r370106;
        double r370108 = r370100 - r370107;
        double r370109 = j;
        double r370110 = r370102 * r370096;
        double r370111 = r370104 * r370093;
        double r370112 = r370110 - r370111;
        double r370113 = r370109 * r370112;
        double r370114 = r370108 + r370113;
        return r370114;
}

↓

double f(double x, double y, double z, double t, double a, double b, double c, double i, double j) {
        double r370115 = b;
        double r370116 = -4.342962072183162e+90;
        bool r370117 = r370115 <= r370116;
        double r370118 = x;
        double r370119 = y;
        double r370120 = z;
        double r370121 = r370119 * r370120;
        double r370122 = t;
        double r370123 = a;
        double r370124 = r370122 * r370123;
        double r370125 = r370121 - r370124;
        double r370126 = r370118 * r370125;
        double r370127 = c;
        double r370128 = r370127 * r370120;
        double r370129 = i;
        double r370130 = r370129 * r370123;
        double r370131 = r370128 - r370130;
        double r370132 = r370115 * r370131;
        double r370133 = r370126 - r370132;
        double r370134 = j;
        double r370135 = r370134 * r370127;
        double r370136 = r370122 * r370135;
        double r370137 = r370134 * r370119;
        double r370138 = r370129 * r370137;
        double r370139 = -r370138;
        double r370140 = r370136 + r370139;
        double r370141 = r370133 + r370140;
        double r370142 = 1.2345520700643167e-278;
        bool r370143 = r370115 <= r370142;
        double r370144 = r370120 * r370118;
        double r370145 = r370119 * r370144;
        double r370146 = r370118 * r370122;
        double r370147 = r370123 * r370146;
        double r370148 = -r370147;
        double r370149 = r370145 + r370148;
        double r370150 = r370115 * r370127;
        double r370151 = r370120 * r370150;
        double r370152 = r370129 * r370115;
        double r370153 = r370123 * r370152;
        double r370154 = -r370153;
        double r370155 = r370151 + r370154;
        double r370156 = r370149 - r370155;
        double r370157 = r370127 * r370122;
        double r370158 = r370129 * r370119;
        double r370159 = r370157 - r370158;
        double r370160 = r370134 * r370159;
        double r370161 = r370156 + r370160;
        double r370162 = 2.8471695514033417e-224;
        bool r370163 = r370115 <= r370162;
        double r370164 = r370121 * r370118;
        double r370165 = r370118 * r370123;
        double r370166 = r370122 * r370165;
        double r370167 = -r370166;
        double r370168 = r370164 + r370167;
        double r370169 = -r370130;
        double r370170 = r370115 * r370169;
        double r370171 = r370151 + r370170;
        double r370172 = r370168 - r370171;
        double r370173 = r370172 + r370160;
        double r370174 = 5.528046101523885e-20;
        bool r370175 = r370115 <= r370174;
        double r370176 = r370130 - r370128;
        double r370177 = fma(r370115, r370176, r370160);
        double r370178 = fma(r370118, r370125, r370177);
        double r370179 = r370175 ? r370161 : r370178;
        double r370180 = r370163 ? r370173 : r370179;
        double r370181 = r370143 ? r370161 : r370180;
        double r370182 = r370117 ? r370141 : r370181;
        return r370182;
}

Original	12.5
Target	16.3
Herbie	9.7

Derivation

Split input into 4 regimes
if b < -4.342962072183162e+90
1. Initial program 7.0
  \[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
2. Using strategy rm
3. Applied sub-neg7.0
  \[\leadsto \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \color{blue}{\left(c \cdot t + \left(-i \cdot y\right)\right)}\]
4. Applied distribute-lft-in7.0
  \[\leadsto \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + \color{blue}{\left(j \cdot \left(c \cdot t\right) + j \cdot \left(-i \cdot y\right)\right)}\]
5. Simplified7.0
  \[\leadsto \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + \left(\color{blue}{t \cdot \left(j \cdot c\right)} + j \cdot \left(-i \cdot y\right)\right)\]
6. Simplified7.4
  \[\leadsto \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + \left(t \cdot \left(j \cdot c\right) + \color{blue}{\left(-i \cdot \left(j \cdot y\right)\right)}\right)\]
if -4.342962072183162e+90 < b < 1.2345520700643167e-278 or 2.8471695514033417e-224 < b < 5.528046101523885e-20
1. Initial program 14.6
  \[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
2. Using strategy rm
3. Applied sub-neg14.6
  \[\leadsto \left(x \cdot \color{blue}{\left(y \cdot z + \left(-t \cdot a\right)\right)} - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
4. Applied distribute-lft-in14.6
  \[\leadsto \left(\color{blue}{\left(x \cdot \left(y \cdot z\right) + x \cdot \left(-t \cdot a\right)\right)} - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
5. Simplified14.6
  \[\leadsto \left(\left(\color{blue}{\left(y \cdot z\right) \cdot x} + x \cdot \left(-t \cdot a\right)\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
6. Simplified14.5
  \[\leadsto \left(\left(\left(y \cdot z\right) \cdot x + \color{blue}{\left(-a \cdot \left(x \cdot t\right)\right)}\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
7. Using strategy rm
8. Applied sub-neg14.5
  \[\leadsto \left(\left(\left(y \cdot z\right) \cdot x + \left(-a \cdot \left(x \cdot t\right)\right)\right) - b \cdot \color{blue}{\left(c \cdot z + \left(-i \cdot a\right)\right)}\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
9. Applied distribute-lft-in14.5
  \[\leadsto \left(\left(\left(y \cdot z\right) \cdot x + \left(-a \cdot \left(x \cdot t\right)\right)\right) - \color{blue}{\left(b \cdot \left(c \cdot z\right) + b \cdot \left(-i \cdot a\right)\right)}\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
10. Simplified12.5
  \[\leadsto \left(\left(\left(y \cdot z\right) \cdot x + \left(-a \cdot \left(x \cdot t\right)\right)\right) - \left(\color{blue}{z \cdot \left(b \cdot c\right)} + b \cdot \left(-i \cdot a\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
11. Using strategy rm
12. Applied associate-*l*12.6
  \[\leadsto \left(\left(\color{blue}{y \cdot \left(z \cdot x\right)} + \left(-a \cdot \left(x \cdot t\right)\right)\right) - \left(z \cdot \left(b \cdot c\right) + b \cdot \left(-i \cdot a\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
13. Using strategy rm
14. Applied distribute-rgt-neg-out12.6
  \[\leadsto \left(\left(y \cdot \left(z \cdot x\right) + \left(-a \cdot \left(x \cdot t\right)\right)\right) - \left(z \cdot \left(b \cdot c\right) + \color{blue}{\left(-b \cdot \left(i \cdot a\right)\right)}\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
15. Simplified10.2
  \[\leadsto \left(\left(y \cdot \left(z \cdot x\right) + \left(-a \cdot \left(x \cdot t\right)\right)\right) - \left(z \cdot \left(b \cdot c\right) + \left(-\color{blue}{a \cdot \left(i \cdot b\right)}\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
if 1.2345520700643167e-278 < b < 2.8471695514033417e-224
1. Initial program 18.9
  \[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
2. Using strategy rm
3. Applied sub-neg18.9
  \[\leadsto \left(x \cdot \color{blue}{\left(y \cdot z + \left(-t \cdot a\right)\right)} - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
4. Applied distribute-lft-in19.0
  \[\leadsto \left(\color{blue}{\left(x \cdot \left(y \cdot z\right) + x \cdot \left(-t \cdot a\right)\right)} - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
5. Simplified19.0
  \[\leadsto \left(\left(\color{blue}{\left(y \cdot z\right) \cdot x} + x \cdot \left(-t \cdot a\right)\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
6. Simplified19.7
  \[\leadsto \left(\left(\left(y \cdot z\right) \cdot x + \color{blue}{\left(-a \cdot \left(x \cdot t\right)\right)}\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
7. Using strategy rm
8. Applied sub-neg19.7
  \[\leadsto \left(\left(\left(y \cdot z\right) \cdot x + \left(-a \cdot \left(x \cdot t\right)\right)\right) - b \cdot \color{blue}{\left(c \cdot z + \left(-i \cdot a\right)\right)}\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
9. Applied distribute-lft-in19.7
  \[\leadsto \left(\left(\left(y \cdot z\right) \cdot x + \left(-a \cdot \left(x \cdot t\right)\right)\right) - \color{blue}{\left(b \cdot \left(c \cdot z\right) + b \cdot \left(-i \cdot a\right)\right)}\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
10. Simplified15.9
  \[\leadsto \left(\left(\left(y \cdot z\right) \cdot x + \left(-a \cdot \left(x \cdot t\right)\right)\right) - \left(\color{blue}{z \cdot \left(b \cdot c\right)} + b \cdot \left(-i \cdot a\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
11. Taylor expanded around inf 15.8
  \[\leadsto \left(\left(\left(y \cdot z\right) \cdot x + \left(-\color{blue}{t \cdot \left(x \cdot a\right)}\right)\right) - \left(z \cdot \left(b \cdot c\right) + b \cdot \left(-i \cdot a\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
if 5.528046101523885e-20 < b
1. Initial program 7.9
  \[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
2. Simplified7.9
  \[\leadsto \color{blue}{\mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, i \cdot a - c \cdot z, j \cdot \left(c \cdot t - i \cdot y\right)\right)\right)}\]
Recombined 4 regimes into one program.
Final simplification9.7
\[\leadsto \begin{array}{l} \mathbf{if}\;b \le -4.342962072183161763686249274375685878126 \cdot 10^{90}:\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + \left(t \cdot \left(j \cdot c\right) + \left(-i \cdot \left(j \cdot y\right)\right)\right)\\ \mathbf{elif}\;b \le 1.234552070064316728666303086170435366235 \cdot 10^{-278}:\\ \;\;\;\;\left(\left(y \cdot \left(z \cdot x\right) + \left(-a \cdot \left(x \cdot t\right)\right)\right) - \left(z \cdot \left(b \cdot c\right) + \left(-a \cdot \left(i \cdot b\right)\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\ \mathbf{elif}\;b \le 2.847169551403341668887341056609846141356 \cdot 10^{-224}:\\ \;\;\;\;\left(\left(\left(y \cdot z\right) \cdot x + \left(-t \cdot \left(x \cdot a\right)\right)\right) - \left(z \cdot \left(b \cdot c\right) + b \cdot \left(-i \cdot a\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\ \mathbf{elif}\;b \le 5.528046101523884974127325839682326929048 \cdot 10^{-20}:\\ \;\;\;\;\left(\left(y \cdot \left(z \cdot x\right) + \left(-a \cdot \left(x \cdot t\right)\right)\right) - \left(z \cdot \left(b \cdot c\right) + \left(-a \cdot \left(i \cdot b\right)\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, i \cdot a - c \cdot z, j \cdot \left(c \cdot t - i \cdot y\right)\right)\right)\\ \end{array}\]

Error

Target

Derivation

`if b < -4.342962072183162e+90`

`if -4.342962072183162e+90 < b < 1.2345520700643167e-278 or 2.8471695514033417e-224 < b < 5.528046101523885e-20`

`if 1.2345520700643167e-278 < b < 2.8471695514033417e-224`

`if 5.528046101523885e-20 < b`

Reproduce