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

↓

\[\begin{array}{l} \mathbf{if}\;\frac{a1 \cdot a2}{b1 \cdot b2} = -\infty:\\ \;\;\;\;\frac{\frac{1}{\frac{b1}{a1}}}{\frac{b2}{a2}}\\ \mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le -1.467391042233376 \cdot 10^{-284}:\\ \;\;\;\;\frac{a1 \cdot a2}{b1 \cdot b2}\\ \mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le -0.0:\\ \;\;\;\;a1 \cdot \frac{\frac{a2}{b1}}{b2}\\ \mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le 3.9728063804597205 \cdot 10^{+288}:\\ \;\;\;\;\frac{a1 \cdot a2}{b1 \cdot b2}\\ \mathbf{else}:\\ \;\;\;\;a1 \cdot \frac{\frac{a2}{b1}}{b2}\\ \end{array}\]

double f(double a1, double a2, double b1, double b2) {
        double r25364084 = a1;
        double r25364085 = a2;
        double r25364086 = r25364084 * r25364085;
        double r25364087 = b1;
        double r25364088 = b2;
        double r25364089 = r25364087 * r25364088;
        double r25364090 = r25364086 / r25364089;
        return r25364090;
}

↓

double f(double a1, double a2, double b1, double b2) {
        double r25364091 = a1;
        double r25364092 = a2;
        double r25364093 = r25364091 * r25364092;
        double r25364094 = b1;
        double r25364095 = b2;
        double r25364096 = r25364094 * r25364095;
        double r25364097 = r25364093 / r25364096;
        double r25364098 = -inf.0;
        bool r25364099 = r25364097 <= r25364098;
        double r25364100 = 1.0;
        double r25364101 = r25364094 / r25364091;
        double r25364102 = r25364100 / r25364101;
        double r25364103 = r25364095 / r25364092;
        double r25364104 = r25364102 / r25364103;
        double r25364105 = -1.467391042233376e-284;
        bool r25364106 = r25364097 <= r25364105;
        double r25364107 = -0.0;
        bool r25364108 = r25364097 <= r25364107;
        double r25364109 = r25364092 / r25364094;
        double r25364110 = r25364109 / r25364095;
        double r25364111 = r25364091 * r25364110;
        double r25364112 = 3.9728063804597205e+288;
        bool r25364113 = r25364097 <= r25364112;
        double r25364114 = r25364113 ? r25364097 : r25364111;
        double r25364115 = r25364108 ? r25364111 : r25364114;
        double r25364116 = r25364106 ? r25364097 : r25364115;
        double r25364117 = r25364099 ? r25364104 : r25364116;
        return r25364117;
}

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

↓

\begin{array}{l}
\mathbf{if}\;\frac{a1 \cdot a2}{b1 \cdot b2} = -\infty:\\
\;\;\;\;\frac{\frac{1}{\frac{b1}{a1}}}{\frac{b2}{a2}}\\

\mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le -1.467391042233376 \cdot 10^{-284}:\\
\;\;\;\;\frac{a1 \cdot a2}{b1 \cdot b2}\\

\mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le -0.0:\\
\;\;\;\;a1 \cdot \frac{\frac{a2}{b1}}{b2}\\

\mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le 3.9728063804597205 \cdot 10^{+288}:\\
\;\;\;\;\frac{a1 \cdot a2}{b1 \cdot b2}\\

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

\end{array}

Original	11.3
Target	10.7
Herbie	3.2

Derivation

Split input into 3 regimes
if (/ (* a1 a2) (* b1 b2)) < -inf.0
1. Initial program 60.0
  \[\frac{a1 \cdot a2}{b1 \cdot b2}\]
2. Using strategy rm
3. Applied clear-num60.0
  \[\leadsto \color{blue}{\frac{1}{\frac{b1 \cdot b2}{a1 \cdot a2}}}\]
4. Using strategy rm
5. Applied times-frac8.8
  \[\leadsto \frac{1}{\color{blue}{\frac{b1}{a1} \cdot \frac{b2}{a2}}}\]
6. Applied associate-/r*9.3
  \[\leadsto \color{blue}{\frac{\frac{1}{\frac{b1}{a1}}}{\frac{b2}{a2}}}\]
if -inf.0 < (/ (* a1 a2) (* b1 b2)) < -1.467391042233376e-284 or -0.0 < (/ (* a1 a2) (* b1 b2)) < 3.9728063804597205e+288
1. Initial program 0.8
  \[\frac{a1 \cdot a2}{b1 \cdot b2}\]
if -1.467391042233376e-284 < (/ (* a1 a2) (* b1 b2)) < -0.0 or 3.9728063804597205e+288 < (/ (* a1 a2) (* b1 b2))
1. Initial program 22.4
  \[\frac{a1 \cdot a2}{b1 \cdot b2}\]
2. Using strategy rm
3. Applied clear-num22.5
  \[\leadsto \color{blue}{\frac{1}{\frac{b1 \cdot b2}{a1 \cdot a2}}}\]
4. Using strategy rm
5. Applied associate-/r*15.4
  \[\leadsto \frac{1}{\color{blue}{\frac{\frac{b1 \cdot b2}{a1}}{a2}}}\]
6. Using strategy rm
7. Applied *-un-lft-identity15.4
  \[\leadsto \frac{1}{\color{blue}{1 \cdot \frac{\frac{b1 \cdot b2}{a1}}{a2}}}\]
8. Applied add-sqr-sqrt15.4
  \[\leadsto \frac{\color{blue}{\sqrt{1} \cdot \sqrt{1}}}{1 \cdot \frac{\frac{b1 \cdot b2}{a1}}{a2}}\]
9. Applied times-frac15.4
  \[\leadsto \color{blue}{\frac{\sqrt{1}}{1} \cdot \frac{\sqrt{1}}{\frac{\frac{b1 \cdot b2}{a1}}{a2}}}\]
10. Simplified15.4
  \[\leadsto \color{blue}{1} \cdot \frac{\sqrt{1}}{\frac{\frac{b1 \cdot b2}{a1}}{a2}}\]
11. Simplified6.1
  \[\leadsto 1 \cdot \color{blue}{\left(a1 \cdot \frac{\frac{a2}{b1}}{b2}\right)}\]
Recombined 3 regimes into one program.
Final simplification3.2
\[\leadsto \begin{array}{l} \mathbf{if}\;\frac{a1 \cdot a2}{b1 \cdot b2} = -\infty:\\ \;\;\;\;\frac{\frac{1}{\frac{b1}{a1}}}{\frac{b2}{a2}}\\ \mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le -1.467391042233376 \cdot 10^{-284}:\\ \;\;\;\;\frac{a1 \cdot a2}{b1 \cdot b2}\\ \mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le -0.0:\\ \;\;\;\;a1 \cdot \frac{\frac{a2}{b1}}{b2}\\ \mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le 3.9728063804597205 \cdot 10^{+288}:\\ \;\;\;\;\frac{a1 \cdot a2}{b1 \cdot b2}\\ \mathbf{else}:\\ \;\;\;\;a1 \cdot \frac{\frac{a2}{b1}}{b2}\\ \end{array}\]

Error

Target

Derivation

`if (/ (* a1 a2) (* b1 b2)) < -inf.0`

`if -inf.0 < (/ (* a1 a2) (* b1 b2)) < -1.467391042233376e-284 or -0.0 < (/ (* a1 a2) (* b1 b2)) < 3.9728063804597205e+288`

`if -1.467391042233376e-284 < (/ (* a1 a2) (* b1 b2)) < -0.0 or 3.9728063804597205e+288 < (/ (* a1 a2) (* b1 b2))`

Reproduce