Linear.Matrix:det33 from linear-1.19.1.3

Average Error: 12.5 → 9.0

Time: 26.0s

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 -3.558679195290626040559800458140671253204 \lor \neg \left(j \le 4.784801129022457779255706995671921542182 \cdot 10^{-23}\right):\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - \left(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)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(x \cdot z\right) \cdot \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right)\right) \cdot \sqrt[3]{y} + \left(-a \cdot \left(x \cdot t\right)\right)\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)\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b, double c, double i, double j) {
        double r416616 = x;
        double r416617 = y;
        double r416618 = z;
        double r416619 = r416617 * r416618;
        double r416620 = t;
        double r416621 = a;
        double r416622 = r416620 * r416621;
        double r416623 = r416619 - r416622;
        double r416624 = r416616 * r416623;
        double r416625 = b;
        double r416626 = c;
        double r416627 = r416626 * r416618;
        double r416628 = i;
        double r416629 = r416628 * r416621;
        double r416630 = r416627 - r416629;
        double r416631 = r416625 * r416630;
        double r416632 = r416624 - r416631;
        double r416633 = j;
        double r416634 = r416626 * r416620;
        double r416635 = r416628 * r416617;
        double r416636 = r416634 - r416635;
        double r416637 = r416633 * r416636;
        double r416638 = r416632 + r416637;
        return r416638;
}

↓

double f(double x, double y, double z, double t, double a, double b, double c, double i, double j) {
        double r416639 = j;
        double r416640 = -3.558679195290626;
        bool r416641 = r416639 <= r416640;
        double r416642 = 4.784801129022458e-23;
        bool r416643 = r416639 <= r416642;
        double r416644 = !r416643;
        bool r416645 = r416641 || r416644;
        double r416646 = x;
        double r416647 = y;
        double r416648 = z;
        double r416649 = r416647 * r416648;
        double r416650 = t;
        double r416651 = a;
        double r416652 = r416650 * r416651;
        double r416653 = r416649 - r416652;
        double r416654 = r416646 * r416653;
        double r416655 = b;
        double r416656 = c;
        double r416657 = r416655 * r416656;
        double r416658 = r416648 * r416657;
        double r416659 = i;
        double r416660 = r416659 * r416651;
        double r416661 = -r416660;
        double r416662 = r416655 * r416661;
        double r416663 = r416658 + r416662;
        double r416664 = r416654 - r416663;
        double r416665 = r416656 * r416650;
        double r416666 = r416659 * r416647;
        double r416667 = r416665 - r416666;
        double r416668 = r416639 * r416667;
        double r416669 = r416664 + r416668;
        double r416670 = r416646 * r416648;
        double r416671 = cbrt(r416647);
        double r416672 = r416671 * r416671;
        double r416673 = r416670 * r416672;
        double r416674 = r416673 * r416671;
        double r416675 = r416646 * r416650;
        double r416676 = r416651 * r416675;
        double r416677 = -r416676;
        double r416678 = r416674 + r416677;
        double r416679 = r416656 * r416648;
        double r416680 = r416679 - r416660;
        double r416681 = r416655 * r416680;
        double r416682 = r416678 - r416681;
        double r416683 = r416639 * r416656;
        double r416684 = r416650 * r416683;
        double r416685 = r416639 * r416647;
        double r416686 = r416659 * r416685;
        double r416687 = -r416686;
        double r416688 = r416684 + r416687;
        double r416689 = r416682 + r416688;
        double r416690 = r416645 ? r416669 : r416689;
        return r416690;
}

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.3
Herbie	9.0

\[\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 j < -3.558679195290626 or 4.784801129022458e-23 < j

   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 \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 7.6

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

      \[\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)\]

   if -3.558679195290626 < j < 4.784801129022458e-23

   1. Initial program 15.9

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

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

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

      \[\leadsto \left(\left(\color{blue}{x \cdot \left(z \cdot y\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)\]

   6. Simplified 15.8

      \[\leadsto \left(\left(x \cdot \left(z \cdot y\right) + \color{blue}{\left(-a \cdot \left(x \cdot t\right)\right)}\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-*r* 15.3

      \[\leadsto \left(\left(\color{blue}{\left(x \cdot z\right) \cdot y} + \left(-a \cdot \left(x \cdot t\right)\right)\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 add-cube-cbrt 15.5

       \[\leadsto \left(\left(\left(x \cdot z\right) \cdot \color{blue}{\left(\left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) \cdot \sqrt[3]{y}\right)} + \left(-a \cdot \left(x \cdot t\right)\right)\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-*r* 15.5

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

   13. Applied sub-neg 15.5

       \[\leadsto \left(\left(\left(\left(x \cdot z\right) \cdot \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right)\right) \cdot \sqrt[3]{y} + \left(-a \cdot \left(x \cdot t\right)\right)\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)}\]

   14. Applied distribute-lft-in 15.5

       \[\leadsto \left(\left(\left(\left(x \cdot z\right) \cdot \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right)\right) \cdot \sqrt[3]{y} + \left(-a \cdot \left(x \cdot t\right)\right)\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)}\]

   15. Simplified 13.0

       \[\leadsto \left(\left(\left(\left(x \cdot z\right) \cdot \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right)\right) \cdot \sqrt[3]{y} + \left(-a \cdot \left(x \cdot t\right)\right)\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)\]

   16. Simplified 9.8

       \[\leadsto \left(\left(\left(\left(x \cdot z\right) \cdot \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right)\right) \cdot \sqrt[3]{y} + \left(-a \cdot \left(x \cdot t\right)\right)\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)\]
3. Recombined 2 regimes into one program.

4. Final simplification 9.0

   \[\leadsto \begin{array}{l} \mathbf{if}\;j \le -3.558679195290626040559800458140671253204 \lor \neg \left(j \le 4.784801129022457779255706995671921542182 \cdot 10^{-23}\right):\\ \;\;\;\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - \left(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)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(x \cdot z\right) \cdot \left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right)\right) \cdot \sqrt[3]{y} + \left(-a \cdot \left(x \cdot t\right)\right)\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)\\ \end{array}\]

Reproduce

herbie shell --seed 2019303 
(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)))))