Average Error: 7.6 → 0.8
Time: 3.5s
Precision: 64
\[\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.53563446928647708 \cdot 10^{306}\right):\\ \;\;\;\;\mathsf{fma}\left(\frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}}, \frac{y}{\sqrt[3]{a}}, -\frac{z}{\sqrt[3]{a}} \cdot \frac{t}{\sqrt[3]{a} \cdot \sqrt[3]{a}}\right) + \frac{t}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \left(\left(-\frac{z}{\sqrt[3]{a}}\right) + \frac{z}{\sqrt[3]{a}}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{x \cdot y}{a} - \left(t \cdot z\right) \cdot \frac{1}{a}\\ \end{array}\]
\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.53563446928647708 \cdot 10^{306}\right):\\
\;\;\;\;\mathsf{fma}\left(\frac{x}{\sqrt[3]{a} \cdot \sqrt[3]{a}}, \frac{y}{\sqrt[3]{a}}, -\frac{z}{\sqrt[3]{a}} \cdot \frac{t}{\sqrt[3]{a} \cdot \sqrt[3]{a}}\right) + \frac{t}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \left(\left(-\frac{z}{\sqrt[3]{a}}\right) + \frac{z}{\sqrt[3]{a}}\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{x \cdot y}{a} - \left(t \cdot z\right) \cdot \frac{1}{a}\\

\end{array}
double f(double x, double y, double z, double t, double a) {
        double r934181 = x;
        double r934182 = y;
        double r934183 = r934181 * r934182;
        double r934184 = z;
        double r934185 = t;
        double r934186 = r934184 * r934185;
        double r934187 = r934183 - r934186;
        double r934188 = a;
        double r934189 = r934187 / r934188;
        return r934189;
}
↓
double f(double x, double y, double z, double t, double a) {
        double r934190 = x;
        double r934191 = y;
        double r934192 = r934190 * r934191;
        double r934193 = z;
        double r934194 = t;
        double r934195 = r934193 * r934194;
        double r934196 = r934192 - r934195;
        double r934197 = -inf.0;
        bool r934198 = r934196 <= r934197;
        double r934199 = 8.535634469286477e+306;
        bool r934200 = r934196 <= r934199;
        double r934201 = !r934200;
        bool r934202 = r934198 || r934201;
        double r934203 = a;
        double r934204 = cbrt(r934203);
        double r934205 = r934204 * r934204;
        double r934206 = r934190 / r934205;
        double r934207 = r934191 / r934204;
        double r934208 = r934193 / r934204;
        double r934209 = r934194 / r934205;
        double r934210 = r934208 * r934209;
        double r934211 = -r934210;
        double r934212 = fma(r934206, r934207, r934211);
        double r934213 = -r934208;
        double r934214 = r934213 + r934208;
        double r934215 = r934209 * r934214;
        double r934216 = r934212 + r934215;
        double r934217 = r934192 / r934203;
        double r934218 = r934194 * r934193;
        double r934219 = 1.0;
        double r934220 = r934219 / r934203;
        double r934221 = r934218 * r934220;
        double r934222 = r934217 - r934221;
        double r934223 = r934202 ? r934216 : r934222;
        return r934223;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Target

Original7.6
Target6.2
Herbie0.8
\[\begin{array}{l} \mathbf{if}\;z \lt -2.46868496869954822 \cdot 10^{170}:\\ \;\;\;\;\frac{y}{a} \cdot x - \frac{t}{a} \cdot z\\ \mathbf{elif}\;z \lt 6.30983112197837121 \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 2 regimes

  2. if (- (* x y) (* z t)) < -inf.0 or 8.535634469286477e+306 < (- (* x y) (* z t))

    1. Initial program 63.3

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

    3. Applied div-sub63.3

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

    4. Simplified63.3

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

    6. Applied add-cube-cbrt63.3

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

    7. Applied times-frac32.0

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

    8. Applied add-cube-cbrt32.0

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

    9. Applied times-frac1.3

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

    10. Applied prod-diff1.3

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

    11. Simplified1.3

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

    if -inf.0 < (- (* x y) (* z t)) < 8.535634469286477e+306

    1. Initial program 0.7

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

    3. Applied div-sub0.7

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

    4. Simplified0.7

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

    6. Applied div-inv0.7

      \[\leadsto \frac{x \cdot y}{a} - \color{blue}{\left(t \cdot z\right) \cdot \frac{1}{a}}\]
  3. Recombined 2 regimes into one program.

  4. Final simplification0.8

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

Reproduce

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

  :herbie-target
  (if (< z -2.468684968699548e+170) (- (* (/ y a) x) (* (/ t a) z)) (if (< z 6.309831121978371e-71) (/ (- (* x y) (* z t)) a) (- (* (/ y a) x) (* (/ t a) z))))

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