| Alternative 1 | |
|---|---|
| Accuracy | 89.3% |
| Cost | 3020 |
(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 (<= t_1 0.0))
(t_3 (- (* z a) t)))
(if t_2
t_1
(if t_2
(/ y (- a (/ t z)))
(if (<= t_1 INFINITY) (- (/ y (/ t_3 z)) (/ x t_3)) (/ 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));
int t_2 = t_1 <= 0.0;
double t_3 = (z * a) - t;
double tmp;
if (t_2) {
tmp = t_1;
} else if (t_2) {
tmp = y / (a - (t / z));
} else if (t_1 <= ((double) INFINITY)) {
tmp = (y / (t_3 / z)) - (x / t_3);
} 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 = (x - (y * z)) / (t - (z * a));
boolean t_2 = t_1 <= 0.0;
double t_3 = (z * a) - t;
double tmp;
if (t_2) {
tmp = t_1;
} else if (t_2) {
tmp = y / (a - (t / z));
} else if (t_1 <= Double.POSITIVE_INFINITY) {
tmp = (y / (t_3 / z)) - (x / t_3);
} 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 = (x - (y * z)) / (t - (z * a)) t_2 = t_1 <= 0.0 t_3 = (z * a) - t tmp = 0 if t_2: tmp = t_1 elif t_2: tmp = y / (a - (t / z)) elif t_1 <= math.inf: tmp = (y / (t_3 / z)) - (x / t_3) 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 = t_1 <= 0.0 t_3 = Float64(Float64(z * a) - t) tmp = 0.0 if (t_2) tmp = t_1; elseif (t_2) tmp = Float64(y / Float64(a - Float64(t / z))); elseif (t_1 <= Inf) tmp = Float64(Float64(y / Float64(t_3 / z)) - Float64(x / t_3)); 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 = (x - (y * z)) / (t - (z * a)); t_2 = t_1 <= 0.0; t_3 = (z * a) - t; tmp = 0.0; if (t_2) tmp = t_1; elseif (t_2) tmp = y / (a - (t / z)); elseif (t_1 <= Inf) tmp = (y / (t_3 / z)) - (x / t_3); 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[(x - N[(y * z), $MachinePrecision]), $MachinePrecision] / N[(t - N[(z * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = LessEqual[t$95$1, 0.0]}, Block[{t$95$3 = N[(N[(z * a), $MachinePrecision] - t), $MachinePrecision]}, If[t$95$2, t$95$1, If[t$95$2, N[(y / N[(a - N[(t / z), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$1, Infinity], N[(N[(y / N[(t$95$3 / z), $MachinePrecision]), $MachinePrecision] - N[(x / t$95$3), $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 := t_1 \leq 0\\
t_3 := z \cdot a - t\\
\mathbf{if}\;t_2:\\
\;\;\;\;t_1\\
\mathbf{elif}\;t_2:\\
\;\;\;\;\frac{y}{a - \frac{t}{z}}\\
\mathbf{elif}\;t_1 \leq \infty:\\
\;\;\;\;\frac{y}{\frac{t_3}{z}} - \frac{x}{t_3}\\
\mathbf{else}:\\
\;\;\;\;\frac{y}{a}\\
\end{array}
Results
| Original | 85.1% |
|---|---|
| Target | 97.2% |
| Herbie | 90.9% |
if (/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (*.f64 a z))) < 0.0Initial program 87.3%
if 0.0 < (/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (*.f64 a z))) < -0.0Initial program 83.7%
Simplified83.7%
[Start]83.7 | \[ \frac{x - y \cdot z}{t - a \cdot z}
\] |
|---|---|
sub-neg [=>]83.7 | \[ \frac{x - y \cdot z}{\color{blue}{t + \left(-a \cdot z\right)}}
\] |
+-commutative [=>]83.7 | \[ \frac{x - y \cdot z}{\color{blue}{\left(-a \cdot z\right) + t}}
\] |
neg-sub0 [=>]83.7 | \[ \frac{x - y \cdot z}{\color{blue}{\left(0 - a \cdot z\right)} + t}
\] |
associate-+l- [=>]83.7 | \[ \frac{x - y \cdot z}{\color{blue}{0 - \left(a \cdot z - t\right)}}
\] |
sub0-neg [=>]83.7 | \[ \frac{x - y \cdot z}{\color{blue}{-\left(a \cdot z - t\right)}}
\] |
neg-mul-1 [=>]83.7 | \[ \frac{x - y \cdot z}{\color{blue}{-1 \cdot \left(a \cdot z - t\right)}}
\] |
sub-neg [=>]83.7 | \[ \frac{\color{blue}{x + \left(-y \cdot z\right)}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
+-commutative [=>]83.7 | \[ \frac{\color{blue}{\left(-y \cdot z\right) + x}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
neg-sub0 [=>]83.7 | \[ \frac{\color{blue}{\left(0 - y \cdot z\right)} + x}{-1 \cdot \left(a \cdot z - t\right)}
\] |
associate-+l- [=>]83.7 | \[ \frac{\color{blue}{0 - \left(y \cdot z - x\right)}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
sub0-neg [=>]83.7 | \[ \frac{\color{blue}{-\left(y \cdot z - x\right)}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
neg-mul-1 [=>]83.7 | \[ \frac{\color{blue}{-1 \cdot \left(y \cdot z - x\right)}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
times-frac [=>]83.7 | \[ \color{blue}{\frac{-1}{-1} \cdot \frac{y \cdot z - x}{a \cdot z - t}}
\] |
metadata-eval [=>]83.7 | \[ \color{blue}{1} \cdot \frac{y \cdot z - x}{a \cdot z - t}
\] |
*-lft-identity [=>]83.7 | \[ \color{blue}{\frac{y \cdot z - x}{a \cdot z - t}}
\] |
*-commutative [=>]83.7 | \[ \frac{y \cdot z - x}{\color{blue}{z \cdot a} - t}
\] |
Taylor expanded in y around inf 43.7%
Simplified45.7%
[Start]43.7 | \[ \frac{y \cdot z}{a \cdot z - t}
\] |
|---|---|
*-commutative [=>]43.7 | \[ \frac{y \cdot z}{\color{blue}{z \cdot a} - t}
\] |
associate-*r/ [<=]45.7 | \[ \color{blue}{y \cdot \frac{z}{z \cdot a - t}}
\] |
*-commutative [<=]45.7 | \[ y \cdot \frac{z}{\color{blue}{a \cdot z} - t}
\] |
Applied egg-rr45.8%
[Start]45.7 | \[ y \cdot \frac{z}{a \cdot z - t}
\] |
|---|---|
clear-num [=>]45.7 | \[ y \cdot \color{blue}{\frac{1}{\frac{a \cdot z - t}{z}}}
\] |
un-div-inv [=>]45.8 | \[ \color{blue}{\frac{y}{\frac{a \cdot z - t}{z}}}
\] |
*-commutative [=>]45.8 | \[ \frac{y}{\frac{\color{blue}{z \cdot a} - t}{z}}
\] |
Taylor expanded in z around 0 56.1%
Simplified56.1%
[Start]56.1 | \[ \frac{y}{a + -1 \cdot \frac{t}{z}}
\] |
|---|---|
neg-mul-1 [<=]56.1 | \[ \frac{y}{a + \color{blue}{\left(-\frac{t}{z}\right)}}
\] |
sub-neg [<=]56.1 | \[ \frac{y}{\color{blue}{a - \frac{t}{z}}}
\] |
if -0.0 < (/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (*.f64 a z))) < +inf.0Initial program 92.4%
Simplified92.4%
[Start]92.4 | \[ \frac{x - y \cdot z}{t - a \cdot z}
\] |
|---|---|
sub-neg [=>]92.4 | \[ \frac{x - y \cdot z}{\color{blue}{t + \left(-a \cdot z\right)}}
\] |
+-commutative [=>]92.4 | \[ \frac{x - y \cdot z}{\color{blue}{\left(-a \cdot z\right) + t}}
\] |
neg-sub0 [=>]92.4 | \[ \frac{x - y \cdot z}{\color{blue}{\left(0 - a \cdot z\right)} + t}
\] |
associate-+l- [=>]92.4 | \[ \frac{x - y \cdot z}{\color{blue}{0 - \left(a \cdot z - t\right)}}
\] |
sub0-neg [=>]92.4 | \[ \frac{x - y \cdot z}{\color{blue}{-\left(a \cdot z - t\right)}}
\] |
neg-mul-1 [=>]92.4 | \[ \frac{x - y \cdot z}{\color{blue}{-1 \cdot \left(a \cdot z - t\right)}}
\] |
sub-neg [=>]92.4 | \[ \frac{\color{blue}{x + \left(-y \cdot z\right)}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
+-commutative [=>]92.4 | \[ \frac{\color{blue}{\left(-y \cdot z\right) + x}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
neg-sub0 [=>]92.4 | \[ \frac{\color{blue}{\left(0 - y \cdot z\right)} + x}{-1 \cdot \left(a \cdot z - t\right)}
\] |
associate-+l- [=>]92.4 | \[ \frac{\color{blue}{0 - \left(y \cdot z - x\right)}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
sub0-neg [=>]92.4 | \[ \frac{\color{blue}{-\left(y \cdot z - x\right)}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
neg-mul-1 [=>]92.4 | \[ \frac{\color{blue}{-1 \cdot \left(y \cdot z - x\right)}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
times-frac [=>]92.4 | \[ \color{blue}{\frac{-1}{-1} \cdot \frac{y \cdot z - x}{a \cdot z - t}}
\] |
metadata-eval [=>]92.4 | \[ \color{blue}{1} \cdot \frac{y \cdot z - x}{a \cdot z - t}
\] |
*-lft-identity [=>]92.4 | \[ \color{blue}{\frac{y \cdot z - x}{a \cdot z - t}}
\] |
*-commutative [=>]92.4 | \[ \frac{y \cdot z - x}{\color{blue}{z \cdot a} - t}
\] |
Applied egg-rr97.6%
[Start]92.4 | \[ \frac{y \cdot z - x}{z \cdot a - t}
\] |
|---|---|
div-sub [=>]91.3 | \[ \color{blue}{\frac{y \cdot z}{z \cdot a - t} - \frac{x}{z \cdot a - t}}
\] |
associate-/l* [=>]97.6 | \[ \color{blue}{\frac{y}{\frac{z \cdot a - t}{z}}} - \frac{x}{z \cdot a - t}
\] |
if +inf.0 < (/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (*.f64 a z))) Initial program 0.0%
Simplified0.0%
[Start]0.0 | \[ \frac{x - y \cdot z}{t - a \cdot z}
\] |
|---|---|
sub-neg [=>]0.0 | \[ \frac{x - y \cdot z}{\color{blue}{t + \left(-a \cdot z\right)}}
\] |
+-commutative [=>]0.0 | \[ \frac{x - y \cdot z}{\color{blue}{\left(-a \cdot z\right) + t}}
\] |
neg-sub0 [=>]0.0 | \[ \frac{x - y \cdot z}{\color{blue}{\left(0 - a \cdot z\right)} + t}
\] |
associate-+l- [=>]0.0 | \[ \frac{x - y \cdot z}{\color{blue}{0 - \left(a \cdot z - t\right)}}
\] |
sub0-neg [=>]0.0 | \[ \frac{x - y \cdot z}{\color{blue}{-\left(a \cdot z - t\right)}}
\] |
neg-mul-1 [=>]0.0 | \[ \frac{x - y \cdot z}{\color{blue}{-1 \cdot \left(a \cdot z - t\right)}}
\] |
sub-neg [=>]0.0 | \[ \frac{\color{blue}{x + \left(-y \cdot z\right)}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
+-commutative [=>]0.0 | \[ \frac{\color{blue}{\left(-y \cdot z\right) + x}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
neg-sub0 [=>]0.0 | \[ \frac{\color{blue}{\left(0 - y \cdot z\right)} + x}{-1 \cdot \left(a \cdot z - t\right)}
\] |
associate-+l- [=>]0.0 | \[ \frac{\color{blue}{0 - \left(y \cdot z - x\right)}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
sub0-neg [=>]0.0 | \[ \frac{\color{blue}{-\left(y \cdot z - x\right)}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
neg-mul-1 [=>]0.0 | \[ \frac{\color{blue}{-1 \cdot \left(y \cdot z - x\right)}}{-1 \cdot \left(a \cdot z - t\right)}
\] |
times-frac [=>]0.0 | \[ \color{blue}{\frac{-1}{-1} \cdot \frac{y \cdot z - x}{a \cdot z - t}}
\] |
metadata-eval [=>]0.0 | \[ \color{blue}{1} \cdot \frac{y \cdot z - x}{a \cdot z - t}
\] |
*-lft-identity [=>]0.0 | \[ \color{blue}{\frac{y \cdot z - x}{a \cdot z - t}}
\] |
*-commutative [=>]0.0 | \[ \frac{y \cdot z - x}{\color{blue}{z \cdot a} - t}
\] |
Taylor expanded in z around inf 100.0%
Final simplification91.8%
| Alternative 1 | |
|---|---|
| Accuracy | 89.3% |
| Cost | 3020 |
| Alternative 2 | |
|---|---|
| Accuracy | 52.9% |
| Cost | 1108 |
| Alternative 3 | |
|---|---|
| Accuracy | 52.9% |
| Cost | 1040 |
| Alternative 4 | |
|---|---|
| Accuracy | 52.9% |
| Cost | 1040 |
| Alternative 5 | |
|---|---|
| Accuracy | 52.9% |
| Cost | 1040 |
| Alternative 6 | |
|---|---|
| Accuracy | 35.0% |
| Cost | 912 |
| Alternative 7 | |
|---|---|
| Accuracy | 35.0% |
| Cost | 912 |
| Alternative 8 | |
|---|---|
| Accuracy | 35.0% |
| Cost | 912 |
| Alternative 9 | |
|---|---|
| Accuracy | 53.5% |
| Cost | 713 |
| Alternative 10 | |
|---|---|
| Accuracy | 52.5% |
| Cost | 712 |
| Alternative 11 | |
|---|---|
| Accuracy | 35.4% |
| Cost | 456 |
| Alternative 12 | |
|---|---|
| Accuracy | 35.2% |
| Cost | 192 |
herbie shell --seed 2023159
(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))))