Development.Shake.Progress:decay from shake-0.15.5

Average Error: 23.4 → 18.2

Time: 9.5s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;z \le -2.081581403037953128436994676205872025341 \cdot 10^{85} \lor \neg \left(z \le 1.802538819047318531632562944860211808714 \cdot 10^{72}\right):\\ \;\;\;\;\frac{a}{y} - \left(\frac{t}{y} + \frac{x}{z}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot y + z \cdot \left(t - a\right)\right) \cdot \frac{1}{y + z \cdot \left(b - y\right)}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r947212 = x;
        double r947213 = y;
        double r947214 = r947212 * r947213;
        double r947215 = z;
        double r947216 = t;
        double r947217 = a;
        double r947218 = r947216 - r947217;
        double r947219 = r947215 * r947218;
        double r947220 = r947214 + r947219;
        double r947221 = b;
        double r947222 = r947221 - r947213;
        double r947223 = r947215 * r947222;
        double r947224 = r947213 + r947223;
        double r947225 = r947220 / r947224;
        return r947225;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r947226 = z;
        double r947227 = -2.081581403037953e+85;
        bool r947228 = r947226 <= r947227;
        double r947229 = 1.8025388190473185e+72;
        bool r947230 = r947226 <= r947229;
        double r947231 = !r947230;
        bool r947232 = r947228 || r947231;
        double r947233 = a;
        double r947234 = y;
        double r947235 = r947233 / r947234;
        double r947236 = t;
        double r947237 = r947236 / r947234;
        double r947238 = x;
        double r947239 = r947238 / r947226;
        double r947240 = r947237 + r947239;
        double r947241 = r947235 - r947240;
        double r947242 = r947238 * r947234;
        double r947243 = r947236 - r947233;
        double r947244 = r947226 * r947243;
        double r947245 = r947242 + r947244;
        double r947246 = 1.0;
        double r947247 = b;
        double r947248 = r947247 - r947234;
        double r947249 = r947226 * r947248;
        double r947250 = r947234 + r947249;
        double r947251 = r947246 / r947250;
        double r947252 = r947245 * r947251;
        double r947253 = r947232 ? r947241 : r947252;
        return r947253;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Bits error versus b

Target

Original	23.4
Target	18.4
Herbie	18.2

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

Derivation

1. Split input into 2 regimes

2. if z < -2.081581403037953e+85 or 1.8025388190473185e+72 < z

   1. Initial program 45.1

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

   3. Applied add-cube-cbrt 45.3

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

   4. Applied add-cube-cbrt 45.4

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

   5. Applied prod-diff 45.4

      \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \color{blue}{\left(\mathsf{fma}\left(\sqrt[3]{b} \cdot \sqrt[3]{b}, \sqrt[3]{b}, -\sqrt[3]{y} \cdot \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right)\right) + \mathsf{fma}\left(-\sqrt[3]{y}, \sqrt[3]{y} \cdot \sqrt[3]{y}, \sqrt[3]{y} \cdot \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right)\right)\right)}}\]

   6. Applied distribute-lft-in 45.9

      \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{y + \color{blue}{\left(z \cdot \mathsf{fma}\left(\sqrt[3]{b} \cdot \sqrt[3]{b}, \sqrt[3]{b}, -\sqrt[3]{y} \cdot \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right)\right) + z \cdot \mathsf{fma}\left(-\sqrt[3]{y}, \sqrt[3]{y} \cdot \sqrt[3]{y}, \sqrt[3]{y} \cdot \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right)\right)\right)}}\]

   7. Simplified 45.8

      \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{y + \left(\color{blue}{z \cdot \mathsf{fma}\left(\sqrt[3]{b} \cdot \sqrt[3]{b}, \sqrt[3]{b}, -y \cdot 1\right)} + z \cdot \mathsf{fma}\left(-\sqrt[3]{y}, \sqrt[3]{y} \cdot \sqrt[3]{y}, \sqrt[3]{y} \cdot \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right)\right)\right)}\]

   8. Simplified 45.3

      \[\leadsto \frac{x \cdot y + z \cdot \left(t - a\right)}{y + \left(z \cdot \mathsf{fma}\left(\sqrt[3]{b} \cdot \sqrt[3]{b}, \sqrt[3]{b}, -y \cdot 1\right) + \color{blue}{z \cdot \mathsf{fma}\left(-y, 1, y\right)}\right)}\]

   9. Taylor expanded around inf 30.9

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

   if -2.081581403037953e+85 < z < 1.8025388190473185e+72

   1. Initial program 10.7

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

   3. Applied div-inv 10.8

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

4. Final simplification 18.2

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -2.081581403037953128436994676205872025341 \cdot 10^{85} \lor \neg \left(z \le 1.802538819047318531632562944860211808714 \cdot 10^{72}\right):\\ \;\;\;\;\frac{a}{y} - \left(\frac{t}{y} + \frac{x}{z}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot y + z \cdot \left(t - a\right)\right) \cdot \frac{1}{y + z \cdot \left(b - y\right)}\\ \end{array}\]

Reproduce

herbie shell --seed 2019353 +o rules:numerics
(FPCore (x y z t a b)
  :name "Development.Shake.Progress:decay from shake-0.15.5"
  :precision binary64

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

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