Quotient of products

Average Error: 11.1 → 2.9

Time: 1.9s

Precision: 64

Math

\[\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 -6.28254 \cdot 10^{-319} \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \le 1.16422584143949291 \cdot 10^{-290} \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \le 6.1160527718578736 \cdot 10^{209}\right)\right)\right):\\ \;\;\;\;\frac{a1}{b1} \cdot \frac{a2}{b2}\\ \mathbf{else}:\\ \;\;\;\;\frac{a1 \cdot a2}{b1 \cdot b2}\\ \end{array}\]

C

double f(double a1, double a2, double b1, double b2) {
        double r159276 = a1;
        double r159277 = a2;
        double r159278 = r159276 * r159277;
        double r159279 = b1;
        double r159280 = b2;
        double r159281 = r159279 * r159280;
        double r159282 = r159278 / r159281;
        return r159282;
}

↓

double f(double a1, double a2, double b1, double b2) {
        double r159283 = a1;
        double r159284 = a2;
        double r159285 = r159283 * r159284;
        double r159286 = b1;
        double r159287 = b2;
        double r159288 = r159286 * r159287;
        double r159289 = r159285 / r159288;
        double r159290 = -inf.0;
        bool r159291 = r159289 <= r159290;
        double r159292 = -6.2825387525173e-319;
        bool r159293 = r159289 <= r159292;
        double r159294 = 1.1642258414394929e-290;
        bool r159295 = r159289 <= r159294;
        double r159296 = 6.1160527718578736e+209;
        bool r159297 = r159289 <= r159296;
        double r159298 = !r159297;
        bool r159299 = r159295 || r159298;
        double r159300 = !r159299;
        bool r159301 = r159293 || r159300;
        double r159302 = !r159301;
        bool r159303 = r159291 || r159302;
        double r159304 = r159283 / r159286;
        double r159305 = r159284 / r159287;
        double r159306 = r159304 * r159305;
        double r159307 = r159303 ? r159306 : r159289;
        return r159307;
}

Error

Bits error versus a1

Bits error versus a2

Bits error versus b1

Bits error versus b2

Target

Original	11.1
Target	11.6
Herbie	2.9

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

Derivation

1. Split input into 2 regimes

2. if (/ (* a1 a2) (* b1 b2)) < -inf.0 or -6.2825387525173e-319 < (/ (* a1 a2) (* b1 b2)) < 1.1642258414394929e-290 or 6.1160527718578736e+209 < (/ (* a1 a2) (* b1 b2))

   1. Initial program 23.1

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

   3. Applied times-frac 5.4

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

   if -inf.0 < (/ (* a1 a2) (* b1 b2)) < -6.2825387525173e-319 or 1.1642258414394929e-290 < (/ (* a1 a2) (* b1 b2)) < 6.1160527718578736e+209

   1. Initial program 0.8

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

   3. Applied associate-/l* 8.0

      \[\leadsto \color{blue}{\frac{a1}{\frac{b1 \cdot b2}{a2}}}\]
   4. Using strategy rm

   5. Applied associate-/r/ 8.1

      \[\leadsto \color{blue}{\frac{a1}{b1 \cdot b2} \cdot a2}\]
   6. Using strategy rm

   7. Applied associate-*l/ 0.8

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

4. Final simplification 2.9

   \[\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 -6.28254 \cdot 10^{-319} \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \le 1.16422584143949291 \cdot 10^{-290} \lor \neg \left(\frac{a1 \cdot a2}{b1 \cdot b2} \le 6.1160527718578736 \cdot 10^{209}\right)\right)\right):\\ \;\;\;\;\frac{a1}{b1} \cdot \frac{a2}{b2}\\ \mathbf{else}:\\ \;\;\;\;\frac{a1 \cdot a2}{b1 \cdot b2}\\ \end{array}\]

Reproduce

herbie shell --seed 2020046 +o rules:numerics
(FPCore (a1 a2 b1 b2)
  :name "Quotient of products"
  :precision binary64

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

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