Average Error: 11.4 → 3.0
Time: 2.4s
Precision: 64
\[\frac{a1 \cdot a2}{b1 \cdot b2}\]
↓
\[\begin{array}{l} \mathbf{if}\;\frac{a1 \cdot a2}{b1 \cdot b2} = -\infty:\\ \;\;\;\;\frac{a1}{\frac{b1 \cdot b2}{a2}}\\ \mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le -1.4671499395447483 \cdot 10^{-308}:\\ \;\;\;\;\left(a1 \cdot a2\right) \cdot \frac{\frac{1}{b1}}{b2}\\ \mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le 0.0:\\ \;\;\;\;\frac{a1}{b1} \cdot \frac{a2}{b2}\\ \mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le 1.3804268269775264 \cdot 10^{294}:\\ \;\;\;\;\left(a1 \cdot a2\right) \cdot \frac{\frac{1}{b1}}{b2}\\ \mathbf{else}:\\ \;\;\;\;\frac{a1}{b1} \cdot \frac{a2}{b2}\\ \end{array}\]
\frac{a1 \cdot a2}{b1 \cdot b2}
↓
\begin{array}{l}
\mathbf{if}\;\frac{a1 \cdot a2}{b1 \cdot b2} = -\infty:\\
\;\;\;\;\frac{a1}{\frac{b1 \cdot b2}{a2}}\\

\mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le -1.4671499395447483 \cdot 10^{-308}:\\
\;\;\;\;\left(a1 \cdot a2\right) \cdot \frac{\frac{1}{b1}}{b2}\\

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

\mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le 1.3804268269775264 \cdot 10^{294}:\\
\;\;\;\;\left(a1 \cdot a2\right) \cdot \frac{\frac{1}{b1}}{b2}\\

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

\end{array}
double f(double a1, double a2, double b1, double b2) {
        double r172440 = a1;
        double r172441 = a2;
        double r172442 = r172440 * r172441;
        double r172443 = b1;
        double r172444 = b2;
        double r172445 = r172443 * r172444;
        double r172446 = r172442 / r172445;
        return r172446;
}
↓
double f(double a1, double a2, double b1, double b2) {
        double r172447 = a1;
        double r172448 = a2;
        double r172449 = r172447 * r172448;
        double r172450 = b1;
        double r172451 = b2;
        double r172452 = r172450 * r172451;
        double r172453 = r172449 / r172452;
        double r172454 = -inf.0;
        bool r172455 = r172453 <= r172454;
        double r172456 = r172452 / r172448;
        double r172457 = r172447 / r172456;
        double r172458 = -1.4671499395447483e-308;
        bool r172459 = r172453 <= r172458;
        double r172460 = 1.0;
        double r172461 = r172460 / r172450;
        double r172462 = r172461 / r172451;
        double r172463 = r172449 * r172462;
        double r172464 = 0.0;
        bool r172465 = r172453 <= r172464;
        double r172466 = r172447 / r172450;
        double r172467 = r172448 / r172451;
        double r172468 = r172466 * r172467;
        double r172469 = 1.3804268269775264e+294;
        bool r172470 = r172453 <= r172469;
        double r172471 = r172470 ? r172463 : r172468;
        double r172472 = r172465 ? r172468 : r172471;
        double r172473 = r172459 ? r172463 : r172472;
        double r172474 = r172455 ? r172457 : r172473;
        return r172474;
}

Error

Bits error versus a1

Bits error versus a2

Bits error versus b1

Bits error versus b2

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original11.4
Target11.0
Herbie3.0
\[\frac{a1}{b1} \cdot \frac{a2}{b2}\]

Derivation

  1. Split input into 3 regimes

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

    1. Initial program 64.0

      \[\frac{a1 \cdot a2}{b1 \cdot b2}\]
    2. Using strategy rm

    3. Applied associate-/l*30.9

      \[\leadsto \color{blue}{\frac{a1}{\frac{b1 \cdot b2}{a2}}}\]

    if -inf.0 < (/ (* a1 a2) (* b1 b2)) < -1.4671499395447483e-308 or 0.0 < (/ (* a1 a2) (* b1 b2)) < 1.3804268269775264e+294

    1. Initial program 0.9

      \[\frac{a1 \cdot a2}{b1 \cdot b2}\]
    2. Using strategy rm

    3. Applied div-inv1.3

      \[\leadsto \color{blue}{\left(a1 \cdot a2\right) \cdot \frac{1}{b1 \cdot b2}}\]
    4. Using strategy rm

    5. Applied associate-/r*1.3

      \[\leadsto \left(a1 \cdot a2\right) \cdot \color{blue}{\frac{\frac{1}{b1}}{b2}}\]

    if -1.4671499395447483e-308 < (/ (* a1 a2) (* b1 b2)) < 0.0 or 1.3804268269775264e+294 < (/ (* a1 a2) (* b1 b2))

    1. Initial program 22.3

      \[\frac{a1 \cdot a2}{b1 \cdot b2}\]
    2. Using strategy rm

    3. Applied times-frac3.1

      \[\leadsto \color{blue}{\frac{a1}{b1} \cdot \frac{a2}{b2}}\]
  3. Recombined 3 regimes into one program.

  4. Final simplification3.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{a1 \cdot a2}{b1 \cdot b2} = -\infty:\\ \;\;\;\;\frac{a1}{\frac{b1 \cdot b2}{a2}}\\ \mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le -1.4671499395447483 \cdot 10^{-308}:\\ \;\;\;\;\left(a1 \cdot a2\right) \cdot \frac{\frac{1}{b1}}{b2}\\ \mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le 0.0:\\ \;\;\;\;\frac{a1}{b1} \cdot \frac{a2}{b2}\\ \mathbf{elif}\;\frac{a1 \cdot a2}{b1 \cdot b2} \le 1.3804268269775264 \cdot 10^{294}:\\ \;\;\;\;\left(a1 \cdot a2\right) \cdot \frac{\frac{1}{b1}}{b2}\\ \mathbf{else}:\\ \;\;\;\;\frac{a1}{b1} \cdot \frac{a2}{b2}\\ \end{array}\]

Reproduce

herbie shell --seed 2020057 
(FPCore (a1 a2 b1 b2)
  :name "Quotient of products"
  :precision binary64

  :herbie-target
  (* (/ a1 b1) (/ a2 b2))

  (/ (* a1 a2) (* b1 b2)))