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

\mathbf{else}:\\
\;\;\;\;\left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\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 r663854 = x;
        double r663855 = 2.0;
        double r663856 = r663854 * r663855;
        double r663857 = y;
        double r663858 = 9.0;
        double r663859 = r663857 * r663858;
        double r663860 = z;
        double r663861 = r663859 * r663860;
        double r663862 = t;
        double r663863 = r663861 * r663862;
        double r663864 = r663856 - r663863;
        double r663865 = a;
        double r663866 = 27.0;
        double r663867 = r663865 * r663866;
        double r663868 = b;
        double r663869 = r663867 * r663868;
        double r663870 = r663864 + r663869;
        return r663870;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r663871 = y;
        double r663872 = 9.0;
        double r663873 = r663871 * r663872;
        double r663874 = z;
        double r663875 = r663873 * r663874;
        double r663876 = -inf.0;
        bool r663877 = r663875 <= r663876;
        double r663878 = 4.927946119306124e-10;
        bool r663879 = r663875 <= r663878;
        double r663880 = !r663879;
        bool r663881 = r663877 || r663880;
        double r663882 = x;
        double r663883 = 2.0;
        double r663884 = r663882 * r663883;
        double r663885 = t;
        double r663886 = r663874 * r663885;
        double r663887 = r663873 * r663886;
        double r663888 = r663884 - r663887;
        double r663889 = 27.0;
        double r663890 = a;
        double r663891 = b;
        double r663892 = r663890 * r663891;
        double r663893 = r663889 * r663892;
        double r663894 = 1.0;
        double r663895 = pow(r663893, r663894);
        double r663896 = r663888 + r663895;
        double r663897 = r663875 * r663885;
        double r663898 = r663884 - r663897;
        double r663899 = r663889 * r663891;
        double r663900 = r663890 * r663899;
        double r663901 = r663898 + r663900;
        double r663902 = r663881 ? r663896 : r663901;
        return r663902;
}

Original	3.8
Target	2.5
Herbie	1.3

Derivation

Split input into 2 regimes
if (* (* y 9.0) z) < -inf.0 or 4.927946119306124e-10 < (* (* y 9.0) z)
1. Initial program 14.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 pow114.6
  \[\leadsto \left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \left(a \cdot 27\right) \cdot \color{blue}{{b}^{1}}\]
4. Applied pow114.6
  \[\leadsto \left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \left(a \cdot \color{blue}{{27}^{1}}\right) \cdot {b}^{1}\]
5. Applied pow114.6
  \[\leadsto \left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \left(\color{blue}{{a}^{1}} \cdot {27}^{1}\right) \cdot {b}^{1}\]
6. Applied pow-prod-down14.6
  \[\leadsto \left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \color{blue}{{\left(a \cdot 27\right)}^{1}} \cdot {b}^{1}\]
7. Applied pow-prod-down14.6
  \[\leadsto \left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \color{blue}{{\left(\left(a \cdot 27\right) \cdot b\right)}^{1}}\]
8. Simplified14.5
  \[\leadsto \left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + {\color{blue}{\left(27 \cdot \left(a \cdot b\right)\right)}}^{1}\]
9. Using strategy rm
10. Applied associate-*l*4.1
  \[\leadsto \left(x \cdot 2 - \color{blue}{\left(y \cdot 9\right) \cdot \left(z \cdot t\right)}\right) + {\left(27 \cdot \left(a \cdot b\right)\right)}^{1}\]
if -inf.0 < (* (* y 9.0) z) < 4.927946119306124e-10
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*0.4
  \[\leadsto \left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + \color{blue}{a \cdot \left(27 \cdot b\right)}\]
Recombined 2 regimes into one program.
Final simplification1.3
\[\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 4.9279461193061243 \cdot 10^{-10}\right):\\ \;\;\;\;\left(x \cdot 2 - \left(y \cdot 9\right) \cdot \left(z \cdot t\right)\right) + {\left(27 \cdot \left(a \cdot b\right)\right)}^{1}\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot 2 - \left(\left(y \cdot 9\right) \cdot z\right) \cdot t\right) + a \cdot \left(27 \cdot b\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if (* (* y 9.0) z) < -inf.0 or 4.927946119306124e-10 < (* (* y 9.0) z)`

`if -inf.0 < (* (* y 9.0) z) < 4.927946119306124e-10`

Reproduce

In
Out