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

↓

\[\begin{array}{l} \mathbf{if}\;x \cdot y - z \cdot y \le -1.2854242699176415 \cdot 10^{155} \lor \neg \left(x \cdot y - z \cdot y \le 1.13733664130517669 \cdot 10^{211}\right):\\ \;\;\;\;y \cdot \left(\left(x - z\right) \cdot t\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(1 \cdot {\left(\sqrt[3]{x}\right)}^{3} + \left(-z\right)\right) \cdot y\right) \cdot t + \left(\mathsf{fma}\left(-z, 1, z\right) \cdot y\right) \cdot t\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;x \cdot y - z \cdot y \le -1.2854242699176415 \cdot 10^{155} \lor \neg \left(x \cdot y - z \cdot y \le 1.13733664130517669 \cdot 10^{211}\right):\\
\;\;\;\;y \cdot \left(\left(x - z\right) \cdot t\right)\\

\mathbf{else}:\\
\;\;\;\;\left(\left(1 \cdot {\left(\sqrt[3]{x}\right)}^{3} + \left(-z\right)\right) \cdot y\right) \cdot t + \left(\mathsf{fma}\left(-z, 1, z\right) \cdot y\right) \cdot t\\

\end{array}

double f(double x, double y, double z, double t) {
        double r808527 = x;
        double r808528 = y;
        double r808529 = r808527 * r808528;
        double r808530 = z;
        double r808531 = r808530 * r808528;
        double r808532 = r808529 - r808531;
        double r808533 = t;
        double r808534 = r808532 * r808533;
        return r808534;
}

↓

double f(double x, double y, double z, double t) {
        double r808535 = x;
        double r808536 = y;
        double r808537 = r808535 * r808536;
        double r808538 = z;
        double r808539 = r808538 * r808536;
        double r808540 = r808537 - r808539;
        double r808541 = -1.2854242699176415e+155;
        bool r808542 = r808540 <= r808541;
        double r808543 = 1.1373366413051767e+211;
        bool r808544 = r808540 <= r808543;
        double r808545 = !r808544;
        bool r808546 = r808542 || r808545;
        double r808547 = r808535 - r808538;
        double r808548 = t;
        double r808549 = r808547 * r808548;
        double r808550 = r808536 * r808549;
        double r808551 = 1.0;
        double r808552 = cbrt(r808535);
        double r808553 = 3.0;
        double r808554 = pow(r808552, r808553);
        double r808555 = r808551 * r808554;
        double r808556 = -r808538;
        double r808557 = r808555 + r808556;
        double r808558 = r808557 * r808536;
        double r808559 = r808558 * r808548;
        double r808560 = fma(r808556, r808551, r808538);
        double r808561 = r808560 * r808536;
        double r808562 = r808561 * r808548;
        double r808563 = r808559 + r808562;
        double r808564 = r808546 ? r808550 : r808563;
        return r808564;
}

Original	7.1
Target	3.0
Herbie	1.9

Derivation

Split input into 2 regimes
if (- (* x y) (* z y)) < -1.2854242699176415e+155 or 1.1373366413051767e+211 < (- (* x y) (* z y))
1. Initial program 24.9
  \[\left(x \cdot y - z \cdot y\right) \cdot t\]
2. Using strategy rm
3. Applied distribute-rgt-out--24.9
  \[\leadsto \color{blue}{\left(y \cdot \left(x - z\right)\right)} \cdot t\]
4. Applied associate-*l*1.4
  \[\leadsto \color{blue}{y \cdot \left(\left(x - z\right) \cdot t\right)}\]
if -1.2854242699176415e+155 < (- (* x y) (* z y)) < 1.1373366413051767e+211
1. Initial program 1.6
  \[\left(x \cdot y - z \cdot y\right) \cdot t\]
2. Taylor expanded around inf 1.6
  \[\leadsto \color{blue}{t \cdot \left(x \cdot y\right) - t \cdot \left(z \cdot y\right)}\]
3. Simplified8.4
  \[\leadsto \color{blue}{\left(t \cdot y\right) \cdot \left(x - z\right)}\]
4. Using strategy rm
5. Applied add-cube-cbrt8.8
  \[\leadsto \left(t \cdot y\right) \cdot \left(x - \color{blue}{\left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \sqrt[3]{z}}\right)\]
6. Applied add-cube-cbrt9.2
  \[\leadsto \left(t \cdot y\right) \cdot \left(\color{blue}{\left(\sqrt[3]{x} \cdot \sqrt[3]{x}\right) \cdot \sqrt[3]{x}} - \left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \sqrt[3]{z}\right)\]
7. Applied prod-diff9.2
  \[\leadsto \left(t \cdot y\right) \cdot \color{blue}{\left(\mathsf{fma}\left(\sqrt[3]{x} \cdot \sqrt[3]{x}, \sqrt[3]{x}, -\sqrt[3]{z} \cdot \left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right)\right) + \mathsf{fma}\left(-\sqrt[3]{z}, \sqrt[3]{z} \cdot \sqrt[3]{z}, \sqrt[3]{z} \cdot \left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right)\right)\right)}\]
8. Applied distribute-lft-in9.2
  \[\leadsto \color{blue}{\left(t \cdot y\right) \cdot \mathsf{fma}\left(\sqrt[3]{x} \cdot \sqrt[3]{x}, \sqrt[3]{x}, -\sqrt[3]{z} \cdot \left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right)\right) + \left(t \cdot y\right) \cdot \mathsf{fma}\left(-\sqrt[3]{z}, \sqrt[3]{z} \cdot \sqrt[3]{z}, \sqrt[3]{z} \cdot \left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right)\right)}\]
9. Simplified3.9
  \[\leadsto \color{blue}{\left(\left(1 \cdot {\left(\sqrt[3]{x}\right)}^{3} + \left(-z\right)\right) \cdot y\right) \cdot t} + \left(t \cdot y\right) \cdot \mathsf{fma}\left(-\sqrt[3]{z}, \sqrt[3]{z} \cdot \sqrt[3]{z}, \sqrt[3]{z} \cdot \left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right)\right)\]
10. Simplified2.1
  \[\leadsto \left(\left(1 \cdot {\left(\sqrt[3]{x}\right)}^{3} + \left(-z\right)\right) \cdot y\right) \cdot t + \color{blue}{\left(\mathsf{fma}\left(-z, 1, z\right) \cdot y\right) \cdot t}\]
Recombined 2 regimes into one program.
Final simplification1.9
\[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y - z \cdot y \le -1.2854242699176415 \cdot 10^{155} \lor \neg \left(x \cdot y - z \cdot y \le 1.13733664130517669 \cdot 10^{211}\right):\\ \;\;\;\;y \cdot \left(\left(x - z\right) \cdot t\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(1 \cdot {\left(\sqrt[3]{x}\right)}^{3} + \left(-z\right)\right) \cdot y\right) \cdot t + \left(\mathsf{fma}\left(-z, 1, z\right) \cdot y\right) \cdot t\\ \end{array}\]

Error

Target

Derivation

`if (- (* x y) (* z y)) < -1.2854242699176415e+155 or 1.1373366413051767e+211 < (- (* x y) (* z y))`

`if -1.2854242699176415e+155 < (- (* x y) (* z y)) < 1.1373366413051767e+211`

Reproduce