| Alternative 1 | |
|---|---|
| Error | 4.1 |
| Cost | 2892 |
(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 (- (* z a) t)) (t_2 (/ (- x (* y z)) (- t (* z a)))))
(if (<= t_2 (- INFINITY))
(/ y (/ t_1 z))
(if (<= t_2 5e+287)
(- (/ (* y z) t_1) (/ x t_1))
(if (<= t_2 INFINITY) (* y (/ z t_1)) (/ 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 = (z * a) - t;
double t_2 = (x - (y * z)) / (t - (z * a));
double tmp;
if (t_2 <= -((double) INFINITY)) {
tmp = y / (t_1 / z);
} else if (t_2 <= 5e+287) {
tmp = ((y * z) / t_1) - (x / t_1);
} else if (t_2 <= ((double) INFINITY)) {
tmp = y * (z / t_1);
} else {
tmp = y / a;
}
return tmp;
}
public static double code(double x, double y, double z, double t, double a) {
return (x - (y * z)) / (t - (a * z));
}
public static double code(double x, double y, double z, double t, double a) {
double t_1 = (z * a) - t;
double t_2 = (x - (y * z)) / (t - (z * a));
double tmp;
if (t_2 <= -Double.POSITIVE_INFINITY) {
tmp = y / (t_1 / z);
} else if (t_2 <= 5e+287) {
tmp = ((y * z) / t_1) - (x / t_1);
} else if (t_2 <= Double.POSITIVE_INFINITY) {
tmp = y * (z / t_1);
} else {
tmp = y / a;
}
return tmp;
}
def code(x, y, z, t, a): return (x - (y * z)) / (t - (a * z))
def code(x, y, z, t, a): t_1 = (z * a) - t t_2 = (x - (y * z)) / (t - (z * a)) tmp = 0 if t_2 <= -math.inf: tmp = y / (t_1 / z) elif t_2 <= 5e+287: tmp = ((y * z) / t_1) - (x / t_1) elif t_2 <= math.inf: tmp = y * (z / t_1) 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(z * a) - t) t_2 = Float64(Float64(x - Float64(y * z)) / Float64(t - Float64(z * a))) tmp = 0.0 if (t_2 <= Float64(-Inf)) tmp = Float64(y / Float64(t_1 / z)); elseif (t_2 <= 5e+287) tmp = Float64(Float64(Float64(y * z) / t_1) - Float64(x / t_1)); elseif (t_2 <= Inf) tmp = Float64(y * Float64(z / t_1)); else tmp = Float64(y / a); end return tmp end
function tmp = code(x, y, z, t, a) tmp = (x - (y * z)) / (t - (a * z)); end
function tmp_2 = code(x, y, z, t, a) t_1 = (z * a) - t; t_2 = (x - (y * z)) / (t - (z * a)); tmp = 0.0; if (t_2 <= -Inf) tmp = y / (t_1 / z); elseif (t_2 <= 5e+287) tmp = ((y * z) / t_1) - (x / t_1); elseif (t_2 <= Inf) tmp = y * (z / t_1); else tmp = y / a; end tmp_2 = 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[(z * a), $MachinePrecision] - t), $MachinePrecision]}, Block[{t$95$2 = N[(N[(x - N[(y * z), $MachinePrecision]), $MachinePrecision] / N[(t - N[(z * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$2, (-Infinity)], N[(y / N[(t$95$1 / z), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$2, 5e+287], N[(N[(N[(y * z), $MachinePrecision] / t$95$1), $MachinePrecision] - N[(x / t$95$1), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$2, Infinity], N[(y * N[(z / t$95$1), $MachinePrecision]), $MachinePrecision], N[(y / a), $MachinePrecision]]]]]]
\frac{x - y \cdot z}{t - a \cdot z}
\begin{array}{l}
t_1 := z \cdot a - t\\
t_2 := \frac{x - y \cdot z}{t - z \cdot a}\\
\mathbf{if}\;t_2 \leq -\infty:\\
\;\;\;\;\frac{y}{\frac{t_1}{z}}\\
\mathbf{elif}\;t_2 \leq 5 \cdot 10^{+287}:\\
\;\;\;\;\frac{y \cdot z}{t_1} - \frac{x}{t_1}\\
\mathbf{elif}\;t_2 \leq \infty:\\
\;\;\;\;y \cdot \frac{z}{t_1}\\
\mathbf{else}:\\
\;\;\;\;\frac{y}{a}\\
\end{array}
Results
| Original | 10.8 |
|---|---|
| Target | 1.7 |
| Herbie | 4.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.1
[Start]64.0 | \[ \frac{y \cdot z}{a \cdot z - t}
\] |
|---|---|
associate-/l* [=>]0.1 | \[ \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}}
\] |
if -inf.0 < (/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (*.f64 a z))) < 5e287Initial program 4.3
Simplified4.3
[Start]4.3 | \[ \frac{x - y \cdot z}{t - a \cdot z}
\] |
|---|---|
sub-neg [=>]4.3 | \[ \frac{\color{blue}{x + \left(-y \cdot z\right)}}{t - a \cdot z}
\] |
remove-double-neg [<=]4.3 | \[ \frac{\color{blue}{\left(-\left(-x\right)\right)} + \left(-y \cdot z\right)}{t - a \cdot z}
\] |
distribute-neg-in [<=]4.3 | \[ \frac{\color{blue}{-\left(\left(-x\right) + y \cdot z\right)}}{t - a \cdot z}
\] |
+-commutative [<=]4.3 | \[ \frac{-\color{blue}{\left(y \cdot z + \left(-x\right)\right)}}{t - a \cdot z}
\] |
sub-neg [<=]4.3 | \[ \frac{-\color{blue}{\left(y \cdot z - x\right)}}{t - a \cdot z}
\] |
neg-mul-1 [=>]4.3 | \[ \frac{\color{blue}{-1 \cdot \left(y \cdot z - x\right)}}{t - a \cdot z}
\] |
sub-neg [=>]4.3 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{t + \left(-a \cdot z\right)}}
\] |
remove-double-neg [<=]4.3 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{\left(-\left(-t\right)\right)} + \left(-a \cdot z\right)}
\] |
distribute-neg-in [<=]4.3 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{-\left(\left(-t\right) + a \cdot z\right)}}
\] |
+-commutative [<=]4.3 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{-\color{blue}{\left(a \cdot z + \left(-t\right)\right)}}
\] |
sub-neg [<=]4.3 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{-\color{blue}{\left(a \cdot z - t\right)}}
\] |
neg-mul-1 [=>]4.3 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{-1 \cdot \left(a \cdot z - t\right)}}
\] |
times-frac [=>]4.3 | \[ \color{blue}{\frac{-1}{-1} \cdot \frac{y \cdot z - x}{a \cdot z - t}}
\] |
metadata-eval [=>]4.3 | \[ \color{blue}{1} \cdot \frac{y \cdot z - x}{a \cdot z - t}
\] |
*-lft-identity [=>]4.3 | \[ \color{blue}{\frac{y \cdot z - x}{a \cdot z - t}}
\] |
*-commutative [=>]4.3 | \[ \frac{y \cdot z - x}{\color{blue}{z \cdot a} - t}
\] |
Applied egg-rr4.3
if 5e287 < (/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (*.f64 a z))) < +inf.0Initial program 52.7
Simplified52.7
[Start]52.7 | \[ \frac{x - y \cdot z}{t - a \cdot z}
\] |
|---|---|
sub-neg [=>]52.7 | \[ \frac{\color{blue}{x + \left(-y \cdot z\right)}}{t - a \cdot z}
\] |
remove-double-neg [<=]52.7 | \[ \frac{\color{blue}{\left(-\left(-x\right)\right)} + \left(-y \cdot z\right)}{t - a \cdot z}
\] |
distribute-neg-in [<=]52.7 | \[ \frac{\color{blue}{-\left(\left(-x\right) + y \cdot z\right)}}{t - a \cdot z}
\] |
+-commutative [<=]52.7 | \[ \frac{-\color{blue}{\left(y \cdot z + \left(-x\right)\right)}}{t - a \cdot z}
\] |
sub-neg [<=]52.7 | \[ \frac{-\color{blue}{\left(y \cdot z - x\right)}}{t - a \cdot z}
\] |
neg-mul-1 [=>]52.7 | \[ \frac{\color{blue}{-1 \cdot \left(y \cdot z - x\right)}}{t - a \cdot z}
\] |
sub-neg [=>]52.7 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{t + \left(-a \cdot z\right)}}
\] |
remove-double-neg [<=]52.7 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{\left(-\left(-t\right)\right)} + \left(-a \cdot z\right)}
\] |
distribute-neg-in [<=]52.7 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{-\left(\left(-t\right) + a \cdot z\right)}}
\] |
+-commutative [<=]52.7 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{-\color{blue}{\left(a \cdot z + \left(-t\right)\right)}}
\] |
sub-neg [<=]52.7 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{-\color{blue}{\left(a \cdot z - t\right)}}
\] |
neg-mul-1 [=>]52.7 | \[ \frac{-1 \cdot \left(y \cdot z - x\right)}{\color{blue}{-1 \cdot \left(a \cdot z - t\right)}}
\] |
times-frac [=>]52.7 | \[ \color{blue}{\frac{-1}{-1} \cdot \frac{y \cdot z - x}{a \cdot z - t}}
\] |
metadata-eval [=>]52.7 | \[ \color{blue}{1} \cdot \frac{y \cdot z - x}{a \cdot z - t}
\] |
*-lft-identity [=>]52.7 | \[ \color{blue}{\frac{y \cdot z - x}{a \cdot z - t}}
\] |
*-commutative [=>]52.7 | \[ \frac{y \cdot z - x}{\color{blue}{z \cdot a} - t}
\] |
Applied egg-rr52.7
Taylor expanded in y around inf 60.4
Simplified8.1
[Start]60.4 | \[ \frac{y \cdot z}{a \cdot z - t}
\] |
|---|---|
*-commutative [<=]60.4 | \[ \frac{\color{blue}{z \cdot y}}{a \cdot z - t}
\] |
*-commutative [<=]60.4 | \[ \frac{z \cdot y}{\color{blue}{z \cdot a} - t}
\] |
associate-*l/ [<=]8.1 | \[ \color{blue}{\frac{z}{z \cdot a - t} \cdot y}
\] |
*-commutative [=>]8.1 | \[ \color{blue}{y \cdot \frac{z}{z \cdot a - t}}
\] |
*-commutative [=>]8.1 | \[ y \cdot \frac{z}{\color{blue}{a \cdot z} - t}
\] |
if +inf.0 < (/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (*.f64 a z))) Initial 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}
\] |
Taylor expanded in z around inf 0.2
Final simplification4.1
| Alternative 1 | |
|---|---|
| Error | 4.1 |
| Cost | 2892 |
| Alternative 2 | |
|---|---|
| Error | 37.7 |
| Cost | 1968 |
| Alternative 3 | |
|---|---|
| Error | 37.7 |
| Cost | 1968 |
| Alternative 4 | |
|---|---|
| Error | 30.4 |
| Cost | 1769 |
| Alternative 5 | |
|---|---|
| Error | 21.5 |
| Cost | 1632 |
| Alternative 6 | |
|---|---|
| Error | 21.5 |
| Cost | 1632 |
| Alternative 7 | |
|---|---|
| Error | 21.6 |
| Cost | 1632 |
| Alternative 8 | |
|---|---|
| Error | 22.1 |
| Cost | 1632 |
| Alternative 9 | |
|---|---|
| Error | 21.6 |
| Cost | 1632 |
| Alternative 10 | |
|---|---|
| Error | 19.4 |
| Cost | 1368 |
| Alternative 11 | |
|---|---|
| Error | 19.4 |
| Cost | 1368 |
| Alternative 12 | |
|---|---|
| Error | 27.5 |
| Cost | 1241 |
| Alternative 13 | |
|---|---|
| Error | 20.0 |
| Cost | 978 |
| Alternative 14 | |
|---|---|
| Error | 30.7 |
| Cost | 780 |
| Alternative 15 | |
|---|---|
| Error | 30.5 |
| Cost | 457 |
| Alternative 16 | |
|---|---|
| Error | 42.5 |
| Cost | 192 |
herbie shell --seed 2023060
(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))))