\[\begin{array}{l}
t_1 := x \cdot y - z \cdot t\\
\mathbf{if}\;t_1 \leq -5 \cdot 10^{+276} \lor \neg \left(t_1 \leq 2 \cdot 10^{+210}\right):\\
\;\;\;\;\frac{x}{\frac{a}{y}} - \frac{z}{\frac{a}{t}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\mathsf{fma}\left(x, y, z \cdot \left(-t\right)\right)}{a}\\
\end{array}
\]
(FPCore (x y z t a) :precision binary64 (/ (- (* x y) (* z t)) a))
↓
(FPCore (x y z t a)
:precision binary64
(let* ((t_1 (- (* x y) (* z t))))
(if (or (<= t_1 -5e+276) (not (<= t_1 2e+210)))
(- (/ x (/ a y)) (/ z (/ a t)))
(/ (fma x y (* z (- t))) a))))
double code(double x, double y, double z, double t, double a) {
return ((x * y) - (z * t)) / a;
}
↓
double code(double x, double y, double z, double t, double a) {
double t_1 = (x * y) - (z * t);
double tmp;
if ((t_1 <= -5e+276) || !(t_1 <= 2e+210)) {
tmp = (x / (a / y)) - (z / (a / t));
} else {
tmp = fma(x, y, (z * -t)) / a;
}
return tmp;
}
function code(x, y, z, t, a)
return Float64(Float64(Float64(x * y) - Float64(z * t)) / a)
end
↓
function code(x, y, z, t, a)
t_1 = Float64(Float64(x * y) - Float64(z * t))
tmp = 0.0
if ((t_1 <= -5e+276) || !(t_1 <= 2e+210))
tmp = Float64(Float64(x / Float64(a / y)) - Float64(z / Float64(a / t)));
else
tmp = Float64(fma(x, y, Float64(z * Float64(-t))) / a);
end
return tmp
end
if -5.00000000000000001e276 < (-.f64 (*.f64 x y) (*.f64 z t)) < 1.99999999999999985e210
Initial program 1.17
\[\frac{x \cdot y - z \cdot t}{a}
\]
Simplified1.16
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(x, y, z \cdot \left(-t\right)\right)}{a}}
\]
Proof
[Start]1.17
\[ \frac{x \cdot y - z \cdot t}{a}
\]
fma-neg [=>]1.16
\[ \frac{\color{blue}{\mathsf{fma}\left(x, y, -z \cdot t\right)}}{a}
\]
distribute-rgt-neg-in [=>]1.16
\[ \frac{\mathsf{fma}\left(x, y, \color{blue}{z \cdot \left(-t\right)}\right)}{a}
\]
Recombined 2 regimes into one program.
Final simplification1.22
\[\leadsto \begin{array}{l}
\mathbf{if}\;x \cdot y - z \cdot t \leq -5 \cdot 10^{+276} \lor \neg \left(x \cdot y - z \cdot t \leq 2 \cdot 10^{+210}\right):\\
\;\;\;\;\frac{x}{\frac{a}{y}} - \frac{z}{\frac{a}{t}}\\
\mathbf{else}:\\
\;\;\;\;\frac{\mathsf{fma}\left(x, y, z \cdot \left(-t\right)\right)}{a}\\
\end{array}
\]
herbie shell --seed 2023121
(FPCore (x y z t a)
:name "Data.Colour.Matrix:inverse from colour-2.3.3, B"
:precision binary64
:herbie-target
(if (< z -2.468684968699548e+170) (- (* (/ y a) x) (* (/ t a) z)) (if (< z 6.309831121978371e-71) (/ (- (* x y) (* z t)) a) (- (* (/ y a) x) (* (/ t a) z))))
(/ (- (* x y) (* z t)) a))