Data.Colour.Matrix:inverse from colour-2.3.3, B

Average Error: 7.7 → 1.6

Time: 11.0s

Precision: 64

Math

\[\frac{x \cdot y - z \cdot t}{a}\]

↓

\[\begin{array}{l} \mathbf{if}\;x \cdot y - z \cdot t = -\infty \lor \neg \left(x \cdot y - z \cdot t \le 8.625599261974259545830604107555064080357 \cdot 10^{293}\right):\\ \;\;\;\;\left(-t \cdot \frac{z}{a}\right) + \frac{y \cdot \frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}}}{{\left(\sqrt[3]{\sqrt[3]{a}}\right)}^{3}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot y - t \cdot z}{a}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a) {
        double r556115 = x;
        double r556116 = y;
        double r556117 = r556115 * r556116;
        double r556118 = z;
        double r556119 = t;
        double r556120 = r556118 * r556119;
        double r556121 = r556117 - r556120;
        double r556122 = a;
        double r556123 = r556121 / r556122;
        return r556123;
}

↓

double f(double x, double y, double z, double t, double a) {
        double r556124 = x;
        double r556125 = y;
        double r556126 = r556124 * r556125;
        double r556127 = z;
        double r556128 = t;
        double r556129 = r556127 * r556128;
        double r556130 = r556126 - r556129;
        double r556131 = -inf.0;
        bool r556132 = r556130 <= r556131;
        double r556133 = 8.62559926197426e+293;
        bool r556134 = r556130 <= r556133;
        double r556135 = !r556134;
        bool r556136 = r556132 || r556135;
        double r556137 = a;
        double r556138 = r556127 / r556137;
        double r556139 = r556128 * r556138;
        double r556140 = -r556139;
        double r556141 = cbrt(r556137);
        double r556142 = r556141 * r556141;
        double r556143 = r556124 / r556142;
        double r556144 = r556125 * r556143;
        double r556145 = cbrt(r556141);
        double r556146 = 3.0;
        double r556147 = pow(r556145, r556146);
        double r556148 = r556144 / r556147;
        double r556149 = r556140 + r556148;
        double r556150 = r556128 * r556127;
        double r556151 = r556126 - r556150;
        double r556152 = r556151 / r556137;
        double r556153 = r556136 ? r556149 : r556152;
        return r556153;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Target

Original	7.7
Target	6.5
Herbie	1.6

\[\begin{array}{l} \mathbf{if}\;z \lt -2.468684968699548224247694913169778644284 \cdot 10^{170}:\\ \;\;\;\;\frac{y}{a} \cdot x - \frac{t}{a} \cdot z\\ \mathbf{elif}\;z \lt 6.309831121978371209578784129518242708809 \cdot 10^{-71}:\\ \;\;\;\;\frac{x \cdot y - z \cdot t}{a}\\ \mathbf{else}:\\ \;\;\;\;\frac{y}{a} \cdot x - \frac{t}{a} \cdot z\\ \end{array}\]

Derivation

1. Split input into 3 regimes

2. if (- (* x y) (* z t)) < -inf.0

   1. Initial program 64.0

      \[\frac{x \cdot y - z \cdot t}{a}\]
   2. Using strategy rm

   3. Applied div-sub 64.0

      \[\leadsto \color{blue}{\frac{x \cdot y}{a} - \frac{z \cdot t}{a}}\]

   4. Simplified 64.0

      \[\leadsto \frac{x \cdot y}{a} - \color{blue}{\frac{t \cdot z}{a}}\]
   5. Using strategy rm

   6. Applied add-cube-cbrt 64.0

      \[\leadsto \frac{x \cdot y}{\color{blue}{\left(\sqrt[3]{a} \cdot \sqrt[3]{a}\right) \cdot \sqrt[3]{a}}} - \frac{t \cdot z}{a}\]

   7. Applied times-frac 35.4

      \[\leadsto \color{blue}{\frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\sqrt[3]{a}}} - \frac{t \cdot z}{a}\]
   8. Using strategy rm

   9. Applied *-un-lft-identity 35.4

      \[\leadsto \frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\sqrt[3]{a}} - \frac{t \cdot z}{\color{blue}{1 \cdot a}}\]

   10. Applied times-frac 0.8

       \[\leadsto \frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\sqrt[3]{a}} - \color{blue}{\frac{t}{1} \cdot \frac{z}{a}}\]

   11. Simplified 0.8

       \[\leadsto \frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\sqrt[3]{a}} - \color{blue}{t} \cdot \frac{z}{a}\]
   12. Using strategy rm

   13. Applied add-cube-cbrt 0.9

       \[\leadsto \frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\color{blue}{\left(\sqrt[3]{\sqrt[3]{a}} \cdot \sqrt[3]{\sqrt[3]{a}}\right) \cdot \sqrt[3]{\sqrt[3]{a}}}} - t \cdot \frac{z}{a}\]

   if -inf.0 < (- (* x y) (* z t)) < 8.62559926197426e+293

   1. Initial program 0.8

      \[\frac{x \cdot y - z \cdot t}{a}\]
   2. Using strategy rm

   3. Applied div-sub 0.8

      \[\leadsto \color{blue}{\frac{x \cdot y}{a} - \frac{z \cdot t}{a}}\]

   4. Simplified 0.8

      \[\leadsto \frac{x \cdot y}{a} - \color{blue}{\frac{t \cdot z}{a}}\]
   5. Using strategy rm

   6. Applied div-inv 0.9

      \[\leadsto \frac{x \cdot y}{a} - \color{blue}{\left(t \cdot z\right) \cdot \frac{1}{a}}\]

   7. Applied div-inv 0.9

      \[\leadsto \color{blue}{\left(x \cdot y\right) \cdot \frac{1}{a}} - \left(t \cdot z\right) \cdot \frac{1}{a}\]

   8. Applied distribute-rgt-out-- 0.9

      \[\leadsto \color{blue}{\frac{1}{a} \cdot \left(x \cdot y - t \cdot z\right)}\]

   if 8.62559926197426e+293 < (- (* x y) (* z t))

   1. Initial program 56.8

      \[\frac{x \cdot y - z \cdot t}{a}\]
   2. Using strategy rm

   3. Applied div-sub 56.8

      \[\leadsto \color{blue}{\frac{x \cdot y}{a} - \frac{z \cdot t}{a}}\]

   4. Simplified 56.8

      \[\leadsto \frac{x \cdot y}{a} - \color{blue}{\frac{t \cdot z}{a}}\]
   5. Using strategy rm

   6. Applied add-cube-cbrt 56.9

      \[\leadsto \frac{x \cdot y}{\color{blue}{\left(\sqrt[3]{a} \cdot \sqrt[3]{a}\right) \cdot \sqrt[3]{a}}} - \frac{t \cdot z}{a}\]

   7. Applied times-frac 33.7

      \[\leadsto \color{blue}{\frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\sqrt[3]{a}}} - \frac{t \cdot z}{a}\]
   8. Using strategy rm

   9. Applied *-un-lft-identity 33.7

      \[\leadsto \frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\sqrt[3]{a}} - \frac{t \cdot z}{\color{blue}{1 \cdot a}}\]

   10. Applied times-frac 0.7

       \[\leadsto \frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\sqrt[3]{a}} - \color{blue}{\frac{t}{1} \cdot \frac{z}{a}}\]

   11. Simplified 0.7

       \[\leadsto \frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\sqrt[3]{a}} - \color{blue}{t} \cdot \frac{z}{a}\]
   12. Using strategy rm

   13. Applied add-cube-cbrt 0.9

       \[\leadsto \frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{y}{\color{blue}{\left(\sqrt[3]{\sqrt[3]{a}} \cdot \sqrt[3]{\sqrt[3]{a}}\right) \cdot \sqrt[3]{\sqrt[3]{a}}}} - t \cdot \frac{z}{a}\]

   14. Applied *-un-lft-identity 0.9

       \[\leadsto \frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{\color{blue}{1 \cdot y}}{\left(\sqrt[3]{\sqrt[3]{a}} \cdot \sqrt[3]{\sqrt[3]{a}}\right) \cdot \sqrt[3]{\sqrt[3]{a}}} - t \cdot \frac{z}{a}\]

   15. Applied times-frac 0.9

       \[\leadsto \frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \color{blue}{\left(\frac{1}{\sqrt[3]{\sqrt[3]{a}} \cdot \sqrt[3]{\sqrt[3]{a}}} \cdot \frac{y}{\sqrt[3]{\sqrt[3]{a}}}\right)} - t \cdot \frac{z}{a}\]

   16. Applied associate-*r* 0.9

       \[\leadsto \color{blue}{\left(\frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{1}{\sqrt[3]{\sqrt[3]{a}} \cdot \sqrt[3]{\sqrt[3]{a}}}\right) \cdot \frac{y}{\sqrt[3]{\sqrt[3]{a}}}} - t \cdot \frac{z}{a}\]

   17. Simplified 0.9

       \[\leadsto \color{blue}{\frac{\frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}}}{\sqrt[3]{\sqrt[3]{a}} \cdot \sqrt[3]{\sqrt[3]{a}}}} \cdot \frac{y}{\sqrt[3]{\sqrt[3]{a}}} - t \cdot \frac{z}{a}\]
3. Recombined 3 regimes into one program.

4. Final simplification 1.6

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y - z \cdot t = -\infty \lor \neg \left(x \cdot y - z \cdot t \le 8.625599261974259545830604107555064080357 \cdot 10^{293}\right):\\ \;\;\;\;\left(-t \cdot \frac{z}{a}\right) + \frac{y \cdot \frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}}}{{\left(\sqrt[3]{\sqrt[3]{a}}\right)}^{3}}\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot y - t \cdot z}{a}\\ \end{array}\]

Reproduce

herbie shell --seed 2019297 
(FPCore (x y z t a)
  :name "Data.Colour.Matrix:inverse from colour-2.3.3, B"
  :precision binary64

  :herbie-target
  (if (< z -2.46868496869954822e170) (- (* (/ y a) x) (* (/ t a) z)) (if (< z 6.30983112197837121e-71) (/ (- (* x y) (* z t)) a) (- (* (/ y a) x) (* (/ t a) z))))

  (/ (- (* x y) (* z t)) a))