Development.Shake.Progress:decay from shake-0.15.5

Average Error: 23.3 → 1.4

Time: 29.8s

Precision: binary64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq -1.0776202918311757 \cdot 10^{+307}:\\ \;\;\;\;\frac{-1}{\frac{y - b}{t - a}} - \frac{x}{z + -1}\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq -3.0865535911923863 \cdot 10^{-232}:\\ \;\;\;\;\frac{1}{\frac{y + z \cdot \left(b - y\right)}{x \cdot y + z \cdot \left(t - a\right)}}\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq 0:\\ \;\;\;\;\frac{t}{b - y} + \left(\left(\frac{\frac{x \cdot y}{z}}{b - y} + \frac{a}{z} \cdot \frac{y}{{\left(b - y\right)}^{2}}\right) - \left(\frac{y}{{\left(b - y\right)}^{2}} \cdot \frac{t}{z} + \frac{a}{b - y}\right)\right)\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq 1.3387691926349812 \cdot 10^{+279}:\\ \;\;\;\;\frac{\left(x \cdot y + z \cdot t\right) - z \cdot a}{y + z \cdot \left(b - y\right)}\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq \infty:\\ \;\;\;\;\frac{y}{\frac{y + z \cdot \left(b - y\right)}{x}} + \frac{z}{\frac{y + z \cdot \left(b - y\right)}{t - a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{t}{b - y} + \left(\left(\frac{a}{z} \cdot \frac{y}{{\left(b - y\right)}^{2}} + \frac{y}{z} \cdot \frac{x}{b - y}\right) - \left(\frac{a}{b - y} + \frac{y}{z} \cdot \frac{t}{{\left(b - y\right)}^{2}}\right)\right)\\ \end{array}\]

FPCore

(FPCore (x y z t a b)
 :precision binary64
 (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))))

↓

(FPCore (x y z t a b)
 :precision binary64
 (if (<=
      (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y))))
      -1.0776202918311757e+307)
   (- (/ -1.0 (/ (- y b) (- t a))) (/ x (+ z -1.0)))
   (if (<=
        (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y))))
        -3.0865535911923863e-232)
     (/ 1.0 (/ (+ y (* z (- b y))) (+ (* x y) (* z (- t a)))))
     (if (<= (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) 0.0)
       (+
        (/ t (- b y))
        (-
         (+ (/ (/ (* x y) z) (- b y)) (* (/ a z) (/ y (pow (- b y) 2.0))))
         (+ (* (/ y (pow (- b y) 2.0)) (/ t z)) (/ a (- b y)))))
       (if (<=
            (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y))))
            1.3387691926349812e+279)
         (/ (- (+ (* x y) (* z t)) (* z a)) (+ y (* z (- b y))))
         (if (<= (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) INFINITY)
           (+
            (/ y (/ (+ y (* z (- b y))) x))
            (/ z (/ (+ y (* z (- b y))) (- t a))))
           (+
            (/ t (- b y))
            (-
             (+ (* (/ a z) (/ y (pow (- b y) 2.0))) (* (/ y z) (/ x (- b y))))
             (+ (/ a (- b y)) (* (/ y z) (/ t (pow (- b y) 2.0))))))))))))

C

double code(double x, double y, double z, double t, double a, double b) {
	return ((x * y) + (z * (t - a))) / (y + (z * (b - y)));
}

↓

double code(double x, double y, double z, double t, double a, double b) {
	double tmp;
	if ((((x * y) + (z * (t - a))) / (y + (z * (b - y)))) <= -1.0776202918311757e+307) {
		tmp = (-1.0 / ((y - b) / (t - a))) - (x / (z + -1.0));
	} else if ((((x * y) + (z * (t - a))) / (y + (z * (b - y)))) <= -3.0865535911923863e-232) {
		tmp = 1.0 / ((y + (z * (b - y))) / ((x * y) + (z * (t - a))));
	} else if ((((x * y) + (z * (t - a))) / (y + (z * (b - y)))) <= 0.0) {
		tmp = (t / (b - y)) + (((((x * y) / z) / (b - y)) + ((a / z) * (y / pow((b - y), 2.0)))) - (((y / pow((b - y), 2.0)) * (t / z)) + (a / (b - y))));
	} else if ((((x * y) + (z * (t - a))) / (y + (z * (b - y)))) <= 1.3387691926349812e+279) {
		tmp = (((x * y) + (z * t)) - (z * a)) / (y + (z * (b - y)));
	} else if ((((x * y) + (z * (t - a))) / (y + (z * (b - y)))) <= ((double) INFINITY)) {
		tmp = (y / ((y + (z * (b - y))) / x)) + (z / ((y + (z * (b - y))) / (t - a)));
	} else {
		tmp = (t / (b - y)) + ((((a / z) * (y / pow((b - y), 2.0))) + ((y / z) * (x / (b - y)))) - ((a / (b - y)) + ((y / z) * (t / pow((b - y), 2.0)))));
	}
	return tmp;
}

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.3
Target	18.3
Herbie	1.4

\[\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 6 regimes

2. if (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < -1.0776202918311757e307

   1. Initial program 63.5

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

   2. Taylor expanded around 0 63.5

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

   3. Simplified 34.8

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

   5. Applied div-inv_binary64_16784 34.9

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

   6. Applied add-cube-cbrt_binary64_16822 35.3

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

   7. Applied times-frac_binary64_16793 42.9

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

   8. Simplified 42.9

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

   9. Taylor expanded around -inf 34.6

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

   10. Simplified 34.7

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

   11. Taylor expanded around -inf 2.9

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

   12. Simplified 2.9

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

   if -1.0776202918311757e307 < (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < -3.08655359119238627e-232

   1. Initial program 0.3

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

   3. Applied clear-num_binary64_16786 0.4

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

   if -3.08655359119238627e-232 < (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < 0.0

   1. Initial program 41.5

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

   2. Taylor expanded around inf 20.7

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

   3. Simplified 5.1

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

   if 0.0 < (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < 1.3387691926349812e279

   1. Initial program 0.3

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

   3. Applied sub-neg_binary64_16780 0.3

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

   4. Applied distribute-rgt-in_binary64_16737 0.3

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

   5. Applied associate-+r+_binary64_16719 0.3

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

   if 1.3387691926349812e279 < (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < +inf.0

   1. Initial program 57.6

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

   2. Taylor expanded around 0 57.6

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

   3. Simplified 33.8

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

   5. Applied associate-/l*_binary64_16732 4.7

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

   if +inf.0 < (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y))))

   1. Initial program 64.0

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

   2. Taylor expanded around inf 39.8

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

   3. Simplified 0.2

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

4. Final simplification 1.4

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq -1.0776202918311757 \cdot 10^{+307}:\\ \;\;\;\;\frac{-1}{\frac{y - b}{t - a}} - \frac{x}{z + -1}\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq -3.0865535911923863 \cdot 10^{-232}:\\ \;\;\;\;\frac{1}{\frac{y + z \cdot \left(b - y\right)}{x \cdot y + z \cdot \left(t - a\right)}}\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq 0:\\ \;\;\;\;\frac{t}{b - y} + \left(\left(\frac{\frac{x \cdot y}{z}}{b - y} + \frac{a}{z} \cdot \frac{y}{{\left(b - y\right)}^{2}}\right) - \left(\frac{y}{{\left(b - y\right)}^{2}} \cdot \frac{t}{z} + \frac{a}{b - y}\right)\right)\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq 1.3387691926349812 \cdot 10^{+279}:\\ \;\;\;\;\frac{\left(x \cdot y + z \cdot t\right) - z \cdot a}{y + z \cdot \left(b - y\right)}\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq \infty:\\ \;\;\;\;\frac{y}{\frac{y + z \cdot \left(b - y\right)}{x}} + \frac{z}{\frac{y + z \cdot \left(b - y\right)}{t - a}}\\ \mathbf{else}:\\ \;\;\;\;\frac{t}{b - y} + \left(\left(\frac{a}{z} \cdot \frac{y}{{\left(b - y\right)}^{2}} + \frac{y}{z} \cdot \frac{x}{b - y}\right) - \left(\frac{a}{b - y} + \frac{y}{z} \cdot \frac{t}{{\left(b - y\right)}^{2}}\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2021176 
(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)))))