Linear.Matrix:det33 from linear-1.19.1.3

Average Error: 12.7 → 10.7

Time: 26.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 -7.9425973173534991 \cdot 10^{59}:\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - \left(z \cdot \left(b \cdot c\right) + \left(\sqrt[3]{\left(i \cdot b\right) \cdot \left(-a\right)} \cdot \sqrt[3]{\left(i \cdot b\right) \cdot \left(-a\right)}\right) \cdot \sqrt[3]{\left(i \cdot b\right) \cdot \left(-a\right)}\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\ \mathbf{elif}\;j \le 4.66076012081488949 \cdot 10^{119}:\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - \left(z \cdot \left(b \cdot c\right) + \left(i \cdot b\right) \cdot \left(-a\right)\right)\right) + \left(t \cdot \left(j \cdot c\right) - i \cdot \left(j \cdot y\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - \left(\left(z \cdot b\right) \cdot c + \left(i \cdot b\right) \cdot \left(-a\right)\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 r384576 = x;
        double r384577 = y;
        double r384578 = z;
        double r384579 = r384577 * r384578;
        double r384580 = t;
        double r384581 = a;
        double r384582 = r384580 * r384581;
        double r384583 = r384579 - r384582;
        double r384584 = r384576 * r384583;
        double r384585 = b;
        double r384586 = c;
        double r384587 = r384586 * r384578;
        double r384588 = i;
        double r384589 = r384588 * r384581;
        double r384590 = r384587 - r384589;
        double r384591 = r384585 * r384590;
        double r384592 = r384584 - r384591;
        double r384593 = j;
        double r384594 = r384586 * r384580;
        double r384595 = r384588 * r384577;
        double r384596 = r384594 - r384595;
        double r384597 = r384593 * r384596;
        double r384598 = r384592 + r384597;
        return r384598;
}

↓

double f(double x, double y, double z, double t, double a, double b, double c, double i, double j) {
        double r384599 = j;
        double r384600 = -7.942597317353499e+59;
        bool r384601 = r384599 <= r384600;
        double r384602 = x;
        double r384603 = y;
        double r384604 = z;
        double r384605 = r384603 * r384604;
        double r384606 = t;
        double r384607 = a;
        double r384608 = r384606 * r384607;
        double r384609 = r384605 - r384608;
        double r384610 = r384602 * r384609;
        double r384611 = b;
        double r384612 = c;
        double r384613 = r384611 * r384612;
        double r384614 = r384604 * r384613;
        double r384615 = i;
        double r384616 = r384615 * r384611;
        double r384617 = -r384607;
        double r384618 = r384616 * r384617;
        double r384619 = cbrt(r384618);
        double r384620 = r384619 * r384619;
        double r384621 = r384620 * r384619;
        double r384622 = r384614 + r384621;
        double r384623 = r384610 - r384622;
        double r384624 = r384612 * r384606;
        double r384625 = r384615 * r384603;
        double r384626 = r384624 - r384625;
        double r384627 = r384599 * r384626;
        double r384628 = r384623 + r384627;
        double r384629 = 4.6607601208148895e+119;
        bool r384630 = r384599 <= r384629;
        double r384631 = r384614 + r384618;
        double r384632 = r384610 - r384631;
        double r384633 = r384599 * r384612;
        double r384634 = r384606 * r384633;
        double r384635 = r384599 * r384603;
        double r384636 = r384615 * r384635;
        double r384637 = r384634 - r384636;
        double r384638 = r384632 + r384637;
        double r384639 = r384604 * r384611;
        double r384640 = r384639 * r384612;
        double r384641 = r384640 + r384618;
        double r384642 = r384610 - r384641;
        double r384643 = r384642 + r384627;
        double r384644 = r384630 ? r384638 : r384643;
        double r384645 = r384601 ? r384628 : r384644;
        return r384645;
}

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.7
Target	16.6
Herbie	10.7

\[\begin{array}{l} \mathbf{if}\;t \lt -8.1209789191959122 \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.7125538182184851 \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.63353334603158369 \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.0535888557455487 \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 < -7.942597317353499e+59

   1. Initial program 8.2

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

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

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

      \[\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-rgt-neg-in 8.3

      \[\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(i \cdot \left(-a\right)\right)}\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   8. Applied associate-*r* 8.5

      \[\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 i\right) \cdot \left(-a\right)}\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   9. Simplified 8.5

      \[\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 b\right)} \cdot \left(-a\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
   10. Using strategy rm

   11. Applied add-cube-cbrt 8.6

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

   if -7.942597317353499e+59 < j < 4.6607601208148895e+119

   1. Initial program 14.1

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

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

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

      \[\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-rgt-neg-in 14.6

      \[\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(i \cdot \left(-a\right)\right)}\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   8. Applied associate-*r* 14.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 i\right) \cdot \left(-a\right)}\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   9. Simplified 14.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 b\right)} \cdot \left(-a\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   10. Taylor expanded around inf 11.3

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

   if 4.6607601208148895e+119 < j

   1. Initial program 8.1

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

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

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

      \[\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-rgt-neg-in 8.3

      \[\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(i \cdot \left(-a\right)\right)}\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   8. Applied associate-*r* 8.1

      \[\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 i\right) \cdot \left(-a\right)}\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]

   9. Simplified 8.1

      \[\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 b\right)} \cdot \left(-a\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\]
   10. Using strategy rm

   11. Applied associate-*r* 9.5

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

4. Final simplification 10.7

   \[\leadsto \begin{array}{l} \mathbf{if}\;j \le -7.9425973173534991 \cdot 10^{59}:\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - \left(z \cdot \left(b \cdot c\right) + \left(\sqrt[3]{\left(i \cdot b\right) \cdot \left(-a\right)} \cdot \sqrt[3]{\left(i \cdot b\right) \cdot \left(-a\right)}\right) \cdot \sqrt[3]{\left(i \cdot b\right) \cdot \left(-a\right)}\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\ \mathbf{elif}\;j \le 4.66076012081488949 \cdot 10^{119}:\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - \left(z \cdot \left(b \cdot c\right) + \left(i \cdot b\right) \cdot \left(-a\right)\right)\right) + \left(t \cdot \left(j \cdot c\right) - i \cdot \left(j \cdot y\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - \left(\left(z \cdot b\right) \cdot c + \left(i \cdot b\right) \cdot \left(-a\right)\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019198 +o rules:numerics
(FPCore (x y z t a b c i j)
  :name "Linear.Matrix:det33 from linear-1.19.1.3"

  :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)))))