\[\frac{a \cdot c + b \cdot d}{c \cdot c + d \cdot d}
\]
↓
\[\begin{array}{l}
t_0 := \frac{a \cdot c + b \cdot d}{c \cdot c + d \cdot d}\\
\mathbf{if}\;t_0 \leq -4 \cdot 10^{+277}:\\
\;\;\;\;\frac{a}{c + d \cdot \frac{d}{c}}\\
\mathbf{elif}\;t_0 \leq 2 \cdot 10^{+282}:\\
\;\;\;\;\frac{1}{\mathsf{hypot}\left(c, d\right)} \cdot \frac{\mathsf{fma}\left(a, c, b \cdot d\right)}{\mathsf{hypot}\left(c, d\right)}\\
\mathbf{else}:\\
\;\;\;\;\frac{a}{c} + \frac{d}{c} \cdot \frac{b}{c}\\
\end{array}
\]
(FPCore (a b c d)
:precision binary64
(/ (+ (* a c) (* b d)) (+ (* c c) (* d d))))
↓
(FPCore (a b c d)
:precision binary64
(let* ((t_0 (/ (+ (* a c) (* b d)) (+ (* c c) (* d d)))))
(if (<= t_0 -4e+277)
(/ a (+ c (* d (/ d c))))
(if (<= t_0 2e+282)
(* (/ 1.0 (hypot c d)) (/ (fma a c (* b d)) (hypot c d)))
(+ (/ a c) (* (/ d c) (/ b c)))))))
double code(double a, double b, double c, double d) {
return ((a * c) + (b * d)) / ((c * c) + (d * d));
}
↓
double code(double a, double b, double c, double d) {
double t_0 = ((a * c) + (b * d)) / ((c * c) + (d * d));
double tmp;
if (t_0 <= -4e+277) {
tmp = a / (c + (d * (d / c)));
} else if (t_0 <= 2e+282) {
tmp = (1.0 / hypot(c, d)) * (fma(a, c, (b * d)) / hypot(c, d));
} else {
tmp = (a / c) + ((d / c) * (b / c));
}
return tmp;
}
function code(a, b, c, d)
return Float64(Float64(Float64(a * c) + Float64(b * d)) / Float64(Float64(c * c) + Float64(d * d)))
end
↓
function code(a, b, c, d)
t_0 = Float64(Float64(Float64(a * c) + Float64(b * d)) / Float64(Float64(c * c) + Float64(d * d)))
tmp = 0.0
if (t_0 <= -4e+277)
tmp = Float64(a / Float64(c + Float64(d * Float64(d / c))));
elseif (t_0 <= 2e+282)
tmp = Float64(Float64(1.0 / hypot(c, d)) * Float64(fma(a, c, Float64(b * d)) / hypot(c, d)));
else
tmp = Float64(Float64(a / c) + Float64(Float64(d / c) * Float64(b / c)));
end
return tmp
end
if (/.f64 (+.f64 (*.f64 a c) (*.f64 b d)) (+.f64 (*.f64 c c) (*.f64 d d))) < -4.00000000000000001e277
Initial program 52.7
\[\frac{a \cdot c + b \cdot d}{c \cdot c + d \cdot d}
\]
Applied egg-rr58.7
\[\leadsto \frac{\color{blue}{\frac{{\left(a \cdot c\right)}^{2}}{a \cdot c - b \cdot d} - \frac{{\left(b \cdot d\right)}^{2}}{a \cdot c - b \cdot d}}}{c \cdot c + d \cdot d}
\]
Simplified58.7
\[\leadsto \frac{\color{blue}{\frac{{\left(d \cdot b\right)}^{2} - {\left(c \cdot a\right)}^{2}}{d \cdot b - c \cdot a}}}{c \cdot c + d \cdot d}
\]
Proof
[Start]58.7
\[ \frac{\frac{{\left(a \cdot c\right)}^{2}}{a \cdot c - b \cdot d} - \frac{{\left(b \cdot d\right)}^{2}}{a \cdot c - b \cdot d}}{c \cdot c + d \cdot d}
\]
div-sub [<=]58.7
\[ \frac{\color{blue}{\frac{{\left(a \cdot c\right)}^{2} - {\left(b \cdot d\right)}^{2}}{a \cdot c - b \cdot d}}}{c \cdot c + d \cdot d}
\]
*-rgt-identity [<=]58.7
\[ \frac{\frac{\color{blue}{\left({\left(a \cdot c\right)}^{2} - {\left(b \cdot d\right)}^{2}\right) \cdot 1}}{a \cdot c - b \cdot d}}{c \cdot c + d \cdot d}
\]
associate-*r/ [<=]58.7
\[ \frac{\color{blue}{\left({\left(a \cdot c\right)}^{2} - {\left(b \cdot d\right)}^{2}\right) \cdot \frac{1}{a \cdot c - b \cdot d}}}{c \cdot c + d \cdot d}
\]
*-rgt-identity [<=]58.7
\[ \frac{\color{blue}{\left(\left({\left(a \cdot c\right)}^{2} - {\left(b \cdot d\right)}^{2}\right) \cdot 1\right)} \cdot \frac{1}{a \cdot c - b \cdot d}}{c \cdot c + d \cdot d}
\]
*-commutative [=>]58.7
\[ \frac{\color{blue}{\left(1 \cdot \left({\left(a \cdot c\right)}^{2} - {\left(b \cdot d\right)}^{2}\right)\right)} \cdot \frac{1}{a \cdot c - b \cdot d}}{c \cdot c + d \cdot d}
\]
associate-*l* [=>]58.7
\[ \frac{\color{blue}{1 \cdot \left(\left({\left(a \cdot c\right)}^{2} - {\left(b \cdot d\right)}^{2}\right) \cdot \frac{1}{a \cdot c - b \cdot d}\right)}}{c \cdot c + d \cdot d}
\]
metadata-eval [<=]58.7
\[ \frac{\color{blue}{\frac{-1}{-1}} \cdot \left(\left({\left(a \cdot c\right)}^{2} - {\left(b \cdot d\right)}^{2}\right) \cdot \frac{1}{a \cdot c - b \cdot d}\right)}{c \cdot c + d \cdot d}
\]
associate-*r/ [=>]58.7
\[ \frac{\frac{-1}{-1} \cdot \color{blue}{\frac{\left({\left(a \cdot c\right)}^{2} - {\left(b \cdot d\right)}^{2}\right) \cdot 1}{a \cdot c - b \cdot d}}}{c \cdot c + d \cdot d}
\]
*-rgt-identity [=>]58.7
\[ \frac{\frac{-1}{-1} \cdot \frac{\color{blue}{{\left(a \cdot c\right)}^{2} - {\left(b \cdot d\right)}^{2}}}{a \cdot c - b \cdot d}}{c \cdot c + d \cdot d}
\]
times-frac [<=]58.7
\[ \frac{\color{blue}{\frac{-1 \cdot \left({\left(a \cdot c\right)}^{2} - {\left(b \cdot d\right)}^{2}\right)}{-1 \cdot \left(a \cdot c - b \cdot d\right)}}}{c \cdot c + d \cdot d}
\]
neg-mul-1 [<=]58.7
\[ \frac{\frac{-1 \cdot \left({\left(a \cdot c\right)}^{2} - {\left(b \cdot d\right)}^{2}\right)}{\color{blue}{-\left(a \cdot c - b \cdot d\right)}}}{c \cdot c + d \cdot d}
\]
herbie shell --seed 2023066
(FPCore (a b c d)
:name "Complex division, real part"
:precision binary64
:herbie-target
(if (< (fabs d) (fabs c)) (/ (+ a (* b (/ d c))) (+ c (* d (/ d c)))) (/ (+ b (* a (/ c d))) (+ d (* c (/ c d)))))
(/ (+ (* a c) (* b d)) (+ (* c c) (* d d))))