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

↓

\[\begin{array}{l} \mathbf{if}\;a1 \cdot a2 \le -5.357495374115058859574803759498417143626 \cdot 10^{281} \lor \neg \left(a1 \cdot a2 \le -1.889894252236271565593841678846670543341 \cdot 10^{-219} \lor \neg \left(a1 \cdot a2 \le 6.190439332305387269953729326062688466342 \cdot 10^{-251} \lor \neg \left(a1 \cdot a2 \le 5.085740809466005128807940672201688268012 \cdot 10^{138}\right)\right)\right):\\ \;\;\;\;\frac{a1}{b2} \cdot \frac{a2}{b1}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{a1 \cdot a2}{\sqrt[3]{b2} \cdot \sqrt[3]{b2}}}{\sqrt[3]{b2} \cdot b1}\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;a1 \cdot a2 \le -5.357495374115058859574803759498417143626 \cdot 10^{281} \lor \neg \left(a1 \cdot a2 \le -1.889894252236271565593841678846670543341 \cdot 10^{-219} \lor \neg \left(a1 \cdot a2 \le 6.190439332305387269953729326062688466342 \cdot 10^{-251} \lor \neg \left(a1 \cdot a2 \le 5.085740809466005128807940672201688268012 \cdot 10^{138}\right)\right)\right):\\
\;\;\;\;\frac{a1}{b2} \cdot \frac{a2}{b1}\\

\mathbf{else}:\\
\;\;\;\;\frac{\frac{a1 \cdot a2}{\sqrt[3]{b2} \cdot \sqrt[3]{b2}}}{\sqrt[3]{b2} \cdot b1}\\

\end{array}

double f(double a1, double a2, double b1, double b2) {
        double r102473 = a1;
        double r102474 = a2;
        double r102475 = r102473 * r102474;
        double r102476 = b1;
        double r102477 = b2;
        double r102478 = r102476 * r102477;
        double r102479 = r102475 / r102478;
        return r102479;
}

↓

double f(double a1, double a2, double b1, double b2) {
        double r102480 = a1;
        double r102481 = a2;
        double r102482 = r102480 * r102481;
        double r102483 = -5.357495374115059e+281;
        bool r102484 = r102482 <= r102483;
        double r102485 = -1.8898942522362716e-219;
        bool r102486 = r102482 <= r102485;
        double r102487 = 6.190439332305387e-251;
        bool r102488 = r102482 <= r102487;
        double r102489 = 5.085740809466005e+138;
        bool r102490 = r102482 <= r102489;
        double r102491 = !r102490;
        bool r102492 = r102488 || r102491;
        double r102493 = !r102492;
        bool r102494 = r102486 || r102493;
        double r102495 = !r102494;
        bool r102496 = r102484 || r102495;
        double r102497 = b2;
        double r102498 = r102480 / r102497;
        double r102499 = b1;
        double r102500 = r102481 / r102499;
        double r102501 = r102498 * r102500;
        double r102502 = cbrt(r102497);
        double r102503 = r102502 * r102502;
        double r102504 = r102482 / r102503;
        double r102505 = r102502 * r102499;
        double r102506 = r102504 / r102505;
        double r102507 = r102496 ? r102501 : r102506;
        return r102507;
}

Original	11.3
Target	10.7
Herbie	4.5

Derivation

Split input into 4 regimes
if (* a1 a2) < -5.357495374115059e+281
1. Initial program 52.3
  \[\frac{a1 \cdot a2}{b1 \cdot b2}\]
2. Using strategy rm
3. Applied times-frac8.2
  \[\leadsto \color{blue}{\frac{a1}{b1} \cdot \frac{a2}{b2}}\]
if -5.357495374115059e+281 < (* a1 a2) < -1.8898942522362716e-219 or 6.190439332305387e-251 < (* a1 a2) < 5.085740809466005e+138
1. Initial program 5.0
  \[\frac{a1 \cdot a2}{b1 \cdot b2}\]
2. Using strategy rm
3. Applied associate-/r*4.5
  \[\leadsto \color{blue}{\frac{\frac{a1 \cdot a2}{b1}}{b2}}\]
4. Using strategy rm
5. Applied add-cube-cbrt5.3
  \[\leadsto \frac{\frac{a1 \cdot a2}{b1}}{\color{blue}{\left(\sqrt[3]{b2} \cdot \sqrt[3]{b2}\right) \cdot \sqrt[3]{b2}}}\]
6. Applied div-inv5.3
  \[\leadsto \frac{\color{blue}{\left(a1 \cdot a2\right) \cdot \frac{1}{b1}}}{\left(\sqrt[3]{b2} \cdot \sqrt[3]{b2}\right) \cdot \sqrt[3]{b2}}\]
7. Applied times-frac3.4
  \[\leadsto \color{blue}{\frac{a1 \cdot a2}{\sqrt[3]{b2} \cdot \sqrt[3]{b2}} \cdot \frac{\frac{1}{b1}}{\sqrt[3]{b2}}}\]
if -1.8898942522362716e-219 < (* a1 a2) < 6.190439332305387e-251
1. Initial program 15.7
  \[\frac{a1 \cdot a2}{b1 \cdot b2}\]
2. Using strategy rm
3. Applied associate-/r*15.2
  \[\leadsto \color{blue}{\frac{\frac{a1 \cdot a2}{b1}}{b2}}\]
4. Using strategy rm
5. Applied *-un-lft-identity15.2
  \[\leadsto \frac{\frac{a1 \cdot a2}{\color{blue}{1 \cdot b1}}}{b2}\]
6. Applied times-frac6.9
  \[\leadsto \frac{\color{blue}{\frac{a1}{1} \cdot \frac{a2}{b1}}}{b2}\]
7. Applied associate-/l*3.6
  \[\leadsto \color{blue}{\frac{\frac{a1}{1}}{\frac{b2}{\frac{a2}{b1}}}}\]
8. Using strategy rm
9. Applied associate-/r/3.6
  \[\leadsto \color{blue}{\frac{\frac{a1}{1}}{b2} \cdot \frac{a2}{b1}}\]
10. Simplified3.6
  \[\leadsto \color{blue}{\frac{a1}{b2}} \cdot \frac{a2}{b1}\]
if 5.085740809466005e+138 < (* a1 a2)
1. Initial program 28.6
  \[\frac{a1 \cdot a2}{b1 \cdot b2}\]
2. Using strategy rm
3. Applied associate-/r*27.4
  \[\leadsto \color{blue}{\frac{\frac{a1 \cdot a2}{b1}}{b2}}\]
4. Using strategy rm
5. Applied *-un-lft-identity27.4
  \[\leadsto \frac{\frac{a1 \cdot a2}{\color{blue}{1 \cdot b1}}}{b2}\]
6. Applied times-frac16.3
  \[\leadsto \frac{\color{blue}{\frac{a1}{1} \cdot \frac{a2}{b1}}}{b2}\]
7. Applied associate-/l*12.8
  \[\leadsto \color{blue}{\frac{\frac{a1}{1}}{\frac{b2}{\frac{a2}{b1}}}}\]
Recombined 4 regimes into one program.
Final simplification4.5
\[\leadsto \begin{array}{l} \mathbf{if}\;a1 \cdot a2 \le -5.357495374115058859574803759498417143626 \cdot 10^{281} \lor \neg \left(a1 \cdot a2 \le -1.889894252236271565593841678846670543341 \cdot 10^{-219} \lor \neg \left(a1 \cdot a2 \le 6.190439332305387269953729326062688466342 \cdot 10^{-251} \lor \neg \left(a1 \cdot a2 \le 5.085740809466005128807940672201688268012 \cdot 10^{138}\right)\right)\right):\\ \;\;\;\;\frac{a1}{b2} \cdot \frac{a2}{b1}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{a1 \cdot a2}{\sqrt[3]{b2} \cdot \sqrt[3]{b2}}}{\sqrt[3]{b2} \cdot b1}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if (* a1 a2) < -5.357495374115059e+281`

`if -5.357495374115059e+281 < (* a1 a2) < -1.8898942522362716e-219 or 6.190439332305387e-251 < (* a1 a2) < 5.085740809466005e+138`

`if -1.8898942522362716e-219 < (* a1 a2) < 6.190439332305387e-251`

`if 5.085740809466005e+138 < (* a1 a2)`

Reproduce

In
Out