Average Error: 7.6 → 0.8
Time: 13.2s
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 2.726444610751361615310158740197919529974 \cdot 10^{264}\right):\\ \;\;\;\;\frac{x}{\frac{a}{y}} - \frac{t}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{z}{\sqrt[3]{a}}\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot y - z \cdot t\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 2.726444610751361615310158740197919529974 \cdot 10^{264}\right):\\
\;\;\;\;\frac{x}{\frac{a}{y}} - \frac{t}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{z}{\sqrt[3]{a}}\\

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

\end{array}
double f(double x, double y, double z, double t, double a) {
        double r623202 = x;
        double r623203 = y;
        double r623204 = r623202 * r623203;
        double r623205 = z;
        double r623206 = t;
        double r623207 = r623205 * r623206;
        double r623208 = r623204 - r623207;
        double r623209 = a;
        double r623210 = r623208 / r623209;
        return r623210;
}
↓
double f(double x, double y, double z, double t, double a) {
        double r623211 = x;
        double r623212 = y;
        double r623213 = r623211 * r623212;
        double r623214 = z;
        double r623215 = t;
        double r623216 = r623214 * r623215;
        double r623217 = r623213 - r623216;
        double r623218 = -inf.0;
        bool r623219 = r623217 <= r623218;
        double r623220 = 2.7264446107513616e+264;
        bool r623221 = r623217 <= r623220;
        double r623222 = !r623221;
        bool r623223 = r623219 || r623222;
        double r623224 = a;
        double r623225 = r623224 / r623212;
        double r623226 = r623211 / r623225;
        double r623227 = cbrt(r623224);
        double r623228 = r623227 * r623227;
        double r623229 = r623215 / r623228;
        double r623230 = r623214 / r623227;
        double r623231 = r623229 * r623230;
        double r623232 = r623226 - r623231;
        double r623233 = 1.0;
        double r623234 = r623233 / r623224;
        double r623235 = r623217 * r623234;
        double r623236 = r623223 ? r623232 : r623235;
        return r623236;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original7.6
Target6.0
Herbie0.8
\[\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 2 regimes

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

    1. Initial program 51.2

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

    3. Applied div-sub51.2

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

    4. Simplified51.2

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

    6. Applied associate-/l*26.4

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

    8. Applied add-cube-cbrt26.5

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

    9. Applied times-frac0.9

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

    if -inf.0 < (- (* x y) (* z t)) < 2.7264446107513616e+264

    1. Initial program 0.7

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

    3. Applied div-inv0.8

      \[\leadsto \color{blue}{\left(x \cdot y - z \cdot t\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 2.726444610751361615310158740197919529974 \cdot 10^{264}\right):\\ \;\;\;\;\frac{x}{\frac{a}{y}} - \frac{t}{\sqrt[3]{a} \cdot \sqrt[3]{a}} \cdot \frac{z}{\sqrt[3]{a}}\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot y - z \cdot t\right) \cdot \frac{1}{a}\\ \end{array}\]

Reproduce

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