Linear.Matrix:det33 from linear-1.19.1.3

Average Error: 12.1 → 9.3

Time: 27.5s

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}\;b \le -1.746485226326191646256035493009197125697 \cdot 10^{-44} \lor \neg \left(b \le 6.97020109897896740211542344045198217806 \cdot 10^{-28}\right):\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + \left(t \cdot \left(j \cdot c\right) + \left(-i \cdot \left(j \cdot y\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - \left(z \cdot \left(b \cdot c\right) + \left(i \cdot \left(-b\right)\right) \cdot a\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 r426033 = x;
        double r426034 = y;
        double r426035 = z;
        double r426036 = r426034 * r426035;
        double r426037 = t;
        double r426038 = a;
        double r426039 = r426037 * r426038;
        double r426040 = r426036 - r426039;
        double r426041 = r426033 * r426040;
        double r426042 = b;
        double r426043 = c;
        double r426044 = r426043 * r426035;
        double r426045 = i;
        double r426046 = r426045 * r426038;
        double r426047 = r426044 - r426046;
        double r426048 = r426042 * r426047;
        double r426049 = r426041 - r426048;
        double r426050 = j;
        double r426051 = r426043 * r426037;
        double r426052 = r426045 * r426034;
        double r426053 = r426051 - r426052;
        double r426054 = r426050 * r426053;
        double r426055 = r426049 + r426054;
        return r426055;
}

↓

double f(double x, double y, double z, double t, double a, double b, double c, double i, double j) {
        double r426056 = b;
        double r426057 = -1.7464852263261916e-44;
        bool r426058 = r426056 <= r426057;
        double r426059 = 6.970201098978967e-28;
        bool r426060 = r426056 <= r426059;
        double r426061 = !r426060;
        bool r426062 = r426058 || r426061;
        double r426063 = x;
        double r426064 = y;
        double r426065 = z;
        double r426066 = r426064 * r426065;
        double r426067 = t;
        double r426068 = a;
        double r426069 = r426067 * r426068;
        double r426070 = r426066 - r426069;
        double r426071 = r426063 * r426070;
        double r426072 = c;
        double r426073 = r426072 * r426065;
        double r426074 = i;
        double r426075 = r426074 * r426068;
        double r426076 = r426073 - r426075;
        double r426077 = r426056 * r426076;
        double r426078 = r426071 - r426077;
        double r426079 = j;
        double r426080 = r426079 * r426072;
        double r426081 = r426067 * r426080;
        double r426082 = r426079 * r426064;
        double r426083 = r426074 * r426082;
        double r426084 = -r426083;
        double r426085 = r426081 + r426084;
        double r426086 = r426078 + r426085;
        double r426087 = r426056 * r426072;
        double r426088 = r426065 * r426087;
        double r426089 = -r426056;
        double r426090 = r426074 * r426089;
        double r426091 = r426090 * r426068;
        double r426092 = r426088 + r426091;
        double r426093 = r426071 - r426092;
        double r426094 = r426072 * r426067;
        double r426095 = r426074 * r426064;
        double r426096 = r426094 - r426095;
        double r426097 = r426079 * r426096;
        double r426098 = r426093 + r426097;
        double r426099 = r426062 ? r426086 : r426098;
        return r426099;
}

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.1
Target	15.9
Herbie	9.3

\[\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 2 regimes

2. if b < -1.7464852263261916e-44 or 6.970201098978967e-28 < b

   1. Initial program 7.6

      \[\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.6

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

   4. Applied distribute-lft-in 7.6

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

   5. Simplified 8.0

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

   6. Simplified 8.1

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

   if -1.7464852263261916e-44 < b < 6.970201098978967e-28

   1. Initial program 16.0

      \[\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 16.0

      \[\leadsto \left(x \cdot \left(y \cdot z - t \cdot a\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)\]

   4. Applied distribute-lft-in 16.0

      \[\leadsto \left(x \cdot \left(y \cdot z - t \cdot a\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)\]

   5. Simplified 13.2

      \[\leadsto \left(x \cdot \left(y \cdot z - t \cdot a\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)\]
   6. Using strategy rm

   7. Applied distribute-lft-neg-in 13.2

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

   8. Applied associate-*r* 10.4

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

   9. Simplified 10.4

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

4. Final simplification 9.3

   \[\leadsto \begin{array}{l} \mathbf{if}\;b \le -1.746485226326191646256035493009197125697 \cdot 10^{-44} \lor \neg \left(b \le 6.97020109897896740211542344045198217806 \cdot 10^{-28}\right):\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + \left(t \cdot \left(j \cdot c\right) + \left(-i \cdot \left(j \cdot y\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - \left(z \cdot \left(b \cdot c\right) + \left(i \cdot \left(-b\right)\right) \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019323 +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.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) (pow (* i y) 2))) (+ (* 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) (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)))))