Diagrams.Trail:splitAtParam from diagrams-lib-1.3.0.3, A

Average Error: 7.2 → 3.5

Time: 19.2s

Precision: 64

Math

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

↓

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

C

double f(double x, double y, double z, double t) {
        double r530228 = x;
        double r530229 = y;
        double r530230 = z;
        double r530231 = r530229 * r530230;
        double r530232 = r530231 - r530228;
        double r530233 = t;
        double r530234 = r530233 * r530230;
        double r530235 = r530234 - r530228;
        double r530236 = r530232 / r530235;
        double r530237 = r530228 + r530236;
        double r530238 = 1.0;
        double r530239 = r530228 + r530238;
        double r530240 = r530237 / r530239;
        return r530240;
}

↓

double f(double x, double y, double z, double t) {
        double r530241 = z;
        double r530242 = -2.917974323621221e+123;
        bool r530243 = r530241 <= r530242;
        double r530244 = 1.6593690766520809e+131;
        bool r530245 = r530241 <= r530244;
        double r530246 = !r530245;
        bool r530247 = r530243 || r530246;
        double r530248 = x;
        double r530249 = y;
        double r530250 = t;
        double r530251 = r530249 / r530250;
        double r530252 = r530248 + r530251;
        double r530253 = 1.0;
        double r530254 = r530248 + r530253;
        double r530255 = r530252 / r530254;
        double r530256 = r530249 * r530241;
        double r530257 = r530256 - r530248;
        double r530258 = 1.0;
        double r530259 = r530250 * r530241;
        double r530260 = r530259 - r530248;
        double r530261 = r530258 / r530260;
        double r530262 = r530257 * r530261;
        double r530263 = r530248 + r530262;
        double r530264 = r530263 / r530254;
        double r530265 = r530247 ? r530255 : r530264;
        return r530265;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Target

Original	7.2
Target	0.3
Herbie	3.5

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

Derivation

1. Split input into 2 regimes

2. if z < -2.917974323621221e+123 or 1.6593690766520809e+131 < z

   1. Initial program 21.2

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

   2. Taylor expanded around inf 7.8

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

   if -2.917974323621221e+123 < z < 1.6593690766520809e+131

   1. Initial program 1.7

      \[\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}\]
   2. Using strategy rm

   3. Applied div-inv 1.8

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

4. Final simplification 3.5

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

Reproduce

herbie shell --seed 2019208 +o rules:numerics
(FPCore (x y z t)
  :name "Diagrams.Trail:splitAtParam  from diagrams-lib-1.3.0.3, A"
  :precision binary64

  :herbie-target
  (/ (+ x (- (/ y (- t (/ x z))) (/ x (- (* t z) x)))) (+ x 1))

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