\left(x \cdot y - z \cdot y\right) \cdot t
\begin{array}{l}
\mathbf{if}\;t \leq -6.925233186446084 \cdot 10^{-16}:\\
\;\;\;\;\left(t \cdot y\right) \cdot x - \left(t \cdot y\right) \cdot z\\
\mathbf{elif}\;t \leq 3.193401404254416 \cdot 10^{-44}:\\
\;\;\;\;y \cdot \left(t \cdot x\right) - y \cdot \left(t \cdot z\right)\\
\mathbf{else}:\\
\;\;\;\;t \cdot \left(y \cdot \left(x - z\right)\right)\\
\end{array}(FPCore (x y z t) :precision binary64 (* (- (* x y) (* z y)) t))
(FPCore (x y z t)
:precision binary64
(if (<= t -6.925233186446084e-16)
(- (* (* t y) x) (* (* t y) z))
(if (<= t 3.193401404254416e-44)
(- (* y (* t x)) (* y (* t z)))
(* t (* y (- x z))))))double code(double x, double y, double z, double t) {
return ((x * y) - (z * y)) * t;
}
double code(double x, double y, double z, double t) {
double tmp;
if (t <= -6.925233186446084e-16) {
tmp = ((t * y) * x) - ((t * y) * z);
} else if (t <= 3.193401404254416e-44) {
tmp = (y * (t * x)) - (y * (t * z));
} else {
tmp = t * (y * (x - z));
}
return tmp;
}




Bits error versus x




Bits error versus y




Bits error versus z




Bits error versus t
Results
| Original | 6.9 |
|---|---|
| Target | 3.0 |
| Herbie | 2.7 |
if t < -6.9252331864460843e-16Initial program 2.8
Simplified14.8
rmApplied associate-*r*_binary643.3
rmApplied sub-neg_binary643.3
Applied distribute-lft-in_binary643.3
if -6.9252331864460843e-16 < t < 3.19340140425441623e-44Initial program 9.8
Simplified2.2
rmApplied sub-neg_binary642.2
Applied distribute-lft-in_binary642.2
Applied distribute-lft-in_binary642.2
if 3.19340140425441623e-44 < t Initial program 3.4
Simplified13.7
rmApplied sub-neg_binary6413.7
Applied distribute-lft-in_binary6413.7
Applied distribute-lft-in_binary6413.7
Taylor expanded around inf 3.4
Simplified3.4
Final simplification2.7
herbie shell --seed 2020220
(FPCore (x y z t)
:name "Linear.Projection:inverseInfinitePerspective from linear-1.19.1.3"
:precision binary64
:herbie-target
(if (< t -9.231879582886777e-80) (* (* y t) (- x z)) (if (< t 2.543067051564877e+83) (* y (* t (- x z))) (* (* y (- x z)) t)))
(* (- (* x y) (* z y)) t))