\[\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 1.07579554652432578 \cdot 10^{266}\right):\\ \;\;\;\;\left(x \cdot 2 - y \cdot \left(\left(9 \cdot z\right) \cdot t\right)\right) + \left(\sqrt[3]{\left(a \cdot 27\right) \cdot b} \cdot \sqrt[3]{\left(a \cdot 27\right) \cdot b}\right) \cdot \sqrt[3]{\left(a \cdot 27\right) \cdot b}\\ \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 1.07579554652432578 \cdot 10^{266}\right):\\
\;\;\;\;\left(x \cdot 2 - y \cdot \left(\left(9 \cdot z\right) \cdot t\right)\right) + \left(\sqrt[3]{\left(a \cdot 27\right) \cdot b} \cdot \sqrt[3]{\left(a \cdot 27\right) \cdot b}\right) \cdot \sqrt[3]{\left(a \cdot 27\right) \cdot b}\\

\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 r816523 = x;
        double r816524 = 2.0;
        double r816525 = r816523 * r816524;
        double r816526 = y;
        double r816527 = 9.0;
        double r816528 = r816526 * r816527;
        double r816529 = z;
        double r816530 = r816528 * r816529;
        double r816531 = t;
        double r816532 = r816530 * r816531;
        double r816533 = r816525 - r816532;
        double r816534 = a;
        double r816535 = 27.0;
        double r816536 = r816534 * r816535;
        double r816537 = b;
        double r816538 = r816536 * r816537;
        double r816539 = r816533 + r816538;
        return r816539;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r816540 = y;
        double r816541 = 9.0;
        double r816542 = r816540 * r816541;
        double r816543 = z;
        double r816544 = r816542 * r816543;
        double r816545 = -inf.0;
        bool r816546 = r816544 <= r816545;
        double r816547 = 1.0757955465243258e+266;
        bool r816548 = r816544 <= r816547;
        double r816549 = !r816548;
        bool r816550 = r816546 || r816549;
        double r816551 = x;
        double r816552 = 2.0;
        double r816553 = r816551 * r816552;
        double r816554 = r816541 * r816543;
        double r816555 = t;
        double r816556 = r816554 * r816555;
        double r816557 = r816540 * r816556;
        double r816558 = r816553 - r816557;
        double r816559 = a;
        double r816560 = 27.0;
        double r816561 = r816559 * r816560;
        double r816562 = b;
        double r816563 = r816561 * r816562;
        double r816564 = cbrt(r816563);
        double r816565 = r816564 * r816564;
        double r816566 = r816565 * r816564;
        double r816567 = r816558 + r816566;
        double r816568 = r816544 * r816555;
        double r816569 = r816553 - r816568;
        double r816570 = r816560 * r816562;
        double r816571 = r816559 * r816570;
        double r816572 = r816569 + r816571;
        double r816573 = r816550 ? r816567 : r816572;
        return r816573;
}

Original	3.8
Target	2.6
Herbie	0.5

Derivation

Split input into 2 regimes
if (* (* y 9.0) z) < -inf.0 or 1.0757955465243258e+266 < (* (* y 9.0) z)
1. Initial program 53.3
  \[\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*2.0
  \[\leadsto \left(x \cdot 2 - \color{blue}{\left(y \cdot 9\right) \cdot \left(z \cdot t\right)}\right) + \left(a \cdot 27\right) \cdot b\]
4. Using strategy rm
5. Applied associate-*l*0.5
  \[\leadsto \left(x \cdot 2 - \color{blue}{y \cdot \left(9 \cdot \left(z \cdot t\right)\right)}\right) + \left(a \cdot 27\right) \cdot b\]
6. Using strategy rm
7. Applied associate-*r*0.5
  \[\leadsto \left(x \cdot 2 - y \cdot \color{blue}{\left(\left(9 \cdot z\right) \cdot t\right)}\right) + \left(a \cdot 27\right) \cdot b\]
8. Using strategy rm
9. Applied add-cube-cbrt0.7
  \[\leadsto \left(x \cdot 2 - y \cdot \left(\left(9 \cdot z\right) \cdot t\right)\right) + \color{blue}{\left(\sqrt[3]{\left(a \cdot 27\right) \cdot b} \cdot \sqrt[3]{\left(a \cdot 27\right) \cdot b}\right) \cdot \sqrt[3]{\left(a \cdot 27\right) \cdot b}}\]
if -inf.0 < (* (* y 9.0) z) < 1.0757955465243258e+266
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.5
  \[\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 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 1.07579554652432578 \cdot 10^{266}\right):\\ \;\;\;\;\left(x \cdot 2 - y \cdot \left(\left(9 \cdot z\right) \cdot t\right)\right) + \left(\sqrt[3]{\left(a \cdot 27\right) \cdot b} \cdot \sqrt[3]{\left(a \cdot 27\right) \cdot b}\right) \cdot \sqrt[3]{\left(a \cdot 27\right) \cdot b}\\ \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}\]

Falling back on racket egraph because egg-herbie package not installed (more)

Error

Try it out

Target

Derivation

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

`if -inf.0 < (* (* y 9.0) z) < 1.0757955465243258e+266`

Reproduce

In
Out