(FPCore (a b c d)
:precision binary64
(/ (- (* b c) (* a d)) (+ (* c c) (* d d))))
↓
(FPCore (a b c d)
:precision binary64
(let* ((t_0 (- (* d a))) (t_1 (/ c (hypot c d))) (t_2 (/ b (hypot c d))))
(if (<= d -1.5e+98)
(fma t_1 t_2 (/ (- a) d))
(if (<= d -1.22e-197)
(/ (/ (fma c b t_0) (hypot c d)) (hypot c d))
(if (<= d 8.5e-179)
(/ (- b (* a (/ d c))) c)
(if (<= d 2.6e+67)
(fma t_1 t_2 (/ t_0 (pow (hypot c d) 2.0)))
(/ (- (/ c (/ d b)) a) (hypot c d))))))))
double code(double a, double b, double c, double d) {
return ((b * c) - (a * d)) / ((c * c) + (d * d));
}
(-.f64 (/.f64 b c) (/.f64 a (/.f64 (*.f64 c c) d))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 b c) (/.f64 a (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) d))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 b c) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 a d) (pow.f64 c 2)))): 24 points increase in error, 10 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 b c) (neg.f64 (/.f64 (*.f64 a d) (pow.f64 c 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 b c) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 a d) (pow.f64 c 2))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 a d) (pow.f64 c 2))) (/.f64 b c))): 0 points increase in error, 0 points decrease in error
\[\leadsto \color{blue}{\frac{b - a \cdot \frac{d}{c}}{c}}
\]
Proof
(/.f64 (-.f64 b (*.f64 a (/.f64 d c))) c): 0 points increase in error, 0 points decrease in error
(Rewrite=> div-sub_binary64 (-.f64 (/.f64 b c) (/.f64 (*.f64 a (/.f64 d c)) c))): 0 points increase in error, 1 points decrease in error
(-.f64 (/.f64 b c) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 a c) (/.f64 d c)))): 13 points increase in error, 18 points decrease in error
(-.f64 (/.f64 b c) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 a d) (*.f64 c c)))): 45 points increase in error, 13 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 b c) (neg.f64 (/.f64 (*.f64 a d) (*.f64 c c))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 b c) (neg.f64 (/.f64 (*.f64 a d) (Rewrite<= unpow2_binary64 (pow.f64 c 2))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 b c) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 a d) (pow.f64 c 2))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 a d) (pow.f64 c 2))) (/.f64 b c))): 0 points increase in error, 0 points decrease in error
if 8.49999999999999932e-179 < d < 2.6e67
Initial program 14.9
\[\frac{b \cdot c - a \cdot d}{c \cdot c + d \cdot d}
\]
herbie shell --seed 2022325
(FPCore (a b c d)
:name "Complex division, imag part"
:precision binary64
:herbie-target
(if (< (fabs d) (fabs c)) (/ (- b (* a (/ d c))) (+ c (* d (/ d c)))) (/ (+ (- a) (* b (/ c d))) (+ d (* c (/ c d)))))
(/ (- (* b c) (* a d)) (+ (* c c) (* d d))))