\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)
\]
↓
\[\begin{array}{l}
t_1 := b \cdot \left(a \cdot i - z \cdot c\right)\\
t_2 := y \cdot z - t \cdot a\\
t_3 := t \cdot c - y \cdot i\\
t_4 := \left(x \cdot t_2 + t_1\right) + j \cdot t_3\\
\mathbf{if}\;t_4 \leq -4 \cdot 10^{+304} \lor \neg \left(t_4 \leq 2 \cdot 10^{+302}\right):\\
\;\;\;\;\left(\left(c \cdot \left(t \cdot j\right) + y \cdot \left(x \cdot z\right)\right) + i \cdot \left(a \cdot b - y \cdot j\right)\right) - c \cdot \left(z \cdot b\right)\\
\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(x, t_2, \mathsf{fma}\left(j, t_3, b \cdot \mathsf{fma}\left(-c, z, z \cdot c\right) + t_1\right)\right)\\
\end{array}
\]
(FPCore (x y z t a b c i j)
:precision binary64
(+
(- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a))))
(* j (- (* c t) (* i y)))))
↓
(FPCore (x y z t a b c i j)
:precision binary64
(let* ((t_1 (* b (- (* a i) (* z c))))
(t_2 (- (* y z) (* t a)))
(t_3 (- (* t c) (* y i)))
(t_4 (+ (+ (* x t_2) t_1) (* j t_3))))
(if (or (<= t_4 -4e+304) (not (<= t_4 2e+302)))
(-
(+ (+ (* c (* t j)) (* y (* x z))) (* i (- (* a b) (* y j))))
(* c (* z b)))
(fma x t_2 (fma j t_3 (+ (* b (fma (- c) z (* z c))) t_1))))))
if (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 i a)))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y)))) < -3.9999999999999998e304 or 2.0000000000000002e302 < (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 i a)))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y))))
Initial program 6.3%
\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)
\]
Simplified6.3%
\[\leadsto \color{blue}{\mathsf{fma}\left(j, t \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(z \cdot c - a \cdot i\right)\right)}
\]
Proof
[Start]6.3
\[ \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)
\]
+-commutative [=>]6.3
\[ \color{blue}{j \cdot \left(c \cdot t - i \cdot y\right) + \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)}
\]
fma-def [=>]6.3
\[ \color{blue}{\mathsf{fma}\left(j, c \cdot t - i \cdot y, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)}
\]
*-commutative [=>]6.3
\[ \mathsf{fma}\left(j, c \cdot t - \color{blue}{y \cdot i}, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)
\]
*-commutative [=>]6.3
\[ \mathsf{fma}\left(j, \color{blue}{t \cdot c} - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right)
\]
*-commutative [=>]6.3
\[ \mathsf{fma}\left(j, t \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - \color{blue}{a \cdot i}\right)\right)
\]
*-commutative [=>]6.3
\[ \mathsf{fma}\left(j, t \cdot c - y \cdot i, x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(\color{blue}{z \cdot c} - a \cdot i\right)\right)
\]
Taylor expanded in i around -inf 60.7%
\[\leadsto \color{blue}{\left(-1 \cdot \left(i \cdot \left(y \cdot j - a \cdot b\right)\right) + \left(c \cdot \left(t \cdot j\right) + \left(y \cdot z - a \cdot t\right) \cdot x\right)\right) - c \cdot \left(b \cdot z\right)}
\]
if -3.9999999999999998e304 < (+.f64 (-.f64 (*.f64 x (-.f64 (*.f64 y z) (*.f64 t a))) (*.f64 b (-.f64 (*.f64 c z) (*.f64 i a)))) (*.f64 j (-.f64 (*.f64 c t) (*.f64 i y)))) < 2.0000000000000002e302
Initial program 98.8%
\[\left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)
\]
Simplified98.8%
\[\leadsto \color{blue}{\mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, b \cdot \left(a \cdot i - z \cdot c\right)\right)\right)}
\]
Proof
[Start]98.8
\[ \left(x \cdot \left(y \cdot z - t \cdot a\right) - b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)
\]
sub-neg [=>]98.8
\[ \color{blue}{\left(x \cdot \left(y \cdot z - t \cdot a\right) + \left(-b \cdot \left(c \cdot z - i \cdot a\right)\right)\right)} + j \cdot \left(c \cdot t - i \cdot y\right)
\]
associate-+l+ [=>]98.8
\[ \color{blue}{x \cdot \left(y \cdot z - t \cdot a\right) + \left(\left(-b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\right)}
\]
fma-def [=>]98.8
\[ \color{blue}{\mathsf{fma}\left(x, y \cdot z - t \cdot a, \left(-b \cdot \left(c \cdot z - i \cdot a\right)\right) + j \cdot \left(c \cdot t - i \cdot y\right)\right)}
\]
+-commutative [=>]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{j \cdot \left(c \cdot t - i \cdot y\right) + \left(-b \cdot \left(c \cdot z - i \cdot a\right)\right)}\right)
\]
fma-def [=>]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \color{blue}{\mathsf{fma}\left(j, c \cdot t - i \cdot y, -b \cdot \left(c \cdot z - i \cdot a\right)\right)}\right)
\]
*-commutative [=>]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, c \cdot t - \color{blue}{y \cdot i}, -b \cdot \left(c \cdot z - i \cdot a\right)\right)\right)
\]
*-commutative [=>]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, \color{blue}{t \cdot c} - y \cdot i, -b \cdot \left(c \cdot z - i \cdot a\right)\right)\right)
\]
distribute-rgt-neg-in [=>]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, \color{blue}{b \cdot \left(-\left(c \cdot z - i \cdot a\right)\right)}\right)\right)
\]
sub-neg [=>]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, b \cdot \left(-\color{blue}{\left(c \cdot z + \left(-i \cdot a\right)\right)}\right)\right)\right)
\]
+-commutative [=>]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, b \cdot \left(-\color{blue}{\left(\left(-i \cdot a\right) + c \cdot z\right)}\right)\right)\right)
\]
distribute-neg-in [=>]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, b \cdot \color{blue}{\left(\left(-\left(-i \cdot a\right)\right) + \left(-c \cdot z\right)\right)}\right)\right)
\]
unsub-neg [=>]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, b \cdot \color{blue}{\left(\left(-\left(-i \cdot a\right)\right) - c \cdot z\right)}\right)\right)
\]
remove-double-neg [=>]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, b \cdot \left(\color{blue}{i \cdot a} - c \cdot z\right)\right)\right)
\]
*-commutative [=>]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, b \cdot \left(\color{blue}{a \cdot i} - c \cdot z\right)\right)\right)
\]
*-commutative [=>]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, b \cdot \left(a \cdot i - \color{blue}{z \cdot c}\right)\right)\right)
\]
Applied egg-rr98.9%
\[\leadsto \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, \color{blue}{b \cdot \left(a \cdot i - z \cdot c\right) + \mathsf{fma}\left(-c, z, z \cdot c\right) \cdot b}\right)\right)
\]
Proof
[Start]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, b \cdot \left(a \cdot i - z \cdot c\right)\right)\right)
\]
prod-diff [=>]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, b \cdot \color{blue}{\left(\mathsf{fma}\left(a, i, -c \cdot z\right) + \mathsf{fma}\left(-c, z, c \cdot z\right)\right)}\right)\right)
\]
*-commutative [<=]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, b \cdot \left(\mathsf{fma}\left(a, i, -\color{blue}{z \cdot c}\right) + \mathsf{fma}\left(-c, z, c \cdot z\right)\right)\right)\right)
\]
fma-neg [<=]98.8
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, b \cdot \left(\color{blue}{\left(a \cdot i - z \cdot c\right)} + \mathsf{fma}\left(-c, z, c \cdot z\right)\right)\right)\right)
\]
distribute-rgt-in [=>]98.9
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, \color{blue}{\left(a \cdot i - z \cdot c\right) \cdot b + \mathsf{fma}\left(-c, z, c \cdot z\right) \cdot b}\right)\right)
\]
*-commutative [<=]98.9
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, \color{blue}{b \cdot \left(a \cdot i - z \cdot c\right)} + \mathsf{fma}\left(-c, z, c \cdot z\right) \cdot b\right)\right)
\]
*-commutative [<=]98.9
\[ \mathsf{fma}\left(x, y \cdot z - t \cdot a, \mathsf{fma}\left(j, t \cdot c - y \cdot i, b \cdot \left(a \cdot i - z \cdot c\right) + \mathsf{fma}\left(-c, z, \color{blue}{z \cdot c}\right) \cdot b\right)\right)
\]
Recombined 2 regimes into one program.
Final simplification93.1%
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(a \cdot i - z \cdot c\right)\right) + j \cdot \left(t \cdot c - y \cdot i\right) \leq -4 \cdot 10^{+304} \lor \neg \left(\left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(a \cdot i - z \cdot c\right)\right) + j \cdot \left(t \cdot c - y \cdot i\right) \leq 2 \cdot 10^{+302}\right):\\
\;\;\;\;\left(\left(c \cdot \left(t \cdot j\right) + y \cdot \left(x \cdot z\right)\right) + i \cdot \left(a \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(j, t \cdot c - y \cdot i, b \cdot \mathsf{fma}\left(-c, z, z \cdot c\right) + b \cdot \left(a \cdot i - z \cdot c\right)\right)\right)\\
\end{array}
\]
Alternatives
Alternative 1
Accuracy
93.1%
Cost
12681
\[\begin{array}{l}
t_1 := b \cdot \left(a \cdot i - z \cdot c\right)\\
t_2 := x \cdot \left(y \cdot z - t \cdot a\right)\\
t_3 := j \cdot \left(t \cdot c - y \cdot i\right)\\
t_4 := \left(t_2 + t_1\right) + t_3\\
\mathbf{if}\;t_4 \leq -4 \cdot 10^{+304} \lor \neg \left(t_4 \leq 2 \cdot 10^{+302}\right):\\
\;\;\;\;\left(\left(c \cdot \left(t \cdot j\right) + y \cdot \left(x \cdot z\right)\right) + i \cdot \left(a \cdot b - y \cdot j\right)\right) - c \cdot \left(z \cdot b\right)\\
\mathbf{else}:\\
\;\;\;\;\left(\left(t_2 + x \cdot \mathsf{fma}\left(-a, t, t \cdot a\right)\right) + t_1\right) + t_3\\
\end{array}
\]
Alternative 2
Accuracy
93.1%
Cost
11977
\[\begin{array}{l}
t_1 := t \cdot c - y \cdot i\\
t_2 := x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(a \cdot i - z \cdot c\right)\\
t_3 := t_2 + j \cdot t_1\\
\mathbf{if}\;t_3 \leq -4 \cdot 10^{+304} \lor \neg \left(t_3 \leq 2 \cdot 10^{+302}\right):\\
\;\;\;\;\left(\left(c \cdot \left(t \cdot j\right) + y \cdot \left(x \cdot z\right)\right) + i \cdot \left(a \cdot b - y \cdot j\right)\right) - c \cdot \left(z \cdot b\right)\\
\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(j, t_1, t_2\right)\\
\end{array}
\]
Alternative 3
Accuracy
93.1%
Cost
5705
\[\begin{array}{l}
t_1 := \left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(a \cdot i - z \cdot c\right)\right) + j \cdot \left(t \cdot c - y \cdot i\right)\\
\mathbf{if}\;t_1 \leq -4 \cdot 10^{+304} \lor \neg \left(t_1 \leq 2 \cdot 10^{+302}\right):\\
\;\;\;\;\left(\left(c \cdot \left(t \cdot j\right) + y \cdot \left(x \cdot z\right)\right) + i \cdot \left(a \cdot b - y \cdot j\right)\right) - c \cdot \left(z \cdot b\right)\\
\mathbf{else}:\\
\;\;\;\;t_1\\
\end{array}
\]
Alternative 4
Accuracy
86.1%
Cost
5704
\[\begin{array}{l}
t_1 := \left(x \cdot \left(y \cdot z - t \cdot a\right) + b \cdot \left(a \cdot i - z \cdot c\right)\right) + j \cdot \left(t \cdot c - y \cdot i\right)\\
\mathbf{if}\;t_1 \leq -4 \cdot 10^{+304}:\\
\;\;\;\;y \cdot \left(x \cdot z - i \cdot j\right)\\
\mathbf{elif}\;t_1 \leq 2 \cdot 10^{+306}:\\
\;\;\;\;t_1\\
\mathbf{else}:\\
\;\;\;\;i \cdot \left(a \cdot b - y \cdot j\right)\\
\end{array}
\]
herbie shell --seed 2023147
(FPCore (x y z t a b c i j)
:name "Linear.Matrix:det33 from linear-1.19.1.3"
:precision binary64
:herbie-target
(if (< t -8.120978919195912e-33) (- (* x (- (* z y) (* a t))) (- (* b (- (* z c) (* a i))) (* (- (* c t) (* y i)) j))) (if (< t -4.712553818218485e-169) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (/ (* j (- (pow (* c t) 2.0) (pow (* i y) 2.0))) (+ (* c t) (* i y)))) (if (< t -7.633533346031584e-308) (- (* x (- (* z y) (* a t))) (- (* b (- (* z c) (* a i))) (* (- (* c t) (* y i)) j))) (if (< t 1.0535888557455487e-139) (+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (/ (* j (- (pow (* c t) 2.0) (pow (* i y) 2.0))) (+ (* c t) (* i y)))) (- (* x (- (* z y) (* a t))) (- (* b (- (* z c) (* a i))) (* (- (* c t) (* y i)) j)))))))
(+ (- (* x (- (* y z) (* t a))) (* b (- (* c z) (* i a)))) (* j (- (* c t) (* i y)))))