Linear.Matrix:det33 from linear-1.19.1.3

Average Error: 12.5 → 9.7

Time: 27.9s

Precision: 64

Math

\[\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}\;j \le -2.961055619344420626519795079213745347097 \cdot 10^{-21}:\\ \;\;\;\;\left(\left(y \cdot \left(z \cdot x\right) + t \cdot \left(\left(-a\right) \cdot x\right)\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\ \mathbf{elif}\;j \le 64272744.59900391101837158203125:\\ \;\;\;\;\left(\left(\left(y \cdot z\right) \cdot x + \left(-t \cdot a\right) \cdot x\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + \left(t \cdot \left(j \cdot c\right) - i \cdot \left(j \cdot y\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(y \cdot \left(z \cdot x\right) + \left(-t \cdot a\right) \cdot x\right) - \left(z \cdot \left(b \cdot c\right) + \left(-i \cdot a\right) \cdot b\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b, double c, double i, double j) {
        double r379036 = x;
        double r379037 = y;
        double r379038 = z;
        double r379039 = r379037 * r379038;
        double r379040 = t;
        double r379041 = a;
        double r379042 = r379040 * r379041;
        double r379043 = r379039 - r379042;
        double r379044 = r379036 * r379043;
        double r379045 = b;
        double r379046 = c;
        double r379047 = r379046 * r379038;
        double r379048 = i;
        double r379049 = r379048 * r379041;
        double r379050 = r379047 - r379049;
        double r379051 = r379045 * r379050;
        double r379052 = r379044 - r379051;
        double r379053 = j;
        double r379054 = r379046 * r379040;
        double r379055 = r379048 * r379037;
        double r379056 = r379054 - r379055;
        double r379057 = r379053 * r379056;
        double r379058 = r379052 + r379057;
        return r379058;
}

↓

double f(double x, double y, double z, double t, double a, double b, double c, double i, double j) {
        double r379059 = j;
        double r379060 = -2.9610556193444206e-21;
        bool r379061 = r379059 <= r379060;
        double r379062 = y;
        double r379063 = z;
        double r379064 = x;
        double r379065 = r379063 * r379064;
        double r379066 = r379062 * r379065;
        double r379067 = t;
        double r379068 = a;
        double r379069 = -r379068;
        double r379070 = r379069 * r379064;
        double r379071 = r379067 * r379070;
        double r379072 = r379066 + r379071;
        double r379073 = b;
        double r379074 = c;
        double r379075 = r379074 * r379063;
        double r379076 = i;
        double r379077 = r379076 * r379068;
        double r379078 = r379075 - r379077;
        double r379079 = r379073 * r379078;
        double r379080 = r379072 - r379079;
        double r379081 = r379074 * r379067;
        double r379082 = r379076 * r379062;
        double r379083 = r379081 - r379082;
        double r379084 = r379059 * r379083;
        double r379085 = r379080 + r379084;
        double r379086 = 64272744.59900391;
        bool r379087 = r379059 <= r379086;
        double r379088 = r379062 * r379063;
        double r379089 = r379088 * r379064;
        double r379090 = r379067 * r379068;
        double r379091 = -r379090;
        double r379092 = r379091 * r379064;
        double r379093 = r379089 + r379092;
        double r379094 = r379093 - r379079;
        double r379095 = r379059 * r379074;
        double r379096 = r379067 * r379095;
        double r379097 = r379059 * r379062;
        double r379098 = r379076 * r379097;
        double r379099 = r379096 - r379098;
        double r379100 = r379094 + r379099;
        double r379101 = r379066 + r379092;
        double r379102 = r379073 * r379074;
        double r379103 = r379063 * r379102;
        double r379104 = -r379077;
        double r379105 = r379104 * r379073;
        double r379106 = r379103 + r379105;
        double r379107 = r379101 - r379106;
        double r379108 = r379107 + r379084;
        double r379109 = r379087 ? r379100 : r379108;
        double r379110 = r379061 ? r379085 : r379109;
        return r379110;
}

Error

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

Target

Original	12.5
Target	16.1
Herbie	9.7

\[\begin{array}{l} \mathbf{if}\;t \lt -8.12097891919591218149793027759825150959 \cdot 10^{-33}:\\ \;\;\;\;x \cdot \left(z \cdot y - a \cdot t\right) - \left(b \cdot \left(z \cdot c - a \cdot i\right) - \left(c \cdot t - y \cdot i\right) \cdot j\right)\\ \mathbf{elif}\;t \lt -4.712553818218485141757938537793350881052 \cdot 10^{-169}:\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + \frac{j \cdot \left({\left(c \cdot t\right)}^{2} - {\left(i \cdot y\right)}^{2}\right)}{c \cdot t + i \cdot y}\\ \mathbf{elif}\;t \lt -7.633533346031583686060259351057142920433 \cdot 10^{-308}:\\ \;\;\;\;x \cdot \left(z \cdot y - a \cdot t\right) - \left(b \cdot \left(z \cdot c - a \cdot i\right) - \left(c \cdot t - y \cdot i\right) \cdot j\right)\\ \mathbf{elif}\;t \lt 1.053588855745548710002760210539645467715 \cdot 10^{-139}:\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + \frac{j \cdot \left({\left(c \cdot t\right)}^{2} - {\left(i \cdot y\right)}^{2}\right)}{c \cdot t + i \cdot y}\\ \mathbf{else}:\\ \;\;\;\;x \cdot \left(z \cdot y - a \cdot t\right) - \left(b \cdot \left(z \cdot c - a \cdot i\right) - \left(c \cdot t - y \cdot i\right) \cdot j\right)\\ \end{array}\]

Derivation

1. Split input into 3 regimes

2. if j < -2.9610556193444206e-21

   1. Initial program 7.3

      \[\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)\]
   2. Using strategy rm

   3. Applied sub-neg 7.3

      \[\leadsto \left(x \cdot \color{blue}{\left(y \cdot z + \left(-t \cdot a\right)\right)} - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   4. Applied distribute-lft-in 7.3

      \[\leadsto \left(\color{blue}{\left(x \cdot \left(y \cdot z\right) + x \cdot \left(-t \cdot a\right)\right)} - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   5. Simplified 7.3

      \[\leadsto \left(\left(\color{blue}{\left(y \cdot z\right) \cdot x} + x \cdot \left(-t \cdot a\right)\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   6. Simplified 7.3

      \[\leadsto \left(\left(\left(y \cdot z\right) \cdot x + \color{blue}{\left(-t \cdot a\right) \cdot x}\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
   7. Using strategy rm

   8. Applied associate-*l* 7.9

      \[\leadsto \left(\left(\color{blue}{y \cdot \left(z \cdot x\right)} + \left(-t \cdot a\right) \cdot x\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
   9. Using strategy rm

   10. Applied *-un-lft-identity 7.9

       \[\leadsto \left(\left(y \cdot \left(z \cdot x\right) + \color{blue}{\left(1 \cdot \left(-t \cdot a\right)\right)} \cdot x\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   11. Applied associate-*l* 7.9

       \[\leadsto \left(\left(y \cdot \left(z \cdot x\right) + \color{blue}{1 \cdot \left(\left(-t \cdot a\right) \cdot x\right)}\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   12. Simplified 8.8

       \[\leadsto \left(\left(y \cdot \left(z \cdot x\right) + 1 \cdot \color{blue}{\left(t \cdot \left(\left(-a\right) \cdot x\right)\right)}\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   if -2.9610556193444206e-21 < j < 64272744.59900391

   1. Initial program 15.8

      \[\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)\]
   2. Using strategy rm

   3. Applied sub-neg 15.8

      \[\leadsto \left(x \cdot \color{blue}{\left(y \cdot z + \left(-t \cdot a\right)\right)} - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   4. Applied distribute-lft-in 15.8

      \[\leadsto \left(\color{blue}{\left(x \cdot \left(y \cdot z\right) + x \cdot \left(-t \cdot a\right)\right)} - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   5. Simplified 15.8

      \[\leadsto \left(\left(\color{blue}{\left(y \cdot z\right) \cdot x} + x \cdot \left(-t \cdot a\right)\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   6. Simplified 15.8

      \[\leadsto \left(\left(\left(y \cdot z\right) \cdot x + \color{blue}{\left(-t \cdot a\right) \cdot x}\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   7. Taylor expanded around inf 10.3

      \[\leadsto \left(\left(\left(y \cdot z\right) \cdot x + \left(-t \cdot a\right) \cdot x\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + \color{blue}{\left(t \cdot \left(j \cdot c\right) - i \cdot \left(j \cdot y\right)\right)}\]

   if 64272744.59900391 < j

   1. Initial program 7.7

      \[\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)\]
   2. Using strategy rm

   3. Applied sub-neg 7.7

      \[\leadsto \left(x \cdot \color{blue}{\left(y \cdot z + \left(-t \cdot a\right)\right)} - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   4. Applied distribute-lft-in 7.7

      \[\leadsto \left(\color{blue}{\left(x \cdot \left(y \cdot z\right) + x \cdot \left(-t \cdot a\right)\right)} - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   5. Simplified 7.7

      \[\leadsto \left(\left(\color{blue}{\left(y \cdot z\right) \cdot x} + x \cdot \left(-t \cdot a\right)\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   6. Simplified 7.7

      \[\leadsto \left(\left(\left(y \cdot z\right) \cdot x + \color{blue}{\left(-t \cdot a\right) \cdot x}\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
   7. Using strategy rm

   8. Applied associate-*l* 8.2

      \[\leadsto \left(\left(\color{blue}{y \cdot \left(z \cdot x\right)} + \left(-t \cdot a\right) \cdot x\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
   9. Using strategy rm

   10. Applied sub-neg 8.2

       \[\leadsto \left(\left(y \cdot \left(z \cdot x\right) + \left(-t \cdot a\right) \cdot x\right) - b \cdot \color{blue}{\left(c \cdot z + \left(-i \cdot a\right)\right)}\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   11. Applied distribute-lft-in 8.2

       \[\leadsto \left(\left(y \cdot \left(z \cdot x\right) + \left(-t \cdot a\right) \cdot x\right) - \color{blue}{\left(b \cdot \left(c \cdot z\right) + b \cdot \left(-i \cdot a\right)\right)}\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   12. Simplified 8.7

       \[\leadsto \left(\left(y \cdot \left(z \cdot x\right) + \left(-t \cdot a\right) \cdot x\right) - \left(\color{blue}{z \cdot \left(b \cdot c\right)} + b \cdot \left(-i \cdot a\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   13. Simplified 8.7

       \[\leadsto \left(\left(y \cdot \left(z \cdot x\right) + \left(-t \cdot a\right) \cdot x\right) - \left(z \cdot \left(b \cdot c\right) + \color{blue}{\left(-i \cdot a\right) \cdot b}\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
3. Recombined 3 regimes into one program.

4. Final simplification 9.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;j \le -2.961055619344420626519795079213745347097 \cdot 10^{-21}:\\ \;\;\;\;\left(\left(y \cdot \left(z \cdot x\right) + t \cdot \left(\left(-a\right) \cdot x\right)\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\ \mathbf{elif}\;j \le 64272744.59900391101837158203125:\\ \;\;\;\;\left(\left(\left(y \cdot z\right) \cdot x + \left(-t \cdot a\right) \cdot x\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + \left(t \cdot \left(j \cdot c\right) - i \cdot \left(j \cdot y\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(y \cdot \left(z \cdot x\right) + \left(-t \cdot a\right) \cdot x\right) - \left(z \cdot \left(b \cdot c\right) + \left(-i \cdot a\right) \cdot b\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019208 +o rules:numerics
(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.1209789191959122e-33) (- (* x (- (* z y) (* a t))) (- (* b (- (* z c) (* a i))) (* (- (* c t) (* y i)) j))) (if (< t -4.7125538182184851e-169) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (/ (* j (- (pow (* c t) 2) (pow (* i y) 2))) (+ (* c t) (* i y)))) (if (< t -7.63353334603158369e-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) (pow (* i y) 2))) (+ (* 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)))))