(FPCore (x y z t a b)
:precision binary64
(/ (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (+ (+ x t) y)))
↓
(FPCore (x y z t a b)
:precision binary64
(let* ((t_1 (+ y (+ x t))))
(if (<= z -4.2e+156)
(/ (+ y x) (/ t_1 z))
(if (<= z 4.2e+148)
(+ (/ (- z b) (/ t_1 y)) (+ (/ a (/ t_1 (+ y t))) (/ (* z x) t_1)))
(* z (/ (+ y x) t_1))))))
double code(double x, double y, double z, double t, double a, double b) {
double t_1 = y + (x + t);
double tmp;
if (z <= -4.2e+156) {
tmp = (y + x) / (t_1 / z);
} else if (z <= 4.2e+148) {
tmp = ((z - b) / (t_1 / y)) + ((a / (t_1 / (y + t))) + ((z * x) / t_1));
} else {
tmp = z * ((y + x) / t_1);
}
return tmp;
}
real(8) function code(x, y, z, t, a, b)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: t
real(8), intent (in) :: a
real(8), intent (in) :: b
code = ((((x + y) * z) + ((t + y) * a)) - (y * b)) / ((x + t) + y)
end function
↓
real(8) function code(x, y, z, t, a, b)
real(8), intent (in) :: x
real(8), intent (in) :: y
real(8), intent (in) :: z
real(8), intent (in) :: t
real(8), intent (in) :: a
real(8), intent (in) :: b
real(8) :: t_1
real(8) :: tmp
t_1 = y + (x + t)
if (z <= (-4.2d+156)) then
tmp = (y + x) / (t_1 / z)
else if (z <= 4.2d+148) then
tmp = ((z - b) / (t_1 / y)) + ((a / (t_1 / (y + t))) + ((z * x) / t_1))
else
tmp = z * ((y + x) / t_1)
end if
code = tmp
end function
public static double code(double x, double y, double z, double t, double a, double b) {
return ((((x + y) * z) + ((t + y) * a)) - (y * b)) / ((x + t) + y);
}
↓
public static double code(double x, double y, double z, double t, double a, double b) {
double t_1 = y + (x + t);
double tmp;
if (z <= -4.2e+156) {
tmp = (y + x) / (t_1 / z);
} else if (z <= 4.2e+148) {
tmp = ((z - b) / (t_1 / y)) + ((a / (t_1 / (y + t))) + ((z * x) / t_1));
} else {
tmp = z * ((y + x) / t_1);
}
return tmp;
}
(/.f64 (+.f64 y x) (/.f64 (+.f64 y (+.f64 t x)) z)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 y x) (/.f64 (Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 y t) x)) z)): 6 points increase in error, 0 points decrease in error
(/.f64 (+.f64 y x) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 x (+.f64 y t))) z)): 0 points increase in error, 6 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 y x) z) (+.f64 x (+.f64 y t)))): 3 points increase in error, 3 points decrease in error
(/.f64 (*.f64 (+.f64 y x) z) (Rewrite=> +-commutative_binary64 (+.f64 (+.f64 y t) x))): 0 points increase in error, 3 points decrease in error
(/.f64 (*.f64 (+.f64 y x) z) (Rewrite<= associate-+r+_binary64 (+.f64 y (+.f64 t x)))): 3 points increase in error, 3 points decrease in error
if -4.19999999999999963e156 < z < 4.19999999999999998e148
Initial program 21.8
\[\frac{\left(\left(x + y\right) \cdot z + \left(t + y\right) \cdot a\right) - y \cdot b}{\left(x + t\right) + y}
\]
Simplified21.8
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(y, z - b, \mathsf{fma}\left(y + t, a, x \cdot z\right)\right)}{x + \left(y + t\right)}}
\]
Proof
(/.f64 (fma.f64 y (-.f64 z b) (fma.f64 (+.f64 y t) a (*.f64 x z))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 y (-.f64 z b) (fma.f64 (Rewrite<= +-commutative_binary64 (+.f64 t y)) a (*.f64 x z))) (+.f64 x (+.f64 y t))): 0 points increase in error, 17 points decrease in error
(/.f64 (fma.f64 y (-.f64 z b) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (+.f64 t y) a) (*.f64 x z)))) (+.f64 x (+.f64 y t))): 17 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 y (-.f64 z b) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 x z) (*.f64 (+.f64 t y) a)))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 y (-.f64 z b)) (+.f64 (*.f64 x z) (*.f64 (+.f64 t y) a)))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 y z) (*.f64 y b))) (+.f64 (*.f64 x z) (*.f64 (+.f64 t y) a))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite=> sub-neg_binary64 (+.f64 (*.f64 y z) (neg.f64 (*.f64 y b)))) (+.f64 (*.f64 x z) (*.f64 (+.f64 t y) a))) (+.f64 x (+.f64 y t))): 0 points increase in error, 17 points decrease in error
(/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 x z) (*.f64 (+.f64 t y) a)) (+.f64 (*.f64 y z) (neg.f64 (*.f64 y b))))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (+.f64 (*.f64 x z) (*.f64 (+.f64 t y) a)) (*.f64 y z)) (neg.f64 (*.f64 y b)))) (+.f64 x (+.f64 y t))): 17 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 y z) (+.f64 (*.f64 x z) (*.f64 (+.f64 t y) a)))) (neg.f64 (*.f64 y b))) (+.f64 x (+.f64 y t))): 0 points increase in error, 17 points decrease in error
(/.f64 (+.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 y z) (*.f64 x z)) (*.f64 (+.f64 t y) a))) (neg.f64 (*.f64 y b))) (+.f64 x (+.f64 y t))): 17 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (+.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 z (+.f64 y x))) (*.f64 (+.f64 t y) a)) (neg.f64 (*.f64 y b))) (+.f64 x (+.f64 y t))): 0 points increase in error, 17 points decrease in error
(/.f64 (+.f64 (+.f64 (*.f64 z (Rewrite<= +-commutative_binary64 (+.f64 x y))) (*.f64 (+.f64 t y) a)) (neg.f64 (*.f64 y b))) (+.f64 x (+.f64 y t))): 4 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 x y) z)) (*.f64 (+.f64 t y) a)) (neg.f64 (*.f64 y b))) (+.f64 x (+.f64 y t))): 0 points increase in error, 4 points decrease in error
(/.f64 (Rewrite<= sub-neg_binary64 (-.f64 (+.f64 (*.f64 (+.f64 x y) z) (*.f64 (+.f64 t y) a)) (*.f64 y b))) (+.f64 x (+.f64 y t))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (+.f64 (*.f64 (+.f64 x y) z) (*.f64 (+.f64 t y) a)) (*.f64 y b)) (+.f64 x (Rewrite<= +-commutative_binary64 (+.f64 t y)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (+.f64 (*.f64 (+.f64 x y) z) (*.f64 (+.f64 t y) a)) (*.f64 y b)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 x t) y))): 17 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (-.f64 z b) (/.f64 (+.f64 (+.f64 x t) y) y)) (+.f64 (/.f64 a (/.f64 (+.f64 (+.f64 x t) y) (+.f64 t y))) (/.f64 (*.f64 z x) (+.f64 (+.f64 x t) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (-.f64 z b) (/.f64 (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 t x)) y) y)) (+.f64 (/.f64 a (/.f64 (+.f64 (+.f64 x t) y) (+.f64 t y))) (/.f64 (*.f64 z x) (+.f64 (+.f64 x t) y)))): 0 points increase in error, 11 points decrease in error
(+.f64 (/.f64 (-.f64 z b) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 y (+.f64 t x))) y)) (+.f64 (/.f64 a (/.f64 (+.f64 (+.f64 x t) y) (+.f64 t y))) (/.f64 (*.f64 z x) (+.f64 (+.f64 x t) y)))): 4 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x)))) (+.f64 (/.f64 a (/.f64 (+.f64 (+.f64 x t) y) (+.f64 t y))) (/.f64 (*.f64 z x) (+.f64 (+.f64 x t) y)))): 4 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 a (/.f64 (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 t x)) y) (+.f64 t y))) (/.f64 (*.f64 z x) (+.f64 (+.f64 x t) y)))): 3 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 a (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 y (+.f64 t x))) (+.f64 t y))) (/.f64 (*.f64 z x) (+.f64 (+.f64 x t) y)))): 0 points increase in error, 7 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 a (/.f64 (+.f64 y (+.f64 t x)) (Rewrite<= +-commutative_binary64 (+.f64 y t)))) (/.f64 (*.f64 z x) (+.f64 (+.f64 x t) y)))): 0 points increase in error, 11 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x)))) (/.f64 (*.f64 z x) (+.f64 (+.f64 x t) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x))) (/.f64 (*.f64 z x) (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 t x)) y)))): 11 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (+.f64 (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x))) (/.f64 (*.f64 z x) (Rewrite<= +-commutative_binary64 (+.f64 y (+.f64 t x)))))): 0 points increase in error, 11 points decrease in error
(+.f64 (/.f64 (*.f64 (-.f64 z b) y) (+.f64 y (+.f64 t x))) (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (*.f64 z x) (+.f64 y (+.f64 t x))) (/.f64 (*.f64 a (+.f64 y t)) (+.f64 y (+.f64 t x)))))): 4 points increase in error, 0 points decrease in error
if 4.19999999999999998e148 < z
Initial program 42.8
\[\frac{\left(\left(x + y\right) \cdot z + \left(t + y\right) \cdot a\right) - y \cdot b}{\left(x + t\right) + y}
\]
herbie shell --seed 2022343
(FPCore (x y z t a b)
:name "AI.Clustering.Hierarchical.Internal:ward from clustering-0.2.1"
:precision binary64
:herbie-target
(if (< (/ (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (+ (+ x t) y)) -3.5813117084150564e+153) (- (+ z a) b) (if (< (/ (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (+ (+ x t) y)) 1.2285964308315609e+82) (/ 1.0 (/ (+ (+ x t) y) (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)))) (- (+ z a) b)))
(/ (- (+ (* (+ x y) z) (* (+ t y) a)) (* y b)) (+ (+ x t) y)))