\[\frac{a1 \cdot a2}{b1 \cdot b2}\]

↓

\[\begin{array}{l} \mathbf{if}\;\frac{a1 \cdot a2}{b1 \cdot b2} = -\infty \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \le -5.21092585859161966 \cdot 10^{-296} \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \le 0.0 \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \le 7.4213287430612339 \cdot 10^{304}\right)\right)\right):\\ \;\;\;\;\left(\frac{a1}{b1} \cdot \frac{\sqrt[3]{a2} \cdot \sqrt[3]{a2}}{\sqrt[3]{b2} \cdot \sqrt[3]{b2}}\right) \cdot \frac{\sqrt[3]{a2}}{\sqrt[3]{b2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{a1 \cdot a2}{b1 \cdot b2}\\ \end{array}\]

\frac{a1 \cdot a2}{b1 \cdot b2}

↓

\begin{array}{l}
\mathbf{if}\;\frac{a1 \cdot a2}{b1 \cdot b2} = -\infty \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \le -5.21092585859161966 \cdot 10^{-296} \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \le 0.0 \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \le 7.4213287430612339 \cdot 10^{304}\right)\right)\right):\\
\;\;\;\;\left(\frac{a1}{b1} \cdot \frac{\sqrt[3]{a2} \cdot \sqrt[3]{a2}}{\sqrt[3]{b2} \cdot \sqrt[3]{b2}}\right) \cdot \frac{\sqrt[3]{a2}}{\sqrt[3]{b2}}\\

\mathbf{else}:\\
\;\;\;\;\frac{a1 \cdot a2}{b1 \cdot b2}\\

\end{array}

double f(double a1, double a2, double b1, double b2) {
        double r183321 = a1;
        double r183322 = a2;
        double r183323 = r183321 * r183322;
        double r183324 = b1;
        double r183325 = b2;
        double r183326 = r183324 * r183325;
        double r183327 = r183323 / r183326;
        return r183327;
}

↓

double f(double a1, double a2, double b1, double b2) {
        double r183328 = a1;
        double r183329 = a2;
        double r183330 = r183328 * r183329;
        double r183331 = b1;
        double r183332 = b2;
        double r183333 = r183331 * r183332;
        double r183334 = r183330 / r183333;
        double r183335 = -inf.0;
        bool r183336 = r183334 <= r183335;
        double r183337 = -5.21092585859162e-296;
        bool r183338 = r183334 <= r183337;
        double r183339 = 0.0;
        bool r183340 = r183334 <= r183339;
        double r183341 = 7.421328743061234e+304;
        bool r183342 = r183334 <= r183341;
        double r183343 = !r183342;
        bool r183344 = r183340 || r183343;
        double r183345 = !r183344;
        bool r183346 = r183338 || r183345;
        double r183347 = !r183346;
        bool r183348 = r183336 || r183347;
        double r183349 = r183328 / r183331;
        double r183350 = cbrt(r183329);
        double r183351 = r183350 * r183350;
        double r183352 = cbrt(r183332);
        double r183353 = r183352 * r183352;
        double r183354 = r183351 / r183353;
        double r183355 = r183349 * r183354;
        double r183356 = r183350 / r183352;
        double r183357 = r183355 * r183356;
        double r183358 = r183348 ? r183357 : r183334;
        return r183358;
}

Original	11.2
Target	11.6
Herbie	1.6

Derivation

Split input into 2 regimes
if (/ (* a1 a2) (* b1 b2)) < -inf.0 or -5.21092585859162e-296 < (/ (* a1 a2) (* b1 b2)) < 0.0 or 7.421328743061234e+304 < (/ (* a1 a2) (* b1 b2))
1. Initial program 25.7
  \[\frac{a1 \cdot a2}{b1 \cdot b2}\]
2. Using strategy rm
3. Applied times-frac4.0
  \[\leadsto \color{blue}{\frac{a1}{b1} \cdot \frac{a2}{b2}}\]
4. Using strategy rm
5. Applied add-cube-cbrt4.4
  \[\leadsto \frac{a1}{b1} \cdot \frac{a2}{\color{blue}{\left(\sqrt[3]{b2} \cdot \sqrt[3]{b2}\right) \cdot \sqrt[3]{b2}}}\]
6. Applied add-cube-cbrt4.5
  \[\leadsto \frac{a1}{b1} \cdot \frac{\color{blue}{\left(\sqrt[3]{a2} \cdot \sqrt[3]{a2}\right) \cdot \sqrt[3]{a2}}}{\left(\sqrt[3]{b2} \cdot \sqrt[3]{b2}\right) \cdot \sqrt[3]{b2}}\]
7. Applied times-frac4.5
  \[\leadsto \frac{a1}{b1} \cdot \color{blue}{\left(\frac{\sqrt[3]{a2} \cdot \sqrt[3]{a2}}{\sqrt[3]{b2} \cdot \sqrt[3]{b2}} \cdot \frac{\sqrt[3]{a2}}{\sqrt[3]{b2}}\right)}\]
8. Applied associate-*r*2.7
  \[\leadsto \color{blue}{\left(\frac{a1}{b1} \cdot \frac{\sqrt[3]{a2} \cdot \sqrt[3]{a2}}{\sqrt[3]{b2} \cdot \sqrt[3]{b2}}\right) \cdot \frac{\sqrt[3]{a2}}{\sqrt[3]{b2}}}\]
if -inf.0 < (/ (* a1 a2) (* b1 b2)) < -5.21092585859162e-296 or 0.0 < (/ (* a1 a2) (* b1 b2)) < 7.421328743061234e+304
1. Initial program 0.8
  \[\frac{a1 \cdot a2}{b1 \cdot b2}\]
2. Using strategy rm
3. Applied times-frac17.1
  \[\leadsto \color{blue}{\frac{a1}{b1} \cdot \frac{a2}{b2}}\]
4. Using strategy rm
5. Applied *-un-lft-identity17.1
  \[\leadsto \frac{a1}{\color{blue}{1 \cdot b1}} \cdot \frac{a2}{b2}\]
6. Applied *-un-lft-identity17.1
  \[\leadsto \frac{\color{blue}{1 \cdot a1}}{1 \cdot b1} \cdot \frac{a2}{b2}\]
7. Applied times-frac17.1
  \[\leadsto \color{blue}{\left(\frac{1}{1} \cdot \frac{a1}{b1}\right)} \cdot \frac{a2}{b2}\]
8. Applied associate-*l*17.1
  \[\leadsto \color{blue}{\frac{1}{1} \cdot \left(\frac{a1}{b1} \cdot \frac{a2}{b2}\right)}\]
9. Simplified0.8
  \[\leadsto \frac{1}{1} \cdot \color{blue}{\frac{a1 \cdot a2}{b1 \cdot b2}}\]
Recombined 2 regimes into one program.
Final simplification1.6
\[\leadsto \begin{array}{l} \mathbf{if}\;\frac{a1 \cdot a2}{b1 \cdot b2} = -\infty \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \le -5.21092585859161966 \cdot 10^{-296} \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \le 0.0 \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \le 7.4213287430612339 \cdot 10^{304}\right)\right)\right):\\ \;\;\;\;\left(\frac{a1}{b1} \cdot \frac{\sqrt[3]{a2} \cdot \sqrt[3]{a2}}{\sqrt[3]{b2} \cdot \sqrt[3]{b2}}\right) \cdot \frac{\sqrt[3]{a2}}{\sqrt[3]{b2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{a1 \cdot a2}{b1 \cdot b2}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if (/ (* a1 a2) (* b1 b2)) < -inf.0 or -5.21092585859162e-296 < (/ (* a1 a2) (* b1 b2)) < 0.0 or 7.421328743061234e+304 < (/ (* a1 a2) (* b1 b2))`

`if -inf.0 < (/ (* a1 a2) (* b1 b2)) < -5.21092585859162e-296 or 0.0 < (/ (* a1 a2) (* b1 b2)) < 7.421328743061234e+304`

Reproduce

In
Out