\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)
\begin{array}{l}
\mathbf{if}\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - a \cdot i\right)\right) + j \cdot \left(t \cdot c - y \cdot i\right) \leq 7.765624636983288 \cdot 10^{+305}:\\
\;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - a \cdot i\right)\right) + j \cdot \left(t \cdot c - y \cdot i\right)\\
\mathbf{else}:\\
\;\;\;\;j \cdot \left(t \cdot c - y \cdot i\right) - b \cdot \left(z \cdot c - a \cdot i\right)\\
\end{array}(FPCore (x y z t a b c i j) :precision binary64 (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (* j (- (* c t) (* i y)))))
(FPCore (x y z t a b c i j)
:precision binary64
(if (<=
(+
(- (* x (- (* y z) (* t a))) (* b (- (* z c) (* a i))))
(* j (- (* t c) (* y i))))
7.765624636983288e+305)
(+
(- (* x (- (* y z) (* t a))) (* b (- (* z c) (* a i))))
(* j (- (* t c) (* y i))))
(- (* j (- (* t c) (* y i))) (* b (- (* z c) (* a i))))))double code(double x, double y, double z, double t, double a, double b, double c, double i, double j) {
return ((x * ((y * z) - (t * a))) - (b * ((c * z) - (i * a)))) + (j * ((c * t) - (i * y)));
}
double code(double x, double y, double z, double t, double a, double b, double c, double i, double j) {
double tmp;
if ((((x * ((y * z) - (t * a))) - (b * ((z * c) - (a * i)))) + (j * ((t * c) - (y * i)))) <= 7.765624636983288e+305) {
tmp = ((x * ((y * z) - (t * a))) - (b * ((z * c) - (a * i)))) + (j * ((t * c) - (y * i)));
} else {
tmp = (j * ((t * c) - (y * i))) - (b * ((z * c) - (a * i)));
}
return tmp;
}




Bits error versus x




Bits error versus y




Bits error versus z




Bits error versus t




Bits error versus a




Bits error versus b




Bits error versus c




Bits error versus i




Bits error versus j
Results
| Original | 12.4 |
|---|---|
| Target | 15.9 |
| Herbie | 11.8 |
if (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 i a)))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y)))) < 7.76562463698328849e305Initial program 6.9
if 7.76562463698328849e305 < (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 i a)))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y)))) Initial program 61.7
Taylor expanded around 0 56.1
Final simplification11.8
herbie shell --seed 2020346
(FPCore (x y z t a b c i j)
:name "Linear.Matrix:det33 from linear-1.19.1.3"
:precision binary64
:herbie-target
(if (< t -8.120978919195912e-33) (- (* x (- (* z y) (* a t))) (- (* b (- (* z c) (* a i))) (* (- (* c t) (* y i)) j))) (if (< t -4.712553818218485e-169) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (/ (* j (- (pow (* c t) 2.0) (pow (* i y) 2.0))) (+ (* c t) (* i y)))) (if (< t -7.633533346031584e-308) (- (* x (- (* z y) (* a t))) (- (* b (- (* z c) (* a i))) (* (- (* c t) (* y i)) j))) (if (< t 1.0535888557455487e-139) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (/ (* j (- (pow (* c t) 2.0) (pow (* i y) 2.0))) (+ (* c t) (* i y)))) (- (* x (- (* z y) (* a t))) (- (* b (- (* z c) (* a i))) (* (- (* c t) (* y i)) j)))))))
(+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (* j (- (* c t) (* i y)))))