\[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right)\]

↓

\[\begin{array}{l} \mathbf{if}\;z \le -1.328483031098398643944942670822321695646 \cdot 10^{154} \lor \neg \left(z \le 1.330402610121395417458956605059713968008 \cdot 10^{154}\right):\\ \;\;\;\;\mathsf{fma}\left(x, x, \left(\left(y \cdot 4\right) \cdot \left(\sqrt{t} + z\right)\right) \cdot \left(\sqrt{t} - z\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x, x, \left(y \cdot 4\right) \cdot \left(t - z \cdot z\right) + \left(y \cdot 4\right) \cdot \mathsf{fma}\left(-z, z, z \cdot z\right)\right)\\ \end{array}\]

x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right)

↓

\begin{array}{l}
\mathbf{if}\;z \le -1.328483031098398643944942670822321695646 \cdot 10^{154} \lor \neg \left(z \le 1.330402610121395417458956605059713968008 \cdot 10^{154}\right):\\
\;\;\;\;\mathsf{fma}\left(x, x, \left(\left(y \cdot 4\right) \cdot \left(\sqrt{t} + z\right)\right) \cdot \left(\sqrt{t} - z\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(x, x, \left(y \cdot 4\right) \cdot \left(t - z \cdot z\right) + \left(y \cdot 4\right) \cdot \mathsf{fma}\left(-z, z, z \cdot z\right)\right)\\

\end{array}

double f(double x, double y, double z, double t) {
        double r777264 = x;
        double r777265 = r777264 * r777264;
        double r777266 = y;
        double r777267 = 4.0;
        double r777268 = r777266 * r777267;
        double r777269 = z;
        double r777270 = r777269 * r777269;
        double r777271 = t;
        double r777272 = r777270 - r777271;
        double r777273 = r777268 * r777272;
        double r777274 = r777265 - r777273;
        return r777274;
}

↓

double f(double x, double y, double z, double t) {
        double r777275 = z;
        double r777276 = -1.3284830310983986e+154;
        bool r777277 = r777275 <= r777276;
        double r777278 = 1.3304026101213954e+154;
        bool r777279 = r777275 <= r777278;
        double r777280 = !r777279;
        bool r777281 = r777277 || r777280;
        double r777282 = x;
        double r777283 = y;
        double r777284 = 4.0;
        double r777285 = r777283 * r777284;
        double r777286 = t;
        double r777287 = sqrt(r777286);
        double r777288 = r777287 + r777275;
        double r777289 = r777285 * r777288;
        double r777290 = r777287 - r777275;
        double r777291 = r777289 * r777290;
        double r777292 = fma(r777282, r777282, r777291);
        double r777293 = r777275 * r777275;
        double r777294 = r777286 - r777293;
        double r777295 = r777285 * r777294;
        double r777296 = -r777275;
        double r777297 = fma(r777296, r777275, r777293);
        double r777298 = r777285 * r777297;
        double r777299 = r777295 + r777298;
        double r777300 = fma(r777282, r777282, r777299);
        double r777301 = r777281 ? r777292 : r777300;
        return r777301;
}

Original	6.1
Target	6.0
Herbie	3.0

Derivation

Split input into 2 regimes
if z < -1.3284830310983986e+154 or 1.3304026101213954e+154 < z
1. Initial program 64.0
  \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right)\]
2. Simplified64.0
  \[\leadsto \color{blue}{\mathsf{fma}\left(x, x, \left(y \cdot 4\right) \cdot \left(t - z \cdot z\right)\right)}\]
3. Using strategy rm
4. Applied add-sqr-sqrt64.0
  \[\leadsto \mathsf{fma}\left(x, x, \left(y \cdot 4\right) \cdot \left(\color{blue}{\sqrt{t} \cdot \sqrt{t}} - z \cdot z\right)\right)\]
5. Applied difference-of-squares64.0
  \[\leadsto \mathsf{fma}\left(x, x, \left(y \cdot 4\right) \cdot \color{blue}{\left(\left(\sqrt{t} + z\right) \cdot \left(\sqrt{t} - z\right)\right)}\right)\]
6. Applied associate-*r*31.8
  \[\leadsto \mathsf{fma}\left(x, x, \color{blue}{\left(\left(y \cdot 4\right) \cdot \left(\sqrt{t} + z\right)\right) \cdot \left(\sqrt{t} - z\right)}\right)\]
if -1.3284830310983986e+154 < z < 1.3304026101213954e+154
1. Initial program 0.1
  \[x \cdot x - \left(y \cdot 4\right) \cdot \left(z \cdot z - t\right)\]
2. Simplified0.1
  \[\leadsto \color{blue}{\mathsf{fma}\left(x, x, \left(y \cdot 4\right) \cdot \left(t - z \cdot z\right)\right)}\]
3. Using strategy rm
4. Applied add-sqr-sqrt31.3
  \[\leadsto \mathsf{fma}\left(x, x, \left(y \cdot 4\right) \cdot \left(\color{blue}{\sqrt{t} \cdot \sqrt{t}} - z \cdot z\right)\right)\]
5. Applied prod-diff31.3
  \[\leadsto \mathsf{fma}\left(x, x, \left(y \cdot 4\right) \cdot \color{blue}{\left(\mathsf{fma}\left(\sqrt{t}, \sqrt{t}, -z \cdot z\right) + \mathsf{fma}\left(-z, z, z \cdot z\right)\right)}\right)\]
6. Applied distribute-lft-in31.3
  \[\leadsto \mathsf{fma}\left(x, x, \color{blue}{\left(y \cdot 4\right) \cdot \mathsf{fma}\left(\sqrt{t}, \sqrt{t}, -z \cdot z\right) + \left(y \cdot 4\right) \cdot \mathsf{fma}\left(-z, z, z \cdot z\right)}\right)\]
7. Simplified0.1
  \[\leadsto \mathsf{fma}\left(x, x, \color{blue}{\left(y \cdot 4\right) \cdot \left(t - z \cdot z\right)} + \left(y \cdot 4\right) \cdot \mathsf{fma}\left(-z, z, z \cdot z\right)\right)\]
Recombined 2 regimes into one program.
Final simplification3.0
\[\leadsto \begin{array}{l} \mathbf{if}\;z \le -1.328483031098398643944942670822321695646 \cdot 10^{154} \lor \neg \left(z \le 1.330402610121395417458956605059713968008 \cdot 10^{154}\right):\\ \;\;\;\;\mathsf{fma}\left(x, x, \left(\left(y \cdot 4\right) \cdot \left(\sqrt{t} + z\right)\right) \cdot \left(\sqrt{t} - z\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(x, x, \left(y \cdot 4\right) \cdot \left(t - z \cdot z\right) + \left(y \cdot 4\right) \cdot \mathsf{fma}\left(-z, z, z \cdot z\right)\right)\\ \end{array}\]

Error

Target

Derivation

`if z < -1.3284830310983986e+154 or 1.3304026101213954e+154 < z`

`if -1.3284830310983986e+154 < z < 1.3304026101213954e+154`

Reproduce