\frac{a1 \cdot a2}{b1 \cdot b2}\begin{array}{l}
\mathbf{if}\;\frac{a1 \cdot a2}{b1 \cdot b2} \leq -\infty \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \leq -1.1225291206462181 \cdot 10^{-307} \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \leq 0\right) \land \frac{a1 \cdot a2}{b1 \cdot b2} \leq 9.463909057472086 \cdot 10^{+305}\right):\\
\;\;\;\;\frac{a1}{b1} \cdot \frac{a2}{b2}\\
\mathbf{else}:\\
\;\;\;\;\frac{a1 \cdot a2}{b1 \cdot b2}\\
\end{array}(FPCore (a1 a2 b1 b2) :precision binary64 (/ (* a1 a2) (* b1 b2)))
(FPCore (a1 a2 b1 b2)
:precision binary64
(if (or (<= (/ (* a1 a2) (* b1 b2)) (- INFINITY))
(not
(or (<= (/ (* a1 a2) (* b1 b2)) -1.1225291206462181e-307)
(and (not (<= (/ (* a1 a2) (* b1 b2)) 0.0))
(<= (/ (* a1 a2) (* b1 b2)) 9.463909057472086e+305)))))
(* (/ a1 b1) (/ a2 b2))
(/ (* a1 a2) (* b1 b2))))double code(double a1, double a2, double b1, double b2) {
return (a1 * a2) / (b1 * b2);
}
double code(double a1, double a2, double b1, double b2) {
double tmp;
if ((((a1 * a2) / (b1 * b2)) <= -((double) INFINITY)) || !((((a1 * a2) / (b1 * b2)) <= -1.1225291206462181e-307) || (!(((a1 * a2) / (b1 * b2)) <= 0.0) && (((a1 * a2) / (b1 * b2)) <= 9.463909057472086e+305)))) {
tmp = (a1 / b1) * (a2 / b2);
} else {
tmp = (a1 * a2) / (b1 * b2);
}
return tmp;
}




Bits error versus a1




Bits error versus a2




Bits error versus b1




Bits error versus b2
Results
| Original | 11.6 |
|---|---|
| Target | 11.3 |
| Herbie | 2.0 |
if (/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) < -inf.0 or -1.1225291206462181e-307 < (/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) < 0.0 or 9.4639090574720859e305 < (/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) Initial program 26.3
rmApplied times-frac_binary643.7
if -inf.0 < (/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) < -1.1225291206462181e-307 or 0.0 < (/.f64 (*.f64 a1 a2) (*.f64 b1 b2)) < 9.4639090574720859e305Initial program 0.8
Final simplification2.0
herbie shell --seed 2020274
(FPCore (a1 a2 b1 b2)
:name "Quotient of products"
:precision binary64
:herbie-target
(* (/ a1 b1) (/ a2 b2))
(/ (* a1 a2) (* b1 b2)))