\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)
\begin{array}{l}
t_1 := x \cdot j - z \cdot k\\
t_2 := k \cdot y2 - j \cdot y3\\
t_3 := c \cdot y4 - a \cdot y5\\
t_4 := x \cdot y2 - z \cdot y3\\
t_5 := t_4 \cdot \left(c \cdot y0 - a \cdot y1\right)\\
t_6 := x \cdot y - z \cdot t\\
t_7 := t_6 \cdot \left(b \cdot a - c \cdot i\right)\\
t_8 := \left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right)\\
t_9 := y1 \cdot y4 - y0 \cdot y5\\
t_10 := t_2 \cdot t_9\\
t_11 := t_1 \cdot \left(b \cdot y0 - i \cdot y1\right)\\
t_12 := \left(\left(t_7 - t_11\right) + t_5\right) + t_8\\
t_13 := \left(t_12 - t \cdot \left(y2 \cdot t_3\right)\right) + t_10\\
\mathbf{if}\;b \leq -2.909509653808407 \cdot 10^{+31}:\\
\;\;\;\;t_13\\
\mathbf{else}:\\
\;\;\;\;\begin{array}{l}
t_14 := \left(a \cdot \left(y \cdot \left(y3 \cdot y5\right)\right) + c \cdot \left(y4 \cdot \left(t \cdot y2\right)\right)\right) - \left(a \cdot \left(t \cdot \left(y2 \cdot y5\right)\right) + c \cdot \left(y4 \cdot \left(y \cdot y3\right)\right)\right)\\
\mathbf{if}\;b \leq -2.806277006557273 \cdot 10^{-68}:\\
\;\;\;\;\left(t_12 - t_14\right) + \left(y4 \cdot \left(y1 \cdot t_2\right) - y0 \cdot \left(y5 \cdot t_2\right)\right)\\
\mathbf{else}:\\
\;\;\;\;\begin{array}{l}
t_15 := t_3 \cdot \left(t \cdot y2 - y \cdot y3\right)\\
\mathbf{if}\;b \leq -1.0040207346650277 \cdot 10^{-209}:\\
\;\;\;\;t_10 + \left(\left(t_8 + \left(t_5 + \left(t_7 - \left(\left(y0 \cdot \left(j \cdot \left(b \cdot x\right)\right) + k \cdot \left(y1 \cdot \left(z \cdot i\right)\right)\right) - \left(y1 \cdot \left(i \cdot \left(x \cdot j\right)\right) + k \cdot \left(y0 \cdot \left(b \cdot z\right)\right)\right)\right)\right)\right)\right) - t_15\right)\\
\mathbf{else}:\\
\;\;\;\;\begin{array}{l}
t_16 := t_5 + \left(\left(a \cdot \left(b \cdot t_6\right) - c \cdot \left(t_6 \cdot i\right)\right) - t_11\right)\\
t_17 := \left(a \cdot \left(b \cdot t_6\right) - c \cdot \left(t_6 \cdot i\right)\right) - t_11\\
\mathbf{if}\;b \leq 1.0685914763402614 \cdot 10^{-285}:\\
\;\;\;\;t_10 + \left(\left(t_16 + \left(\left(y4 \cdot \left(t \cdot \left(b \cdot j\right)\right) + k \cdot \left(i \cdot \left(y \cdot y5\right)\right)\right) - \left(i \cdot \left(t \cdot \left(j \cdot y5\right)\right) + k \cdot \left(y4 \cdot \left(b \cdot y\right)\right)\right)\right)\right) - t_14\right)\\
\mathbf{elif}\;b \leq 1.4583693835051775 \cdot 10^{-227}:\\
\;\;\;\;t_10 + \left(\left(t_8 + \left(t_17 - a \cdot \left(y1 \cdot t_4\right)\right)\right) - t_14\right)\\
\mathbf{elif}\;b \leq 7.2281729213613215 \cdot 10^{-118}:\\
\;\;\;\;\left(t_12 - t_15\right) + \left(\left(y0 \cdot \left(y3 \cdot \left(j \cdot y5\right)\right) + k \cdot \left(y4 \cdot \left(y1 \cdot y2\right)\right)\right) - \left(k \cdot \left(y0 \cdot \left(y2 \cdot y5\right)\right) + y4 \cdot \left(y1 \cdot \left(j \cdot y3\right)\right)\right)\right)\\
\mathbf{elif}\;b \leq 4.337347052576901 \cdot 10^{+61}:\\
\;\;\;\;t_10 + \left(\left(t_8 + \left(t_17 + \left(c \cdot \left(y0 \cdot t_4\right) - y1 \cdot \left(a \cdot t_4\right)\right)\right)\right) - t_14\right)\\
\mathbf{elif}\;b \leq 7.254232084859899 \cdot 10^{+167}:\\
\;\;\;\;t_13\\
\mathbf{elif}\;b \leq 3.710958107572736 \cdot 10^{+214}:\\
\;\;\;\;t_10 + \left(\left(t_8 + \left(t_5 + \left(t_7 - y0 \cdot \left(b \cdot t_1\right)\right)\right)\right) - t_14\right)\\
\mathbf{else}:\\
\;\;\;\;\left(\left(t_8 + t_16\right) - t_14\right) + k \cdot \left(y2 \cdot t_9\right)\\
\end{array}\\
\end{array}\\
\end{array}\\
\end{array}
(FPCore (x y z t a b c i j k y0 y1 y2 y3 y4 y5)
:precision binary64
(+
(-
(+
(+
(-
(* (- (* x y) (* z t)) (- (* a b) (* c i)))
(* (- (* x j) (* z k)) (- (* y0 b) (* y1 i))))
(* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a))))
(* (- (* t j) (* y k)) (- (* y4 b) (* y5 i))))
(* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a))))
(* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))))(FPCore (x y z t a b c i j k y0 y1 y2 y3 y4 y5)
:precision binary64
(let* ((t_1 (- (* x j) (* z k)))
(t_2 (- (* k y2) (* j y3)))
(t_3 (- (* c y4) (* a y5)))
(t_4 (- (* x y2) (* z y3)))
(t_5 (* t_4 (- (* c y0) (* a y1))))
(t_6 (- (* x y) (* z t)))
(t_7 (* t_6 (- (* b a) (* c i))))
(t_8 (* (- (* t j) (* y k)) (- (* b y4) (* i y5))))
(t_9 (- (* y1 y4) (* y0 y5)))
(t_10 (* t_2 t_9))
(t_11 (* t_1 (- (* b y0) (* i y1))))
(t_12 (+ (+ (- t_7 t_11) t_5) t_8))
(t_13 (+ (- t_12 (* t (* y2 t_3))) t_10)))
(if (<= b -2.909509653808407e+31)
t_13
(let* ((t_14
(-
(+ (* a (* y (* y3 y5))) (* c (* y4 (* t y2))))
(+ (* a (* t (* y2 y5))) (* c (* y4 (* y y3)))))))
(if (<= b -2.806277006557273e-68)
(+ (- t_12 t_14) (- (* y4 (* y1 t_2)) (* y0 (* y5 t_2))))
(let* ((t_15 (* t_3 (- (* t y2) (* y y3)))))
(if (<= b -1.0040207346650277e-209)
(+
t_10
(-
(+
t_8
(+
t_5
(-
t_7
(-
(+ (* y0 (* j (* b x))) (* k (* y1 (* z i))))
(+ (* y1 (* i (* x j))) (* k (* y0 (* b z))))))))
t_15))
(let* ((t_16 (+ t_5 (- (- (* a (* b t_6)) (* c (* t_6 i))) t_11)))
(t_17 (- (- (* a (* b t_6)) (* c (* t_6 i))) t_11)))
(if (<= b 1.0685914763402614e-285)
(+
t_10
(-
(+
t_16
(-
(+ (* y4 (* t (* b j))) (* k (* i (* y y5))))
(+ (* i (* t (* j y5))) (* k (* y4 (* b y))))))
t_14))
(if (<= b 1.4583693835051775e-227)
(+ t_10 (- (+ t_8 (- t_17 (* a (* y1 t_4)))) t_14))
(if (<= b 7.2281729213613215e-118)
(+
(- t_12 t_15)
(-
(+ (* y0 (* y3 (* j y5))) (* k (* y4 (* y1 y2))))
(+ (* k (* y0 (* y2 y5))) (* y4 (* y1 (* j y3))))))
(if (<= b 4.337347052576901e+61)
(+
t_10
(-
(+ t_8 (+ t_17 (- (* c (* y0 t_4)) (* y1 (* a t_4)))))
t_14))
(if (<= b 7.254232084859899e+167)
t_13
(if (<= b 3.710958107572736e+214)
(+
t_10
(- (+ t_8 (+ t_5 (- t_7 (* y0 (* b t_1))))) t_14))
(+
(- (+ t_8 t_16) t_14)
(* k (* y2 t_9)))))))))))))))))double code(double x, double y, double z, double t, double a, double b, double c, double i, double j, double k, double y0, double y1, double y2, double y3, double y4, double y5) {
return (((((((x * y) - (z * t)) * ((a * b) - (c * i))) - (((x * j) - (z * k)) * ((y0 * b) - (y1 * i)))) + (((x * y2) - (z * y3)) * ((y0 * c) - (y1 * a)))) + (((t * j) - (y * k)) * ((y4 * b) - (y5 * i)))) - (((t * y2) - (y * y3)) * ((y4 * c) - (y5 * a)))) + (((k * y2) - (j * y3)) * ((y4 * y1) - (y5 * y0)));
}
double code(double x, double y, double z, double t, double a, double b, double c, double i, double j, double k, double y0, double y1, double y2, double y3, double y4, double y5) {
double t_1 = (x * j) - (z * k);
double t_2 = (k * y2) - (j * y3);
double t_3 = (c * y4) - (a * y5);
double t_4 = (x * y2) - (z * y3);
double t_5 = t_4 * ((c * y0) - (a * y1));
double t_6 = (x * y) - (z * t);
double t_7 = t_6 * ((b * a) - (c * i));
double t_8 = ((t * j) - (y * k)) * ((b * y4) - (i * y5));
double t_9 = (y1 * y4) - (y0 * y5);
double t_10 = t_2 * t_9;
double t_11 = t_1 * ((b * y0) - (i * y1));
double t_12 = ((t_7 - t_11) + t_5) + t_8;
double t_13 = (t_12 - (t * (y2 * t_3))) + t_10;
double tmp;
if (b <= -2.909509653808407e+31) {
tmp = t_13;
} else {
double t_14 = ((a * (y * (y3 * y5))) + (c * (y4 * (t * y2)))) - ((a * (t * (y2 * y5))) + (c * (y4 * (y * y3))));
double tmp_1;
if (b <= -2.806277006557273e-68) {
tmp_1 = (t_12 - t_14) + ((y4 * (y1 * t_2)) - (y0 * (y5 * t_2)));
} else {
double t_15 = t_3 * ((t * y2) - (y * y3));
double tmp_2;
if (b <= -1.0040207346650277e-209) {
tmp_2 = t_10 + ((t_8 + (t_5 + (t_7 - (((y0 * (j * (b * x))) + (k * (y1 * (z * i)))) - ((y1 * (i * (x * j))) + (k * (y0 * (b * z)))))))) - t_15);
} else {
double t_16 = t_5 + (((a * (b * t_6)) - (c * (t_6 * i))) - t_11);
double t_17 = ((a * (b * t_6)) - (c * (t_6 * i))) - t_11;
double tmp_3;
if (b <= 1.0685914763402614e-285) {
tmp_3 = t_10 + ((t_16 + (((y4 * (t * (b * j))) + (k * (i * (y * y5)))) - ((i * (t * (j * y5))) + (k * (y4 * (b * y)))))) - t_14);
} else if (b <= 1.4583693835051775e-227) {
tmp_3 = t_10 + ((t_8 + (t_17 - (a * (y1 * t_4)))) - t_14);
} else if (b <= 7.2281729213613215e-118) {
tmp_3 = (t_12 - t_15) + (((y0 * (y3 * (j * y5))) + (k * (y4 * (y1 * y2)))) - ((k * (y0 * (y2 * y5))) + (y4 * (y1 * (j * y3)))));
} else if (b <= 4.337347052576901e+61) {
tmp_3 = t_10 + ((t_8 + (t_17 + ((c * (y0 * t_4)) - (y1 * (a * t_4))))) - t_14);
} else if (b <= 7.254232084859899e+167) {
tmp_3 = t_13;
} else if (b <= 3.710958107572736e+214) {
tmp_3 = t_10 + ((t_8 + (t_5 + (t_7 - (y0 * (b * t_1))))) - t_14);
} else {
tmp_3 = ((t_8 + t_16) - t_14) + (k * (y2 * t_9));
}
tmp_2 = tmp_3;
}
tmp_1 = tmp_2;
}
tmp = tmp_1;
}
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
Bits error versus k
Bits error versus y0
Bits error versus y1
Bits error versus y2
Bits error versus y3
Bits error versus y4
Bits error versus y5
Results
| Original | 27.0 |
|---|---|
| Target | 30.9 |
| Herbie | 28.6 |
if b < -2.9095096538084068e31 or 4.33734705257690116e61 < b < 7.25423208485989863e167Initial program 28.0
Taylor expanded in t around inf 29.8
if -2.9095096538084068e31 < b < -2.80627700655727312e-68Initial program 23.3
Taylor expanded in t around inf 24.7
Applied sub-neg_binary6424.7
Applied distribute-rgt-in_binary6424.7
Simplified24.5
Simplified23.7
if -2.80627700655727312e-68 < b < -1.00402073466502775e-209Initial program 27.4
Taylor expanded in x around inf 28.4
if -1.00402073466502775e-209 < b < 1.06859147634026138e-285Initial program 28.4
Taylor expanded in t around inf 29.6
Applied sub-neg_binary6429.6
Applied distribute-rgt-in_binary6429.6
Simplified29.6
Simplified30.6
Taylor expanded in t around 0 30.3
if 1.06859147634026138e-285 < b < 1.4583693835051775e-227Initial program 26.4
Taylor expanded in t around inf 29.3
Applied sub-neg_binary6429.3
Applied distribute-rgt-in_binary6429.3
Simplified29.4
Simplified29.9
Taylor expanded in a around inf 33.2
if 1.4583693835051775e-227 < b < 7.2281729213613215e-118Initial program 27.7
Taylor expanded in k around 0 27.9
if 7.2281729213613215e-118 < b < 4.33734705257690116e61Initial program 24.3
Taylor expanded in t around inf 25.6
Applied sub-neg_binary6425.6
Applied distribute-rgt-in_binary6425.6
Simplified25.6
Simplified26.0
Applied sub-neg_binary6426.0
Applied distribute-rgt-in_binary6426.0
Simplified25.6
Simplified25.5
if 7.25423208485989863e167 < b < 3.71095810757273607e214Initial program 25.3
Taylor expanded in t around inf 26.4
Taylor expanded in y0 around inf 29.2
if 3.71095810757273607e214 < b Initial program 35.3
Taylor expanded in t around inf 37.7
Applied sub-neg_binary6437.7
Applied distribute-rgt-in_binary6437.7
Simplified38.1
Simplified36.8
Taylor expanded in y2 around inf 36.8
Final simplification28.6
herbie shell --seed 2021280
(FPCore (x y z t a b c i j k y0 y1 y2 y3 y4 y5)
:name "Linear.Matrix:det44 from linear-1.19.1.3"
:precision binary64
:herbie-target
(if (< y4 -7.206256231996481e+60) (- (- (* (- (* b a) (* i c)) (- (* y x) (* t z))) (- (* (- (* j x) (* k z)) (- (* y0 b) (* i y1))) (* (- (* j t) (* k y)) (- (* y4 b) (* y5 i))))) (- (/ (- (* y2 t) (* y3 y)) (/ 1.0 (- (* y4 c) (* y5 a)))) (* (- (* y2 k) (* y3 j)) (- (* y4 y1) (* y5 y0))))) (if (< y4 -3.364603505246317e-66) (+ (- (- (- (* (* t c) (* i z)) (* (* a t) (* b z))) (* (* y c) (* i x))) (* (- (* b y0) (* i y1)) (- (* j x) (* k z)))) (- (* (- (* y0 c) (* a y1)) (- (* x y2) (* z y3))) (- (* (- (* t y2) (* y y3)) (- (* y4 c) (* a y5))) (* (- (* y1 y4) (* y5 y0)) (- (* k y2) (* j y3)))))) (if (< y4 -1.2000065055686116e-105) (+ (+ (- (* (- (* j t) (* k y)) (- (* y4 b) (* y5 i))) (* (* y3 y) (- (* y5 a) (* y4 c)))) (+ (* (* y5 a) (* t y2)) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0))))) (- (* (- (* x y2) (* z y3)) (- (* c y0) (* a y1))) (- (* (- (* b y0) (* i y1)) (- (* j x) (* k z))) (* (- (* y x) (* z t)) (- (* b a) (* i c)))))) (if (< y4 6.718963124057495e-279) (+ (- (- (- (* (* k y) (* y5 i)) (* (* y b) (* y4 k))) (* (* y5 t) (* i j))) (- (* (- (* y2 t) (* y3 y)) (- (* y4 c) (* y5 a))) (* (- (* y2 k) (* y3 j)) (- (* y4 y1) (* y5 y0))))) (- (* (- (* b a) (* i c)) (- (* y x) (* t z))) (- (* (- (* j x) (* k z)) (- (* y0 b) (* i y1))) (* (- (* y2 x) (* y3 z)) (- (* c y0) (* y1 a)))))) (if (< y4 4.77962681403792e-222) (+ (+ (- (* (- (* j t) (* k y)) (- (* y4 b) (* y5 i))) (* (* y3 y) (- (* y5 a) (* y4 c)))) (+ (* (* y5 a) (* t y2)) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0))))) (- (* (- (* x y2) (* z y3)) (- (* c y0) (* a y1))) (- (* (- (* b y0) (* i y1)) (- (* j x) (* k z))) (* (- (* y x) (* z t)) (- (* b a) (* i c)))))) (if (< y4 2.2852241541266835e-175) (+ (- (- (- (* (* k y) (* y5 i)) (* (* y b) (* y4 k))) (* (* y5 t) (* i j))) (- (* (- (* y2 t) (* y3 y)) (- (* y4 c) (* y5 a))) (* (- (* y2 k) (* y3 j)) (- (* y4 y1) (* y5 y0))))) (- (* (- (* b a) (* i c)) (- (* y x) (* t z))) (- (* (- (* j x) (* k z)) (- (* y0 b) (* i y1))) (* (- (* y2 x) (* y3 z)) (- (* c y0) (* y1 a)))))) (+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (- (* k (* i (* z y1))) (+ (* j (* i (* x y1))) (* y0 (* k (* z b)))))) (- (* z (* y3 (* a y1))) (+ (* y2 (* x (* a y1))) (* y0 (* z (* c y3)))))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0))))))))))
(+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))))