Numeric.Histogram:binBounds from Chart-1.5.3

Average Error: 6.6 → 1.9

Time: 3.0s

Precision: 64

Math

\[x + \frac{\left(y - x\right) \cdot z}{t}\]

↓

\[\begin{array}{l} \mathbf{if}\;x \le -1.15003287352819712 \cdot 10^{-238} \lor \neg \left(x \le 1.0116038839391772 \cdot 10^{-300}\right):\\ \;\;\;\;x + \left(y - x\right) \cdot \frac{z}{t}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{\frac{y - x}{t}}{\frac{1}{z}}\\ \end{array}\]

C

double f(double x, double y, double z, double t) {
        double r544467 = x;
        double r544468 = y;
        double r544469 = r544468 - r544467;
        double r544470 = z;
        double r544471 = r544469 * r544470;
        double r544472 = t;
        double r544473 = r544471 / r544472;
        double r544474 = r544467 + r544473;
        return r544474;
}

↓

double f(double x, double y, double z, double t) {
        double r544475 = x;
        double r544476 = -1.1500328735281971e-238;
        bool r544477 = r544475 <= r544476;
        double r544478 = 1.0116038839391772e-300;
        bool r544479 = r544475 <= r544478;
        double r544480 = !r544479;
        bool r544481 = r544477 || r544480;
        double r544482 = y;
        double r544483 = r544482 - r544475;
        double r544484 = z;
        double r544485 = t;
        double r544486 = r544484 / r544485;
        double r544487 = r544483 * r544486;
        double r544488 = r544475 + r544487;
        double r544489 = r544483 / r544485;
        double r544490 = 1.0;
        double r544491 = r544490 / r544484;
        double r544492 = r544489 / r544491;
        double r544493 = r544475 + r544492;
        double r544494 = r544481 ? r544488 : r544493;
        return r544494;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	6.6
Target	1.9
Herbie	1.9

\[\begin{array}{l} \mathbf{if}\;x \lt -9.0255111955330046 \cdot 10^{-135}:\\ \;\;\;\;x - \frac{z}{t} \cdot \left(x - y\right)\\ \mathbf{elif}\;x \lt 4.2750321637007147 \cdot 10^{-250}:\\ \;\;\;\;x + \frac{y - x}{t} \cdot z\\ \mathbf{else}:\\ \;\;\;\;x + \frac{y - x}{\frac{t}{z}}\\ \end{array}\]

Derivation

1. Split input into 2 regimes

2. if x < -1.1500328735281971e-238 or 1.0116038839391772e-300 < x

   1. Initial program 6.7

      \[x + \frac{\left(y - x\right) \cdot z}{t}\]
   2. Using strategy rm

   3. Applied *-un-lft-identity 6.7

      \[\leadsto x + \frac{\left(y - x\right) \cdot z}{\color{blue}{1 \cdot t}}\]

   4. Applied times-frac 1.7

      \[\leadsto x + \color{blue}{\frac{y - x}{1} \cdot \frac{z}{t}}\]

   5. Simplified 1.7

      \[\leadsto x + \color{blue}{\left(y - x\right)} \cdot \frac{z}{t}\]

   if -1.1500328735281971e-238 < x < 1.0116038839391772e-300

   1. Initial program 5.6

      \[x + \frac{\left(y - x\right) \cdot z}{t}\]
   2. Using strategy rm

   3. Applied associate-/l* 6.8

      \[\leadsto x + \color{blue}{\frac{y - x}{\frac{t}{z}}}\]
   4. Using strategy rm

   5. Applied div-inv 6.8

      \[\leadsto x + \frac{y - x}{\color{blue}{t \cdot \frac{1}{z}}}\]

   6. Applied associate-/r* 4.7

      \[\leadsto x + \color{blue}{\frac{\frac{y - x}{t}}{\frac{1}{z}}}\]
3. Recombined 2 regimes into one program.

4. Final simplification 1.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le -1.15003287352819712 \cdot 10^{-238} \lor \neg \left(x \le 1.0116038839391772 \cdot 10^{-300}\right):\\ \;\;\;\;x + \left(y - x\right) \cdot \frac{z}{t}\\ \mathbf{else}:\\ \;\;\;\;x + \frac{\frac{y - x}{t}}{\frac{1}{z}}\\ \end{array}\]

Reproduce

herbie shell --seed 2020056 
(FPCore (x y z t)
  :name "Numeric.Histogram:binBounds from Chart-1.5.3"
  :precision binary64

  :herbie-target
  (if (< x -9.025511195533005e-135) (- x (* (/ z t) (- x y))) (if (< x 4.275032163700715e-250) (+ x (* (/ (- y x) t) z)) (+ x (/ (- y x) (/ t z)))))

  (+ x (/ (* (- y x) z) t)))