Development.Shake.Progress:decay from shake-0.15.5

Average Error: 23.5 → 7.5

Time: 21.6s

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 -\infty:\\ \;\;\;\;\left(\frac{a}{y \cdot z} + \frac{a - t}{y - b}\right) - \frac{y}{z} \cdot \left(\frac{t}{{\left(y - b\right)}^{2}} + \frac{x}{y - b}\right)\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq -4.0617195255428953 \cdot 10^{-278}:\\ \;\;\;\;\frac{x \cdot y}{y + z \cdot \left(b - y\right)} + \frac{z \cdot \left(t - a\right)}{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 0:\\ \;\;\;\;\left(\frac{a - t}{y - b} + \frac{y \cdot a}{z \cdot {\left(y - b\right)}^{2}}\right) - \frac{y}{z} \cdot \left(\frac{t}{{\left(y - b\right)}^{2}} + \frac{x}{y - b}\right)\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq 1.2517468488886882 \cdot 10^{+308}:\\ \;\;\;\;\left(\frac{z \cdot t}{\left(y + z \cdot b\right) - y \cdot z} + \frac{x \cdot y}{\left(y + z \cdot b\right) - y \cdot z}\right) - \frac{z \cdot a}{\left(y + z \cdot b\right) - y \cdot z}\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq \infty:\\ \;\;\;\;\frac{x}{1 - z}\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{a}{y \cdot z} + \frac{a - t}{y - b}\right) - \frac{y}{z} \cdot \left(\frac{t}{{\left(y - b\right)}^{2}} + \frac{x}{y - b}\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)))) (- INFINITY))
   (-
    (+ (/ a (* y z)) (/ (- a t) (- y b)))
    (* (/ y z) (+ (/ t (pow (- y b) 2.0)) (/ x (- y b)))))
   (if (<=
        (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y))))
        -4.0617195255428953e-278)
     (+ (/ (* x y) (+ y (* z (- b y)))) (/ (* z (- t a)) (+ y (* z (- b y)))))
     (if (<= (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) 0.0)
       (-
        (+ (/ (- a t) (- y b)) (/ (* y a) (* z (pow (- y b) 2.0))))
        (* (/ y z) (+ (/ t (pow (- y b) 2.0)) (/ x (- y b)))))
       (if (<=
            (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y))))
            1.2517468488886882e+308)
         (-
          (+
           (/ (* z t) (- (+ y (* z b)) (* y z)))
           (/ (* x y) (- (+ y (* z b)) (* y z))))
          (/ (* z a) (- (+ y (* z b)) (* y z))))
         (if (<= (/ (+ (* x y) (* z (- t a))) (+ y (* z (- b y)))) INFINITY)
           (/ x (- 1.0 z))
           (-
            (+ (/ a (* y z)) (/ (- a t) (- y b)))
            (* (/ y z) (+ (/ t (pow (- y b) 2.0)) (/ x (- y b)))))))))))

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)))) <= -((double) INFINITY)) {
		tmp = ((a / (y * z)) + ((a - t) / (y - b))) - ((y / z) * ((t / pow((y - b), 2.0)) + (x / (y - b))));
	} else if ((((x * y) + (z * (t - a))) / (y + (z * (b - y)))) <= -4.0617195255428953e-278) {
		tmp = ((x * y) / (y + (z * (b - y)))) + ((z * (t - a)) / (y + (z * (b - y))));
	} else if ((((x * y) + (z * (t - a))) / (y + (z * (b - y)))) <= 0.0) {
		tmp = (((a - t) / (y - b)) + ((y * a) / (z * pow((y - b), 2.0)))) - ((y / z) * ((t / pow((y - b), 2.0)) + (x / (y - b))));
	} else if ((((x * y) + (z * (t - a))) / (y + (z * (b - y)))) <= 1.2517468488886882e+308) {
		tmp = (((z * t) / ((y + (z * b)) - (y * z))) + ((x * y) / ((y + (z * b)) - (y * z)))) - ((z * a) / ((y + (z * b)) - (y * z)));
	} else if ((((x * y) + (z * (t - a))) / (y + (z * (b - y)))) <= ((double) INFINITY)) {
		tmp = x / (1.0 - z);
	} else {
		tmp = ((a / (y * z)) + ((a - t) / (y - b))) - ((y / z) * ((t / pow((y - b), 2.0)) + (x / (y - b))));
	}
	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.5
Target	17.8
Herbie	7.5

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

2. if (/.f64 (+.f64 (*.f64 x y) (*.f64 z (-.f64 t a))) (+.f64 y (*.f64 z (-.f64 b y)))) < -inf.0 or +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. Using strategy rm

   3. Applied add-cube-cbrt_binary64_17504 64.0

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

   4. Applied associate-*l*_binary64_17410 64.0

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

   5. Simplified 64.0

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

   6. Taylor expanded around -inf 40.4

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

   7. Simplified 24.4

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

   8. Taylor expanded around inf 18.2

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

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

   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 add-cube-cbrt_binary64_17504 0.8

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

   4. Applied associate-*l*_binary64_17410 0.8

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

   5. Simplified 0.8

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

   6. Taylor expanded around 0 0.3

      \[\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}}\]

   7. Simplified 0.3

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

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

   1. Initial program 45.2

      \[\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_binary64_17504 45.2

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

   4. Applied associate-*l*_binary64_17410 45.2

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

   5. Simplified 45.2

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

   6. Taylor expanded around -inf 20.2

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

   7. Simplified 9.7

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

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

   1. Initial program 0.3

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

   2. Taylor expanded around 0 0.3

      \[\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}}\]

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

   1. Initial program 63.9

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

   2. Taylor expanded around inf 31.4

      \[\leadsto \color{blue}{\frac{x}{1 - z}}\]
3. Recombined 5 regimes into one program.

4. Final simplification 7.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq -\infty:\\ \;\;\;\;\left(\frac{a}{y \cdot z} + \frac{a - t}{y - b}\right) - \frac{y}{z} \cdot \left(\frac{t}{{\left(y - b\right)}^{2}} + \frac{x}{y - b}\right)\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq -4.0617195255428953 \cdot 10^{-278}:\\ \;\;\;\;\frac{x \cdot y}{y + z \cdot \left(b - y\right)} + \frac{z \cdot \left(t - a\right)}{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 0:\\ \;\;\;\;\left(\frac{a - t}{y - b} + \frac{y \cdot a}{z \cdot {\left(y - b\right)}^{2}}\right) - \frac{y}{z} \cdot \left(\frac{t}{{\left(y - b\right)}^{2}} + \frac{x}{y - b}\right)\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq 1.2517468488886882 \cdot 10^{+308}:\\ \;\;\;\;\left(\frac{z \cdot t}{\left(y + z \cdot b\right) - y \cdot z} + \frac{x \cdot y}{\left(y + z \cdot b\right) - y \cdot z}\right) - \frac{z \cdot a}{\left(y + z \cdot b\right) - y \cdot z}\\ \mathbf{elif}\;\frac{x \cdot y + z \cdot \left(t - a\right)}{y + z \cdot \left(b - y\right)} \leq \infty:\\ \;\;\;\;\frac{x}{1 - z}\\ \mathbf{else}:\\ \;\;\;\;\left(\frac{a}{y \cdot z} + \frac{a - t}{y - b}\right) - \frac{y}{z} \cdot \left(\frac{t}{{\left(y - b\right)}^{2}} + \frac{x}{y - b}\right)\\ \end{array}\]

Reproduce

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