Development.Shake.Progress:decay from shake-0.15.5

Average Error: 22.9 → 6.1

Time: 29.4s

Precision: binary64

Math

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

↓

\[\begin{array}{l} t_1 := {\left(b - y\right)}^{2}\\ t_2 := \mathsf{fma}\left(\frac{y}{b - y}, \frac{x}{z}, \mathsf{fma}\left(\frac{a}{t_1}, \frac{y}{z}, \frac{t}{b - y}\right)\right) - \mathsf{fma}\left(\frac{y}{t_1}, \frac{t}{z}, \frac{a}{b - y}\right)\\ \mathbf{if}\;z \leq -369640450397408.9:\\ \;\;\;\;t_2\\ \mathbf{elif}\;z \leq -3.910612387742409 \cdot 10^{-279}:\\ \;\;\;\;\frac{\mathsf{fma}\left(x, y, z \cdot t - z \cdot a\right)}{\mathsf{fma}\left(z, b - y, y\right)}\\ \mathbf{else}:\\ \;\;\;\;\begin{array}{l} t_3 := \left(y + z \cdot b\right) - z \cdot y\\ t_4 := \frac{z \cdot t}{t_3}\\ \mathbf{if}\;z \leq 6.002196668933548 \cdot 10^{-210}:\\ \;\;\;\;t_4 + \left(\mathsf{fma}\left(z, x, x\right) - \left(\frac{z \cdot a}{y} + \frac{b \cdot \left(z \cdot x\right)}{y}\right)\right)\\ \mathbf{elif}\;z \leq 95120340125.92792:\\ \;\;\;\;t_4 + \frac{\mathsf{fma}\left(x, y, z \cdot \left(-a\right)\right) + \mathsf{fma}\left(-a, z, z \cdot a\right)}{t_3}\\ \mathbf{else}:\\ \;\;\;\;t_2\\ \end{array}\\ \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
 (let* ((t_1 (pow (- b y) 2.0))
        (t_2
         (-
          (fma (/ y (- b y)) (/ x z) (fma (/ a t_1) (/ y z) (/ t (- b y))))
          (fma (/ y t_1) (/ t z) (/ a (- b y))))))
   (if (<= z -369640450397408.9)
     t_2
     (if (<= z -3.910612387742409e-279)
       (/ (fma x y (- (* z t) (* z a))) (fma z (- b y) y))
       (let* ((t_3 (- (+ y (* z b)) (* z y))) (t_4 (/ (* z t) t_3)))
         (if (<= z 6.002196668933548e-210)
           (+ t_4 (- (fma z x x) (+ (/ (* z a) y) (/ (* b (* z x)) y))))
           (if (<= z 95120340125.92792)
             (+ t_4 (/ (+ (fma x y (* z (- a))) (fma (- a) z (* z a))) t_3))
             t_2)))))))

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 t_1 = pow((b - y), 2.0);
	double t_2 = fma((y / (b - y)), (x / z), fma((a / t_1), (y / z), (t / (b - y)))) - fma((y / t_1), (t / z), (a / (b - y)));
	double tmp;
	if (z <= -369640450397408.9) {
		tmp = t_2;
	} else if (z <= -3.910612387742409e-279) {
		tmp = fma(x, y, ((z * t) - (z * a))) / fma(z, (b - y), y);
	} else {
		double t_3 = (y + (z * b)) - (z * y);
		double t_4 = (z * t) / t_3;
		double tmp_1;
		if (z <= 6.002196668933548e-210) {
			tmp_1 = t_4 + (fma(z, x, x) - (((z * a) / y) + ((b * (z * x)) / y)));
		} else if (z <= 95120340125.92792) {
			tmp_1 = t_4 + ((fma(x, y, (z * -a)) + fma(-a, z, (z * a))) / t_3);
		} else {
			tmp_1 = t_2;
		}
		tmp = tmp_1;
	}
	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	22.9
Target	18.0
Herbie	6.1

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

2. if z < -369640450397408.88 or 95120340125.927917 < z

   1. Initial program 39.1

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

   2. Simplified 39.1

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

   3. Taylor expanded in z around inf 22.2

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

   4. Simplified 3.6

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

   if -369640450397408.88 < z < -3.9106123877424087e-279

   1. Initial program 8.7

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

   2. Simplified 8.7

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

   3. Applied *-un-lft-identity_binary64 8.7

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

   4. Applied cancel-sign-sub-inv_binary64 8.7

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

   5. Applied distribute-lft-in_binary64 8.7

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

   if -3.9106123877424087e-279 < z < 6.0021966689335478e-210

   1. Initial program 8.5

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

   2. Simplified 8.5

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

   3. Applied clear-num_binary64 8.7

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

   4. Taylor expanded in x around 0 8.5

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

   5. Simplified 8.5

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

   6. Taylor expanded in z around 0 14.6

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

   7. Simplified 9.4

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

   if 6.0021966689335478e-210 < z < 95120340125.927917

   1. Initial program 7.5

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

   2. Simplified 7.5

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

   3. Applied clear-num_binary64 7.7

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

   4. Taylor expanded in x around 0 7.5

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

   5. Simplified 7.5

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

   6. Applied prod-diff_binary64 7.5

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

4. Final simplification 6.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;z \leq -369640450397408.9:\\ \;\;\;\;\mathsf{fma}\left(\frac{y}{b - y}, \frac{x}{z}, \mathsf{fma}\left(\frac{a}{{\left(b - y\right)}^{2}}, \frac{y}{z}, \frac{t}{b - y}\right)\right) - \mathsf{fma}\left(\frac{y}{{\left(b - y\right)}^{2}}, \frac{t}{z}, \frac{a}{b - y}\right)\\ \mathbf{elif}\;z \leq -3.910612387742409 \cdot 10^{-279}:\\ \;\;\;\;\frac{\mathsf{fma}\left(x, y, z \cdot t - z \cdot a\right)}{\mathsf{fma}\left(z, b - y, y\right)}\\ \mathbf{elif}\;z \leq 6.002196668933548 \cdot 10^{-210}:\\ \;\;\;\;\frac{z \cdot t}{\left(y + z \cdot b\right) - z \cdot y} + \left(\mathsf{fma}\left(z, x, x\right) - \left(\frac{z \cdot a}{y} + \frac{b \cdot \left(z \cdot x\right)}{y}\right)\right)\\ \mathbf{elif}\;z \leq 95120340125.92792:\\ \;\;\;\;\frac{z \cdot t}{\left(y + z \cdot b\right) - z \cdot y} + \frac{\mathsf{fma}\left(x, y, z \cdot \left(-a\right)\right) + \mathsf{fma}\left(-a, z, z \cdot a\right)}{\left(y + z \cdot b\right) - z \cdot y}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\frac{y}{b - y}, \frac{x}{z}, \mathsf{fma}\left(\frac{a}{{\left(b - y\right)}^{2}}, \frac{y}{z}, \frac{t}{b - y}\right)\right) - \mathsf{fma}\left(\frac{y}{{\left(b - y\right)}^{2}}, \frac{t}{z}, \frac{a}{b - y}\right)\\ \end{array} \]

Reproduce

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