Development.Shake.Progress:decay from shake-0.15.5

Average Error: 23.4 → 18.2

Time: 10.0s

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 r879100 = x;
        double r879101 = y;
        double r879102 = r879100 * r879101;
        double r879103 = z;
        double r879104 = t;
        double r879105 = a;
        double r879106 = r879104 - r879105;
        double r879107 = r879103 * r879106;
        double r879108 = r879102 + r879107;
        double r879109 = b;
        double r879110 = r879109 - r879101;
        double r879111 = r879103 * r879110;
        double r879112 = r879101 + r879111;
        double r879113 = r879108 / r879112;
        return r879113;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r879114 = z;
        double r879115 = -2.081581403037953e+85;
        bool r879116 = r879114 <= r879115;
        double r879117 = 1.8025388190473185e+72;
        bool r879118 = r879114 <= r879117;
        double r879119 = !r879118;
        bool r879120 = r879116 || r879119;
        double r879121 = a;
        double r879122 = y;
        double r879123 = r879121 / r879122;
        double r879124 = t;
        double r879125 = r879124 / r879122;
        double r879126 = x;
        double r879127 = r879126 / r879114;
        double r879128 = r879125 + r879127;
        double r879129 = r879123 - r879128;
        double r879130 = r879126 * r879122;
        double r879131 = r879124 - r879121;
        double r879132 = r879114 * r879131;
        double r879133 = r879130 + r879132;
        double r879134 = 1.0;
        double r879135 = b;
        double r879136 = r879135 - r879122;
        double r879137 = r879114 * r879136;
        double r879138 = r879122 + r879137;
        double r879139 = r879134 / r879138;
        double r879140 = r879133 * r879139;
        double r879141 = r879120 ? r879129 : r879140;
        return r879141;
}

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)))))