\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}
\mathbf{if}\;y3 \le -3.76857872627632948 \cdot 10^{-10}:\\
\;\;\;\;\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(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-y1 \cdot a\right)\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(y0 \cdot \left(y3 \cdot \left(j \cdot y5\right)\right) - \left(y0 \cdot \left(y2 \cdot \left(k \cdot y5\right)\right) + y1 \cdot \left(y3 \cdot \left(j \cdot y4\right)\right)\right)\right)\\
\mathbf{elif}\;y3 \le 6.4349932201675677 \cdot 10^{-284}:\\
\;\;\;\;\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(a \cdot \left(y3 \cdot \left(y1 \cdot z\right)\right) - \left(y0 \cdot \left(z \cdot \left(y3 \cdot c\right)\right) + a \cdot \left(x \cdot \left(y2 \cdot y1\right)\right)\right)\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)\\
\mathbf{elif}\;y3 \le 1.4622191323114389 \cdot 10^{-28}:\\
\;\;\;\;\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(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-y1 \cdot a\right)\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(y0 \cdot \left(y3 \cdot \left(j \cdot y5\right)\right) - \left(y0 \cdot \left(y2 \cdot \left(k \cdot y5\right)\right) + y1 \cdot \left(y3 \cdot \left(j \cdot y4\right)\right)\right)\right)\\
\mathbf{elif}\;y3 \le 6.90918167605642245 \cdot 10^{47}:\\
\;\;\;\;\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(a \cdot \left(y3 \cdot \left(y1 \cdot z\right)\right) - \left(y0 \cdot \left(z \cdot \left(y3 \cdot c\right)\right) + a \cdot \left(x \cdot \left(y2 \cdot y1\right)\right)\right)\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)\\
\mathbf{elif}\;y3 \le 1.08865228153120512 \cdot 10^{178}:\\
\;\;\;\;\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(a \cdot \left(y3 \cdot \left(y \cdot y5\right)\right) - \left(y \cdot \left(y3 \cdot \left(y4 \cdot c\right)\right) + y5 \cdot \left(a \cdot \left(y2 \cdot t\right)\right)\right)\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\\
\mathbf{else}:\\
\;\;\;\;\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(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-y1 \cdot a\right)\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(y0 \cdot \left(y3 \cdot \left(j \cdot y5\right)\right) - \left(y0 \cdot \left(y2 \cdot \left(k \cdot y5\right)\right) + y1 \cdot \left(y3 \cdot \left(j \cdot y4\right)\right)\right)\right)\\
\end{array}double f(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 r791832 = x;
double r791833 = y;
double r791834 = r791832 * r791833;
double r791835 = z;
double r791836 = t;
double r791837 = r791835 * r791836;
double r791838 = r791834 - r791837;
double r791839 = a;
double r791840 = b;
double r791841 = r791839 * r791840;
double r791842 = c;
double r791843 = i;
double r791844 = r791842 * r791843;
double r791845 = r791841 - r791844;
double r791846 = r791838 * r791845;
double r791847 = j;
double r791848 = r791832 * r791847;
double r791849 = k;
double r791850 = r791835 * r791849;
double r791851 = r791848 - r791850;
double r791852 = y0;
double r791853 = r791852 * r791840;
double r791854 = y1;
double r791855 = r791854 * r791843;
double r791856 = r791853 - r791855;
double r791857 = r791851 * r791856;
double r791858 = r791846 - r791857;
double r791859 = y2;
double r791860 = r791832 * r791859;
double r791861 = y3;
double r791862 = r791835 * r791861;
double r791863 = r791860 - r791862;
double r791864 = r791852 * r791842;
double r791865 = r791854 * r791839;
double r791866 = r791864 - r791865;
double r791867 = r791863 * r791866;
double r791868 = r791858 + r791867;
double r791869 = r791836 * r791847;
double r791870 = r791833 * r791849;
double r791871 = r791869 - r791870;
double r791872 = y4;
double r791873 = r791872 * r791840;
double r791874 = y5;
double r791875 = r791874 * r791843;
double r791876 = r791873 - r791875;
double r791877 = r791871 * r791876;
double r791878 = r791868 + r791877;
double r791879 = r791836 * r791859;
double r791880 = r791833 * r791861;
double r791881 = r791879 - r791880;
double r791882 = r791872 * r791842;
double r791883 = r791874 * r791839;
double r791884 = r791882 - r791883;
double r791885 = r791881 * r791884;
double r791886 = r791878 - r791885;
double r791887 = r791849 * r791859;
double r791888 = r791847 * r791861;
double r791889 = r791887 - r791888;
double r791890 = r791872 * r791854;
double r791891 = r791874 * r791852;
double r791892 = r791890 - r791891;
double r791893 = r791889 * r791892;
double r791894 = r791886 + r791893;
return r791894;
}
double f(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 r791895 = y3;
double r791896 = -3.7685787262763295e-10;
bool r791897 = r791895 <= r791896;
double r791898 = x;
double r791899 = y;
double r791900 = r791898 * r791899;
double r791901 = z;
double r791902 = t;
double r791903 = r791901 * r791902;
double r791904 = r791900 - r791903;
double r791905 = a;
double r791906 = b;
double r791907 = r791905 * r791906;
double r791908 = c;
double r791909 = i;
double r791910 = r791908 * r791909;
double r791911 = r791907 - r791910;
double r791912 = r791904 * r791911;
double r791913 = j;
double r791914 = r791898 * r791913;
double r791915 = k;
double r791916 = r791901 * r791915;
double r791917 = r791914 - r791916;
double r791918 = y0;
double r791919 = r791918 * r791906;
double r791920 = y1;
double r791921 = r791920 * r791909;
double r791922 = r791919 - r791921;
double r791923 = r791917 * r791922;
double r791924 = r791912 - r791923;
double r791925 = y2;
double r791926 = r791898 * r791925;
double r791927 = r791901 * r791895;
double r791928 = r791926 - r791927;
double r791929 = r791918 * r791908;
double r791930 = r791928 * r791929;
double r791931 = r791920 * r791905;
double r791932 = -r791931;
double r791933 = r791928 * r791932;
double r791934 = r791930 + r791933;
double r791935 = r791924 + r791934;
double r791936 = r791902 * r791913;
double r791937 = r791899 * r791915;
double r791938 = r791936 - r791937;
double r791939 = y4;
double r791940 = r791939 * r791906;
double r791941 = y5;
double r791942 = r791941 * r791909;
double r791943 = r791940 - r791942;
double r791944 = r791938 * r791943;
double r791945 = r791935 + r791944;
double r791946 = r791902 * r791925;
double r791947 = r791899 * r791895;
double r791948 = r791946 - r791947;
double r791949 = r791939 * r791908;
double r791950 = r791941 * r791905;
double r791951 = r791949 - r791950;
double r791952 = r791948 * r791951;
double r791953 = r791945 - r791952;
double r791954 = r791913 * r791941;
double r791955 = r791895 * r791954;
double r791956 = r791918 * r791955;
double r791957 = r791915 * r791941;
double r791958 = r791925 * r791957;
double r791959 = r791918 * r791958;
double r791960 = r791913 * r791939;
double r791961 = r791895 * r791960;
double r791962 = r791920 * r791961;
double r791963 = r791959 + r791962;
double r791964 = r791956 - r791963;
double r791965 = r791953 + r791964;
double r791966 = 6.434993220167568e-284;
bool r791967 = r791895 <= r791966;
double r791968 = r791920 * r791901;
double r791969 = r791895 * r791968;
double r791970 = r791905 * r791969;
double r791971 = r791895 * r791908;
double r791972 = r791901 * r791971;
double r791973 = r791918 * r791972;
double r791974 = r791925 * r791920;
double r791975 = r791898 * r791974;
double r791976 = r791905 * r791975;
double r791977 = r791973 + r791976;
double r791978 = r791970 - r791977;
double r791979 = r791924 + r791978;
double r791980 = r791979 + r791944;
double r791981 = r791980 - r791952;
double r791982 = r791915 * r791925;
double r791983 = r791913 * r791895;
double r791984 = r791982 - r791983;
double r791985 = r791939 * r791920;
double r791986 = r791941 * r791918;
double r791987 = r791985 - r791986;
double r791988 = r791984 * r791987;
double r791989 = r791981 + r791988;
double r791990 = 1.462219132311439e-28;
bool r791991 = r791895 <= r791990;
double r791992 = 6.9091816760564224e+47;
bool r791993 = r791895 <= r791992;
double r791994 = 1.0886522815312051e+178;
bool r791995 = r791895 <= r791994;
double r791996 = r791929 - r791931;
double r791997 = r791928 * r791996;
double r791998 = r791924 + r791997;
double r791999 = r791998 + r791944;
double r792000 = r791899 * r791941;
double r792001 = r791895 * r792000;
double r792002 = r791905 * r792001;
double r792003 = r791895 * r791949;
double r792004 = r791899 * r792003;
double r792005 = r791925 * r791902;
double r792006 = r791905 * r792005;
double r792007 = r791941 * r792006;
double r792008 = r792004 + r792007;
double r792009 = r792002 - r792008;
double r792010 = r791999 - r792009;
double r792011 = r792010 + r791988;
double r792012 = r791995 ? r792011 : r791965;
double r792013 = r791993 ? r791989 : r792012;
double r792014 = r791991 ? r791965 : r792013;
double r792015 = r791967 ? r791989 : r792014;
double r792016 = r791897 ? r791965 : r792015;
return r792016;
}




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.5 |
|---|---|
| Target | 30.8 |
| Herbie | 29.8 |
if y3 < -3.7685787262763295e-10 or 6.434993220167568e-284 < y3 < 1.462219132311439e-28 or 1.0886522815312051e+178 < y3 Initial program 28.7
rmApplied sub-neg28.7
Applied distribute-lft-in28.7
Taylor expanded around inf 31.0
if -3.7685787262763295e-10 < y3 < 6.434993220167568e-284 or 1.462219132311439e-28 < y3 < 6.9091816760564224e+47Initial program 26.4
Taylor expanded around inf 28.6
if 6.9091816760564224e+47 < y3 < 1.0886522815312051e+178Initial program 26.3
Taylor expanded around inf 28.5
Final simplification29.8
herbie shell --seed 2020025
(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 (- (* 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)))))