Numeric.Histogram:binBounds from Chart-1.5.3

Average Error: 6.5 → 1.4

Time: 3.4s

Precision: 64

Math

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

↓

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

C

double f(double x, double y, double z, double t) {
        double r397137 = x;
        double r397138 = y;
        double r397139 = r397138 - r397137;
        double r397140 = z;
        double r397141 = r397139 * r397140;
        double r397142 = t;
        double r397143 = r397141 / r397142;
        double r397144 = r397137 + r397143;
        return r397144;
}

↓

double f(double x, double y, double z, double t) {
        double r397145 = x;
        double r397146 = y;
        double r397147 = r397146 - r397145;
        double r397148 = z;
        double r397149 = r397147 * r397148;
        double r397150 = t;
        double r397151 = r397149 / r397150;
        double r397152 = r397145 + r397151;
        double r397153 = -inf.0;
        bool r397154 = r397152 <= r397153;
        double r397155 = 4.782228900807809e-260;
        bool r397156 = r397152 <= r397155;
        double r397157 = !r397156;
        bool r397158 = r397154 || r397157;
        double r397159 = 1.0;
        double r397160 = r397150 / r397148;
        double r397161 = r397160 / r397147;
        double r397162 = r397159 / r397161;
        double r397163 = r397145 + r397162;
        double r397164 = r397158 ? r397163 : r397152;
        return r397164;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	6.5
Target	2.2
Herbie	1.4

\[\begin{array}{l} \mathbf{if}\;x \lt -9.025511195533004570453352523209034680317 \cdot 10^{-135}:\\ \;\;\;\;x - \frac{z}{t} \cdot \left(x - y\right)\\ \mathbf{elif}\;x \lt 4.275032163700714748507147332551979944314 \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 (/ (* (- y x) z) t)) < -inf.0 or 4.782228900807809e-260 < (+ x (/ (* (- y x) z) t))

   1. Initial program 11.4

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

   3. Applied associate-/l* 1.7

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

   5. Applied clear-num 1.8

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

   if -inf.0 < (+ x (/ (* (- y x) z) t)) < 4.782228900807809e-260

   1. Initial program 0.9

      \[x + \frac{\left(y - x\right) \cdot z}{t}\]
3. Recombined 2 regimes into one program.

4. Final simplification 1.4

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

Reproduce

herbie shell --seed 2019356 +o rules:numerics
(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)))