| Alternative 1 | |
|---|---|
| Error | 3.1 |
| Cost | 3792 |
(FPCore (x y z t a) :precision binary64 (/ (- x (* y z)) (- t (* a z))))
(FPCore (x y z t a)
:precision binary64
(let* ((t_1 (/ (- x (* y z)) (- t (* z a)))) (t_2 (- (* y z) x)))
(if (<= t_1 (- INFINITY))
(/ y (/ (- (* z a) t) z))
(if (<= t_1 -2e-314)
t_1
(if (<= t_1 0.0)
(/ (/ t_2 a) z)
(if (<= t_1 1e+303) (/ t_2 (fma z a (- t))) (/ y a)))))))double code(double x, double y, double z, double t, double a) {
return (x - (y * z)) / (t - (a * z));
}
double code(double x, double y, double z, double t, double a) {
double t_1 = (x - (y * z)) / (t - (z * a));
double t_2 = (y * z) - x;
double tmp;
if (t_1 <= -((double) INFINITY)) {
tmp = y / (((z * a) - t) / z);
} else if (t_1 <= -2e-314) {
tmp = t_1;
} else if (t_1 <= 0.0) {
tmp = (t_2 / a) / z;
} else if (t_1 <= 1e+303) {
tmp = t_2 / fma(z, a, -t);
} else {
tmp = y / a;
}
return tmp;
}
function code(x, y, z, t, a) return Float64(Float64(x - Float64(y * z)) / Float64(t - Float64(a * z))) end
function code(x, y, z, t, a) t_1 = Float64(Float64(x - Float64(y * z)) / Float64(t - Float64(z * a))) t_2 = Float64(Float64(y * z) - x) tmp = 0.0 if (t_1 <= Float64(-Inf)) tmp = Float64(y / Float64(Float64(Float64(z * a) - t) / z)); elseif (t_1 <= -2e-314) tmp = t_1; elseif (t_1 <= 0.0) tmp = Float64(Float64(t_2 / a) / z); elseif (t_1 <= 1e+303) tmp = Float64(t_2 / fma(z, a, Float64(-t))); else tmp = Float64(y / a); end return tmp end
code[x_, y_, z_, t_, a_] := N[(N[(x - N[(y * z), $MachinePrecision]), $MachinePrecision] / N[(t - N[(a * z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
code[x_, y_, z_, t_, a_] := Block[{t$95$1 = N[(N[(x - N[(y * z), $MachinePrecision]), $MachinePrecision] / N[(t - N[(z * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[(y * z), $MachinePrecision] - x), $MachinePrecision]}, If[LessEqual[t$95$1, (-Infinity)], N[(y / N[(N[(N[(z * a), $MachinePrecision] - t), $MachinePrecision] / z), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$1, -2e-314], t$95$1, If[LessEqual[t$95$1, 0.0], N[(N[(t$95$2 / a), $MachinePrecision] / z), $MachinePrecision], If[LessEqual[t$95$1, 1e+303], N[(t$95$2 / N[(z * a + (-t)), $MachinePrecision]), $MachinePrecision], N[(y / a), $MachinePrecision]]]]]]]
\frac{x - y \cdot z}{t - a \cdot z}
\begin{array}{l}
t_1 := \frac{x - y \cdot z}{t - z \cdot a}\\
t_2 := y \cdot z - x\\
\mathbf{if}\;t_1 \leq -\infty:\\
\;\;\;\;\frac{y}{\frac{z \cdot a - t}{z}}\\
\mathbf{elif}\;t_1 \leq -2 \cdot 10^{-314}:\\
\;\;\;\;t_1\\
\mathbf{elif}\;t_1 \leq 0:\\
\;\;\;\;\frac{\frac{t_2}{a}}{z}\\
\mathbf{elif}\;t_1 \leq 10^{+303}:\\
\;\;\;\;\frac{t_2}{\mathsf{fma}\left(z, a, -t\right)}\\
\mathbf{else}:\\
\;\;\;\;\frac{y}{a}\\
\end{array}
| Original | 10.7 |
|---|---|
| Target | 1.8 |
| Herbie | 3.1 |
if (/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (*.f64 a z))) < -inf.0Initial program 64.0
Simplified64.0
[Start]64.0 | \[ \frac{x - y \cdot z}{t - a \cdot z}
\] |
|---|---|
sub-neg [=>]64.0 | \[ \frac{\color{blue}{x + \left(-y \cdot z\right)}}{t - a \cdot z}
\] |
remove-double-neg [<=]64.0 | \[ \frac{\color{blue}{\left(-\left(-x\right)\right)} + \left(-y \cdot z\right)}{t - a \cdot z}
\] |
distribute-neg-in [<=]64.0 | \[ \frac{\color{blue}{-\left(\left(-x\right) + y \cdot z\right)}}{t - a \cdot z}
\] |
+-commutative [<=]64.0 | \[ \frac{-\color{blue}{\left(y \cdot z + \left(-x\right)\right)}}{t - a \cdot z}
\] |
sub-neg [<=]64.0 | \[ \frac{-\color{blue}{\left(y \cdot z - x\right)}}{t - a \cdot z}
\] |
neg-mul-1 [=>]64.0 | \[ \frac{\color{blue}{-1 \cdot \left(y \cdot z - x\right)}}{t - a \cdot z}
\] |
sub-neg [=>]64.0 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{t + \left(-a \cdot z\right)}}
\] |
remove-double-neg [<=]64.0 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{\left(-\left(-t\right)\right)} + \left(-a \cdot z\right)}
\] |
distribute-neg-in [<=]64.0 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{-\left(\left(-t\right) + a \cdot z\right)}}
\] |
+-commutative [<=]64.0 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{-\color{blue}{\left(a \cdot z + \left(-t\right)\right)}}
\] |
sub-neg [<=]64.0 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{-\color{blue}{\left(a \cdot z - t\right)}}
\] |
neg-mul-1 [=>]64.0 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{-1 \cdot \left(a \cdot z - t\right)}}
\] |
times-frac [=>]64.0 | \[ \color{blue}{\frac{-1}{-1} \cdot \frac{y \cdot z - x}{a \cdot z - t}}
\] |
metadata-eval [=>]64.0 | \[ \color{blue}{1} \cdot \frac{y \cdot z - x}{a \cdot z - t}
\] |
*-lft-identity [=>]64.0 | \[ \color{blue}{\frac{y \cdot z - x}{a \cdot z - t}}
\] |
*-commutative [=>]64.0 | \[ \frac{y \cdot z - x}{\color{blue}{z \cdot a} - t}
\] |
Applied egg-rr64.0
Taylor expanded in y around inf 64.0
Simplified0.2
[Start]64.0 | \[ \frac{y \cdot z}{a \cdot z - t}
\] |
|---|---|
associate-/l* [=>]0.2 | \[ \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}}
\] |
if -inf.0 < (/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (*.f64 a z))) < -1.9999999999e-314Initial program 0.2
if -1.9999999999e-314 < (/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (*.f64 a z))) < -0.0Initial program 26.0
Simplified26.0
[Start]26.0 | \[ \frac{x - y \cdot z}{t - a \cdot z}
\] |
|---|---|
sub-neg [=>]26.0 | \[ \frac{\color{blue}{x + \left(-y \cdot z\right)}}{t - a \cdot z}
\] |
remove-double-neg [<=]26.0 | \[ \frac{\color{blue}{\left(-\left(-x\right)\right)} + \left(-y \cdot z\right)}{t - a \cdot z}
\] |
distribute-neg-in [<=]26.0 | \[ \frac{\color{blue}{-\left(\left(-x\right) + y \cdot z\right)}}{t - a \cdot z}
\] |
+-commutative [<=]26.0 | \[ \frac{-\color{blue}{\left(y \cdot z + \left(-x\right)\right)}}{t - a \cdot z}
\] |
sub-neg [<=]26.0 | \[ \frac{-\color{blue}{\left(y \cdot z - x\right)}}{t - a \cdot z}
\] |
neg-mul-1 [=>]26.0 | \[ \frac{\color{blue}{-1 \cdot \left(y \cdot z - x\right)}}{t - a \cdot z}
\] |
sub-neg [=>]26.0 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{t + \left(-a \cdot z\right)}}
\] |
remove-double-neg [<=]26.0 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{\left(-\left(-t\right)\right)} + \left(-a \cdot z\right)}
\] |
distribute-neg-in [<=]26.0 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{-\left(\left(-t\right) + a \cdot z\right)}}
\] |
+-commutative [<=]26.0 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{-\color{blue}{\left(a \cdot z + \left(-t\right)\right)}}
\] |
sub-neg [<=]26.0 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{-\color{blue}{\left(a \cdot z - t\right)}}
\] |
neg-mul-1 [=>]26.0 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{-1 \cdot \left(a \cdot z - t\right)}}
\] |
times-frac [=>]26.0 | \[ \color{blue}{\frac{-1}{-1} \cdot \frac{y \cdot z - x}{a \cdot z - t}}
\] |
metadata-eval [=>]26.0 | \[ \color{blue}{1} \cdot \frac{y \cdot z - x}{a \cdot z - t}
\] |
*-lft-identity [=>]26.0 | \[ \color{blue}{\frac{y \cdot z - x}{a \cdot z - t}}
\] |
*-commutative [=>]26.0 | \[ \frac{y \cdot z - x}{\color{blue}{z \cdot a} - t}
\] |
Applied egg-rr26.0
Taylor expanded in z around inf 42.7
Applied egg-rr14.1
if -0.0 < (/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (*.f64 a z))) < 1e303Initial program 0.2
Simplified0.2
[Start]0.2 | \[ \frac{x - y \cdot z}{t - a \cdot z}
\] |
|---|---|
sub-neg [=>]0.2 | \[ \frac{\color{blue}{x + \left(-y \cdot z\right)}}{t - a \cdot z}
\] |
remove-double-neg [<=]0.2 | \[ \frac{\color{blue}{\left(-\left(-x\right)\right)} + \left(-y \cdot z\right)}{t - a \cdot z}
\] |
distribute-neg-in [<=]0.2 | \[ \frac{\color{blue}{-\left(\left(-x\right) + y \cdot z\right)}}{t - a \cdot z}
\] |
+-commutative [<=]0.2 | \[ \frac{-\color{blue}{\left(y \cdot z + \left(-x\right)\right)}}{t - a \cdot z}
\] |
sub-neg [<=]0.2 | \[ \frac{-\color{blue}{\left(y \cdot z - x\right)}}{t - a \cdot z}
\] |
neg-mul-1 [=>]0.2 | \[ \frac{\color{blue}{-1 \cdot \left(y \cdot z - x\right)}}{t - a \cdot z}
\] |
sub-neg [=>]0.2 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{t + \left(-a \cdot z\right)}}
\] |
remove-double-neg [<=]0.2 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{\left(-\left(-t\right)\right)} + \left(-a \cdot z\right)}
\] |
distribute-neg-in [<=]0.2 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{-\left(\left(-t\right) + a \cdot z\right)}}
\] |
+-commutative [<=]0.2 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{-\color{blue}{\left(a \cdot z + \left(-t\right)\right)}}
\] |
sub-neg [<=]0.2 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{-\color{blue}{\left(a \cdot z - t\right)}}
\] |
neg-mul-1 [=>]0.2 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{-1 \cdot \left(a \cdot z - t\right)}}
\] |
times-frac [=>]0.2 | \[ \color{blue}{\frac{-1}{-1} \cdot \frac{y \cdot z - x}{a \cdot z - t}}
\] |
metadata-eval [=>]0.2 | \[ \color{blue}{1} \cdot \frac{y \cdot z - x}{a \cdot z - t}
\] |
*-lft-identity [=>]0.2 | \[ \color{blue}{\frac{y \cdot z - x}{a \cdot z - t}}
\] |
*-commutative [=>]0.2 | \[ \frac{y \cdot z - x}{\color{blue}{z \cdot a} - t}
\] |
Applied egg-rr0.2
if 1e303 < (/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (*.f64 a z))) Initial program 62.6
Simplified62.6
[Start]62.6 | \[ \frac{x - y \cdot z}{t - a \cdot z}
\] |
|---|---|
sub-neg [=>]62.6 | \[ \frac{\color{blue}{x + \left(-y \cdot z\right)}}{t - a \cdot z}
\] |
remove-double-neg [<=]62.6 | \[ \frac{\color{blue}{\left(-\left(-x\right)\right)} + \left(-y \cdot z\right)}{t - a \cdot z}
\] |
distribute-neg-in [<=]62.6 | \[ \frac{\color{blue}{-\left(\left(-x\right) + y \cdot z\right)}}{t - a \cdot z}
\] |
+-commutative [<=]62.6 | \[ \frac{-\color{blue}{\left(y \cdot z + \left(-x\right)\right)}}{t - a \cdot z}
\] |
sub-neg [<=]62.6 | \[ \frac{-\color{blue}{\left(y \cdot z - x\right)}}{t - a \cdot z}
\] |
neg-mul-1 [=>]62.6 | \[ \frac{\color{blue}{-1 \cdot \left(y \cdot z - x\right)}}{t - a \cdot z}
\] |
sub-neg [=>]62.6 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{t + \left(-a \cdot z\right)}}
\] |
remove-double-neg [<=]62.6 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{\left(-\left(-t\right)\right)} + \left(-a \cdot z\right)}
\] |
distribute-neg-in [<=]62.6 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{-\left(\left(-t\right) + a \cdot z\right)}}
\] |
+-commutative [<=]62.6 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{-\color{blue}{\left(a \cdot z + \left(-t\right)\right)}}
\] |
sub-neg [<=]62.6 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{-\color{blue}{\left(a \cdot z - t\right)}}
\] |
neg-mul-1 [=>]62.6 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{-1 \cdot \left(a \cdot z - t\right)}}
\] |
times-frac [=>]62.6 | \[ \color{blue}{\frac{-1}{-1} \cdot \frac{y \cdot z - x}{a \cdot z - t}}
\] |
metadata-eval [=>]62.6 | \[ \color{blue}{1} \cdot \frac{y \cdot z - x}{a \cdot z - t}
\] |
*-lft-identity [=>]62.6 | \[ \color{blue}{\frac{y \cdot z - x}{a \cdot z - t}}
\] |
*-commutative [=>]62.6 | \[ \frac{y \cdot z - x}{\color{blue}{z \cdot a} - t}
\] |
Taylor expanded in z around inf 11.7
Final simplification3.1
| Alternative 1 | |
|---|---|
| Error | 3.1 |
| Cost | 3792 |
| Alternative 2 | |
|---|---|
| Error | 18.8 |
| Cost | 1369 |
| Alternative 3 | |
|---|---|
| Error | 18.7 |
| Cost | 1369 |
| Alternative 4 | |
|---|---|
| Error | 25.7 |
| Cost | 1108 |
| Alternative 5 | |
|---|---|
| Error | 18.6 |
| Cost | 1040 |
| Alternative 6 | |
|---|---|
| Error | 31.6 |
| Cost | 912 |
| Alternative 7 | |
|---|---|
| Error | 30.9 |
| Cost | 912 |
| Alternative 8 | |
|---|---|
| Error | 31.9 |
| Cost | 780 |
| Alternative 9 | |
|---|---|
| Error | 31.7 |
| Cost | 780 |
| Alternative 10 | |
|---|---|
| Error | 18.7 |
| Cost | 777 |
| Alternative 11 | |
|---|---|
| Error | 30.3 |
| Cost | 456 |
| Alternative 12 | |
|---|---|
| Error | 41.7 |
| Cost | 192 |
herbie shell --seed 2023039
(FPCore (x y z t a)
:name "Diagrams.Solve.Tridiagonal:solveTriDiagonal from diagrams-solve-0.1, A"
:precision binary64
:herbie-target
(if (< z -32113435955957344.0) (- (/ x (- t (* a z))) (/ y (- (/ t z) a))) (if (< z 3.5139522372978296e-86) (* (- x (* y z)) (/ 1.0 (- t (* a z)))) (- (/ x (- t (* a z))) (/ y (- (/ t z) a)))))
(/ (- x (* y z)) (- t (* a z))))