Average Error: 7.6 → 4.1
Time: 10.1s
Precision: binary64
\[[x, y] = \mathsf{sort}([x, y]) \\]
\[\frac{x \cdot y - z \cdot t}{a} \]
↓
\[\begin{array}{l} t_1 := \mathsf{fma}\left(y, \frac{x}{a}, -\frac{z \cdot t}{a}\right)\\ \mathbf{if}\;x \cdot y \leq -3.582027594675778 \cdot 10^{+252}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;x \cdot y \leq 1.153667036843088 \cdot 10^{+244}:\\ \;\;\;\;\frac{\mathsf{fma}\left(1, -z \cdot t, x \cdot y\right)}{a}\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]
\frac{x \cdot y - z \cdot t}{a}
↓
\begin{array}{l}
t_1 := \mathsf{fma}\left(y, \frac{x}{a}, -\frac{z \cdot t}{a}\right)\\
\mathbf{if}\;x \cdot y \leq -3.582027594675778 \cdot 10^{+252}:\\
\;\;\;\;t_1\\

\mathbf{elif}\;x \cdot y \leq 1.153667036843088 \cdot 10^{+244}:\\
\;\;\;\;\frac{\mathsf{fma}\left(1, -z \cdot t, x \cdot y\right)}{a}\\

\mathbf{else}:\\
\;\;\;\;t_1\\


\end{array}

(FPCore (x y z t a) :precision binary64 (/ (- (* x y) (* z t)) a))
↓
(FPCore (x y z t a)
 :precision binary64
 (let* ((t_1 (fma y (/ x a) (- (/ (* z t) a)))))
   (if (<= (* x y) -3.582027594675778e+252)
     t_1
     (if (<= (* x y) 1.153667036843088e+244)
       (/ (fma 1.0 (- (* z t)) (* x y)) a)
       t_1))))
double code(double x, double y, double z, double t, double a) {
	return ((x * y) - (z * t)) / a;
}
↓
double code(double x, double y, double z, double t, double a) {
	double t_1 = fma(y, (x / a), -((z * t) / a));
	double tmp;
	if ((x * y) <= -3.582027594675778e+252) {
		tmp = t_1;
	} else if ((x * y) <= 1.153667036843088e+244) {
		tmp = fma(1.0, -(z * t), (x * y)) / a;
	} else {
		tmp = t_1;
	}
	return tmp;
}

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.0
Herbie4.1
\[\begin{array}{l} \mathbf{if}\;z < -2.468684968699548 \cdot 10^{+170}:\\ \;\;\;\;\frac{y}{a} \cdot x - \frac{t}{a} \cdot z\\ \mathbf{elif}\;z < 6.309831121978371 \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 (*.f64 x y) < -3.58202759467577795e252 or 1.153667036843088e244 < (*.f64 x y)

    1. Initial program 40.4

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

    2. Applied egg-rr5.6

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

    if -3.58202759467577795e252 < (*.f64 x y) < 1.153667036843088e244

    1. Initial program 4.0

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

    2. Applied egg-rr4.0

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

  4. Final simplification4.1

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \cdot y \leq -3.582027594675778 \cdot 10^{+252}:\\ \;\;\;\;\mathsf{fma}\left(y, \frac{x}{a}, -\frac{z \cdot t}{a}\right)\\ \mathbf{elif}\;x \cdot y \leq 1.153667036843088 \cdot 10^{+244}:\\ \;\;\;\;\frac{\mathsf{fma}\left(1, -z \cdot t, x \cdot y\right)}{a}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(y, \frac{x}{a}, -\frac{z \cdot t}{a}\right)\\ \end{array} \]

Reproduce

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