\[\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 2.800494683264158 \cdot 10^{208}\right):\\ \;\;\;\;\mathsf{fma}\left(a, 27 \cdot b, x \cdot 2 - \left(y \cdot 9\right) \cdot \left(z \cdot t\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(2 \cdot x - 9 \cdot \left(t \cdot \left(z \cdot y\right)\right)\right) + \left(\left(y \cdot 9\right) \cdot z\right) \cdot \left(\left(-t\right) + t\right)\right) + \left(a \cdot 27\right) \cdot b\\ \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 2.800494683264158 \cdot 10^{208}\right):\\
\;\;\;\;\mathsf{fma}\left(a, 27 \cdot b, x \cdot 2 - \left(y \cdot 9\right) \cdot \left(z \cdot t\right)\right)\\

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

\end{array}

double f(double x, double y, double z, double t, double a, double b) {
        double r827598 = x;
        double r827599 = 2.0;
        double r827600 = r827598 * r827599;
        double r827601 = y;
        double r827602 = 9.0;
        double r827603 = r827601 * r827602;
        double r827604 = z;
        double r827605 = r827603 * r827604;
        double r827606 = t;
        double r827607 = r827605 * r827606;
        double r827608 = r827600 - r827607;
        double r827609 = a;
        double r827610 = 27.0;
        double r827611 = r827609 * r827610;
        double r827612 = b;
        double r827613 = r827611 * r827612;
        double r827614 = r827608 + r827613;
        return r827614;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r827615 = y;
        double r827616 = 9.0;
        double r827617 = r827615 * r827616;
        double r827618 = z;
        double r827619 = r827617 * r827618;
        double r827620 = -inf.0;
        bool r827621 = r827619 <= r827620;
        double r827622 = 2.800494683264158e+208;
        bool r827623 = r827619 <= r827622;
        double r827624 = !r827623;
        bool r827625 = r827621 || r827624;
        double r827626 = a;
        double r827627 = 27.0;
        double r827628 = b;
        double r827629 = r827627 * r827628;
        double r827630 = x;
        double r827631 = 2.0;
        double r827632 = r827630 * r827631;
        double r827633 = t;
        double r827634 = r827618 * r827633;
        double r827635 = r827617 * r827634;
        double r827636 = r827632 - r827635;
        double r827637 = fma(r827626, r827629, r827636);
        double r827638 = r827631 * r827630;
        double r827639 = r827618 * r827615;
        double r827640 = r827633 * r827639;
        double r827641 = r827616 * r827640;
        double r827642 = r827638 - r827641;
        double r827643 = -r827633;
        double r827644 = r827643 + r827633;
        double r827645 = r827619 * r827644;
        double r827646 = r827642 + r827645;
        double r827647 = r827626 * r827627;
        double r827648 = r827647 * r827628;
        double r827649 = r827646 + r827648;
        double r827650 = r827625 ? r827637 : r827649;
        return r827650;
}

Original	3.7
Target	2.6
Herbie	0.5

Derivation

Split input into 2 regimes
if (* (* y 9.0) z) < -inf.0 or 2.800494683264158e+208 < (* (* y 9.0) z)
1. Initial program 39.8
  \[\left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \left(a \cdot 27\right) \cdot b\]
2. Simplified39.8
  \[\leadsto \color{blue}{\mathsf{fma}\left(a, 27 \cdot b, x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right)}\]
3. Using strategy rm
4. Applied associate-*l*0.7
  \[\leadsto \mathsf{fma}\left(a, 27 \cdot b, x \cdot 2 - \color{blue}{\left(y \cdot 9\right) \cdot \left(z \cdot t\right)}\right)\]
if -inf.0 < (* (* y 9.0) z) < 2.800494683264158e+208
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 prod-diff0.5
  \[\leadsto \color{blue}{\left(\mathsf{fma}\left(x, 2, -t \cdot \left(\left(y \cdot 9\right) \cdot z\right)\right) + \mathsf{fma}\left(-t, \left(y \cdot 9\right) \cdot z, t \cdot \left(\left(y \cdot 9\right) \cdot z\right)\right)\right)} + \left(a \cdot 27\right) \cdot b\]
4. Simplified0.5
  \[\leadsto \left(\color{blue}{\left(2 \cdot x - 9 \cdot \left(t \cdot \left(z \cdot y\right)\right)\right)} + \mathsf{fma}\left(-t, \left(y \cdot 9\right) \cdot z, t \cdot \left(\left(y \cdot 9\right) \cdot z\right)\right)\right) + \left(a \cdot 27\right) \cdot b\]
5. Simplified0.5
  \[\leadsto \left(\left(2 \cdot x - 9 \cdot \left(t \cdot \left(z \cdot y\right)\right)\right) + \color{blue}{\left(\left(y \cdot 9\right) \cdot z\right) \cdot \left(\left(-t\right) + t\right)}\right) + \left(a \cdot 27\right) \cdot b\]
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 2.800494683264158 \cdot 10^{208}\right):\\ \;\;\;\;\mathsf{fma}\left(a, 27 \cdot b, x \cdot 2 - \left(y \cdot 9\right) \cdot \left(z \cdot t\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(2 \cdot x - 9 \cdot \left(t \cdot \left(z \cdot y\right)\right)\right) + \left(\left(y \cdot 9\right) \cdot z\right) \cdot \left(\left(-t\right) + t\right)\right) + \left(a \cdot 27\right) \cdot b\\ \end{array}\]

Error

Target

Derivation

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

`if -inf.0 < (* (* y 9.0) z) < 2.800494683264158e+208`

Reproduce