\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)
\]
↓
\[\begin{array}{l}
t_1 := y \cdot z - t \cdot a\\
t_2 := x \cdot t_1\\
t_3 := j \cdot \left(a \cdot c - y \cdot i\right)\\
t_4 := \left(t_2 - b \cdot \left(z \cdot c - t \cdot i\right)\right) + t_3\\
\mathbf{if}\;t_4 \leq -\infty \lor \neg \left(t_4 \leq \infty\right):\\
\;\;\;\;\left(\left(t_2 + c \cdot \left(a \cdot j\right)\right) + i \cdot \left(t \cdot b - y \cdot j\right)\right) - c \cdot \left(z \cdot b\right)\\
\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(x, t_1, \mathsf{fma}\left(b, t \cdot i - z \cdot c, t_3\right)\right)\\
\end{array}
\]
(FPCore (x y z t a b c i j)
:precision binary64
(+
(- (* x (- (* y z) (* t a))) (* b (- (* c z) (* t i))))
(* j (- (* c a) (* y i)))))
↓
(FPCore (x y z t a b c i j)
:precision binary64
(let* ((t_1 (- (* y z) (* t a)))
(t_2 (* x t_1))
(t_3 (* j (- (* a c) (* y i))))
(t_4 (+ (- t_2 (* b (- (* z c) (* t i)))) t_3)))
(if (or (<= t_4 (- INFINITY)) (not (<= t_4 INFINITY)))
(- (+ (+ t_2 (* c (* a j))) (* i (- (* t b) (* y j)))) (* c (* z b)))
(fma x t_1 (fma b (- (* t i) (* z c)) t_3)))))
\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)
↓
\begin{array}{l}
t_1 := y \cdot z - t \cdot a\\
t_2 := x \cdot t_1\\
t_3 := j \cdot \left(a \cdot c - y \cdot i\right)\\
t_4 := \left(t_2 - b \cdot \left(z \cdot c - t \cdot i\right)\right) + t_3\\
\mathbf{if}\;t_4 \leq -\infty \lor \neg \left(t_4 \leq \infty\right):\\
\;\;\;\;\left(\left(t_2 + c \cdot \left(a \cdot j\right)\right) + i \cdot \left(t \cdot b - y \cdot j\right)\right) - c \cdot \left(z \cdot b\right)\\
\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(x, t_1, \mathsf{fma}\left(b, t \cdot i - z \cdot c, t_3\right)\right)\\
\end{array}
if (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))) < -inf.0 or +inf.0 < (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i))))
Initial program 0.0%
\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)
\]
Simplified0.0%
\[\leadsto \color{blue}{\mathsf{fma}\left(j, a \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right)}
\]
Proof
[Start]0.0
\[ \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)
\]
+-commutative [=>]0.0
\[ \color{blue}{j \cdot \left(c \cdot a - y \cdot i\right) + \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right)}
\]
fma-def [=>]0.0
\[ \color{blue}{\mathsf{fma}\left(j, c \cdot a - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right)}
\]
*-commutative [=>]0.0
\[ \mathsf{fma}\left(j, \color{blue}{a \cdot c} - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right)
\]
*-commutative [=>]0.0
\[ \mathsf{fma}\left(j, a \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(\color{blue}{z \cdot c} - t \cdot i\right)\right)
\]
Taylor expanded in i around -inf 62.7%
\[\leadsto \color{blue}{\left(-1 \cdot \left(i \cdot \left(y \cdot j - t \cdot b\right)\right) + \left(\left(y \cdot z - a \cdot t\right) \cdot x + c \cdot \left(a \cdot j\right)\right)\right) - c \cdot \left(b \cdot z\right)}
\]
if -inf.0 < (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 t i)))) (*.f64 j (-.f64 (*.f64 c a) (*.f64 y i)))) < +inf.0
Initial program 89.4%
\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)
\]
Simplified89.4%
\[\leadsto \color{blue}{\mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, t \cdot i - z \cdot c, j \cdot \left(a \cdot c - y \cdot i\right)\right)\right)}
\]
Proof
[Start]89.4
\[ \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - t \cdot i\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)
\]
associate-+l- [=>]89.4
\[ \color{blue}{x \cdot \left(y \cdot z - t \cdot a\right) - \left(b \cdot \left(c \cdot z - t \cdot i\right) - j \cdot \left(c \cdot a - y \cdot i\right)\right)}
\]
fma-neg [=>]89.4
\[ \color{blue}{\mathsf{fma}\left(x, y \cdot z - t \cdot a, -\left(b \cdot \left(c \cdot z - t \cdot i\right) - j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)}
\]
neg-sub0 [=>]89.4
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{0 - \left(b \cdot \left(c \cdot z - t \cdot i\right) - j \cdot \left(c \cdot a - y \cdot i\right)\right)}\right)
\]
associate-+l- [<=]89.4
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{\left(0 - b \cdot \left(c \cdot z - t \cdot i\right)\right) + j \cdot \left(c \cdot a - y \cdot i\right)}\right)
\]
neg-sub0 [<=]89.4
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{\left(-b \cdot \left(c \cdot z - t \cdot i\right)\right)} + j \cdot \left(c \cdot a - y \cdot i\right)\right)
\]
distribute-rgt-neg-in [=>]89.4
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{b \cdot \left(-\left(c \cdot z - t \cdot i\right)\right)} + j \cdot \left(c \cdot a - y \cdot i\right)\right)
\]
fma-def [=>]89.4
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{\mathsf{fma}\left(b, -\left(c \cdot z - t \cdot i\right), j \cdot \left(c \cdot a - y \cdot i\right)\right)}\right)
\]
sub-neg [=>]89.4
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, -\color{blue}{\left(c \cdot z + \left(-t \cdot i\right)\right)}, j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)
\]
distribute-neg-in [=>]89.4
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, \color{blue}{\left(-c \cdot z\right) + \left(-\left(-t \cdot i\right)\right)}, j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)
\]
+-commutative [=>]89.4
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, \color{blue}{\left(-\left(-t \cdot i\right)\right) + \left(-c \cdot z\right)}, j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)
\]
remove-double-neg [=>]89.4
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, \color{blue}{t \cdot i} + \left(-c \cdot z\right), j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)
\]
sub-neg [<=]89.4
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, \color{blue}{t \cdot i - c \cdot z}, j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)
\]
*-commutative [=>]89.4
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, t \cdot i - \color{blue}{z \cdot c}, j \cdot \left(c \cdot a - y \cdot i\right)\right)\right)
\]
*-commutative [=>]89.4
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, t \cdot i - z \cdot c, j \cdot \left(\color{blue}{a \cdot c} - y \cdot i\right)\right)\right)
\]
Recombined 2 regimes into one program.
Final simplification86.7%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right) \leq -\infty \lor \neg \left(\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right) \leq \infty\right):\\
\;\;\;\;\left(\left(x \cdot \left(y \cdot z - t \cdot a\right) + c \cdot \left(a \cdot j\right)\right) + i \cdot \left(t \cdot b - y \cdot j\right)\right) - c \cdot \left(z \cdot b\right)\\
\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(b, t \cdot i - z \cdot c, j \cdot \left(a \cdot c - y \cdot i\right)\right)\right)\\
\end{array}
\]
Alternatives
Alternative 1
Accuracy
86.7%
Cost
5833
\[\begin{array}{l}
t_1 := b \cdot \left(z \cdot c - t \cdot i\right)\\
t_2 := x \cdot \left(y \cdot z - t \cdot a\right)\\
t_3 := j \cdot \left(a \cdot c - y \cdot i\right)\\
t_4 := \left(t_2 - t_1\right) + t_3\\
\mathbf{if}\;t_4 \leq -\infty \lor \neg \left(t_4 \leq \infty\right):\\
\;\;\;\;\left(\left(t_2 + c \cdot \left(a \cdot j\right)\right) + i \cdot \left(t \cdot b - y \cdot j\right)\right) - c \cdot \left(z \cdot b\right)\\
\mathbf{else}:\\
\;\;\;\;t_3 - \left(t_1 + \left(x \cdot \left(t \cdot a\right) - x \cdot \left(y \cdot z\right)\right)\right)\\
\end{array}
\]
Alternative 2
Accuracy
83.7%
Cost
5832
\[\begin{array}{l}
t_1 := b \cdot \left(z \cdot c - t \cdot i\right)\\
t_2 := j \cdot \left(a \cdot c - y \cdot i\right)\\
t_3 := \left(x \cdot \left(y \cdot z - t \cdot a\right) - t_1\right) + t_2\\
\mathbf{if}\;t_3 \leq -\infty:\\
\;\;\;\;t \cdot \left(b \cdot i - x \cdot a\right)\\
\mathbf{elif}\;t_3 \leq \infty:\\
\;\;\;\;t_2 - \left(t_1 + \left(x \cdot \left(t \cdot a\right) - x \cdot \left(y \cdot z\right)\right)\right)\\
\mathbf{else}:\\
\;\;\;\;i \cdot \left(t \cdot b - y \cdot j\right)\\
\end{array}
\]
Alternative 3
Accuracy
83.7%
Cost
5704
\[\begin{array}{l}
t_1 := \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - t \cdot i\right)\right) + j \cdot \left(a \cdot c - y \cdot i\right)\\
\mathbf{if}\;t_1 \leq -\infty:\\
\;\;\;\;t \cdot \left(b \cdot i - x \cdot a\right)\\
\mathbf{elif}\;t_1 \leq \infty:\\
\;\;\;\;t_1\\
\mathbf{else}:\\
\;\;\;\;i \cdot \left(t \cdot b - y \cdot j\right)\\
\end{array}
\]
herbie shell --seed 2023137
(FPCore (x y z t a b c i j)
:name "Data.Colour.Matrix:determinant from colour-2.3.3, A"
:precision binary64
:herbie-target
(if (< x -1.469694296777705e-64) (+ (- (* x (- (* y z) (* t a))) (/ (* b (- (pow (* c z) 2.0) (pow (* t i) 2.0))) (+ (* c z) (* t i)))) (* j (- (* c a) (* y i)))) (if (< x 3.2113527362226803e-147) (- (* (- (* b i) (* x a)) t) (- (* z (* c b)) (* j (- (* c a) (* y i))))) (+ (- (* x (- (* y z) (* t a))) (/ (* b (- (pow (* c z) 2.0) (pow (* t i) 2.0))) (+ (* c z) (* t i)))) (* j (- (* c a) (* y i))))))
(+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* t i)))) (* j (- (* c a) (* y i)))))