| Alternative 1 | |
|---|---|
| Accuracy | 97.2% |
| Cost | 3784 |

(FPCore (x y z t) :precision binary64 (/ (+ x (/ (- (* y z) x) (- (* t z) x))) (+ x 1.0)))
(FPCore (x y z t)
:precision binary64
(let* ((t_1 (- (* z t) x)) (t_2 (/ (+ x (/ (- (* y z) x) t_1)) (+ x 1.0))))
(if (<= t_2 (- INFINITY))
(/ (+ (* z (/ 1.0 (/ t_1 y))) (- x -1.0)) (+ x 1.0))
(if (<= t_2 5e+263)
t_2
(-
(+ (/ y (* t (+ x 1.0))) (/ x (+ x 1.0)))
(/ x (* (* z t) (+ x 1.0))))))))double code(double x, double y, double z, double t) {
return (x + (((y * z) - x) / ((t * z) - x))) / (x + 1.0);
}
double code(double x, double y, double z, double t) {
double t_1 = (z * t) - x;
double t_2 = (x + (((y * z) - x) / t_1)) / (x + 1.0);
double tmp;
if (t_2 <= -((double) INFINITY)) {
tmp = ((z * (1.0 / (t_1 / y))) + (x - -1.0)) / (x + 1.0);
} else if (t_2 <= 5e+263) {
tmp = t_2;
} else {
tmp = ((y / (t * (x + 1.0))) + (x / (x + 1.0))) - (x / ((z * t) * (x + 1.0)));
}
return tmp;
}
public static double code(double x, double y, double z, double t) {
return (x + (((y * z) - x) / ((t * z) - x))) / (x + 1.0);
}
public static double code(double x, double y, double z, double t) {
double t_1 = (z * t) - x;
double t_2 = (x + (((y * z) - x) / t_1)) / (x + 1.0);
double tmp;
if (t_2 <= -Double.POSITIVE_INFINITY) {
tmp = ((z * (1.0 / (t_1 / y))) + (x - -1.0)) / (x + 1.0);
} else if (t_2 <= 5e+263) {
tmp = t_2;
} else {
tmp = ((y / (t * (x + 1.0))) + (x / (x + 1.0))) - (x / ((z * t) * (x + 1.0)));
}
return tmp;
}
def code(x, y, z, t): return (x + (((y * z) - x) / ((t * z) - x))) / (x + 1.0)
def code(x, y, z, t): t_1 = (z * t) - x t_2 = (x + (((y * z) - x) / t_1)) / (x + 1.0) tmp = 0 if t_2 <= -math.inf: tmp = ((z * (1.0 / (t_1 / y))) + (x - -1.0)) / (x + 1.0) elif t_2 <= 5e+263: tmp = t_2 else: tmp = ((y / (t * (x + 1.0))) + (x / (x + 1.0))) - (x / ((z * t) * (x + 1.0))) return tmp
function code(x, y, z, t) return Float64(Float64(x + Float64(Float64(Float64(y * z) - x) / Float64(Float64(t * z) - x))) / Float64(x + 1.0)) end
function code(x, y, z, t) t_1 = Float64(Float64(z * t) - x) t_2 = Float64(Float64(x + Float64(Float64(Float64(y * z) - x) / t_1)) / Float64(x + 1.0)) tmp = 0.0 if (t_2 <= Float64(-Inf)) tmp = Float64(Float64(Float64(z * Float64(1.0 / Float64(t_1 / y))) + Float64(x - -1.0)) / Float64(x + 1.0)); elseif (t_2 <= 5e+263) tmp = t_2; else tmp = Float64(Float64(Float64(y / Float64(t * Float64(x + 1.0))) + Float64(x / Float64(x + 1.0))) - Float64(x / Float64(Float64(z * t) * Float64(x + 1.0)))); end return tmp end
function tmp = code(x, y, z, t) tmp = (x + (((y * z) - x) / ((t * z) - x))) / (x + 1.0); end
function tmp_2 = code(x, y, z, t) t_1 = (z * t) - x; t_2 = (x + (((y * z) - x) / t_1)) / (x + 1.0); tmp = 0.0; if (t_2 <= -Inf) tmp = ((z * (1.0 / (t_1 / y))) + (x - -1.0)) / (x + 1.0); elseif (t_2 <= 5e+263) tmp = t_2; else tmp = ((y / (t * (x + 1.0))) + (x / (x + 1.0))) - (x / ((z * t) * (x + 1.0))); end tmp_2 = tmp; end
code[x_, y_, z_, t_] := N[(N[(x + N[(N[(N[(y * z), $MachinePrecision] - x), $MachinePrecision] / N[(N[(t * z), $MachinePrecision] - x), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(x + 1.0), $MachinePrecision]), $MachinePrecision]
code[x_, y_, z_, t_] := Block[{t$95$1 = N[(N[(z * t), $MachinePrecision] - x), $MachinePrecision]}, Block[{t$95$2 = N[(N[(x + N[(N[(N[(y * z), $MachinePrecision] - x), $MachinePrecision] / t$95$1), $MachinePrecision]), $MachinePrecision] / N[(x + 1.0), $MachinePrecision]), $MachinePrecision]}, If[LessEqual[t$95$2, (-Infinity)], N[(N[(N[(z * N[(1.0 / N[(t$95$1 / y), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(x - -1.0), $MachinePrecision]), $MachinePrecision] / N[(x + 1.0), $MachinePrecision]), $MachinePrecision], If[LessEqual[t$95$2, 5e+263], t$95$2, N[(N[(N[(y / N[(t * N[(x + 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(x / N[(x + 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(x / N[(N[(z * t), $MachinePrecision] * N[(x + 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]]]
\frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\begin{array}{l}
t_1 := z \cdot t - x\\
t_2 := \frac{x + \frac{y \cdot z - x}{t_1}}{x + 1}\\
\mathbf{if}\;t_2 \leq -\infty:\\
\;\;\;\;\frac{z \cdot \frac{1}{\frac{t_1}{y}} + \left(x - -1\right)}{x + 1}\\
\mathbf{elif}\;t_2 \leq 5 \cdot 10^{+263}:\\
\;\;\;\;t_2\\
\mathbf{else}:\\
\;\;\;\;\left(\frac{y}{t \cdot \left(x + 1\right)} + \frac{x}{x + 1}\right) - \frac{x}{\left(z \cdot t\right) \cdot \left(x + 1\right)}\\
\end{array}
Herbie found 15 alternatives:
| Alternative | Accuracy | Speedup |
|---|
Results
| Original | 89.2% |
|---|---|
| Target | 99.5% |
| Herbie | 97.2% |
if (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1)) < -inf.0Initial program 30.0%
Simplified30.0%
[Start]30.0% | \[ \frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\] |
|---|---|
*-commutative [=>]30.0% | \[ \frac{x + \frac{y \cdot z - x}{\color{blue}{z \cdot t} - x}}{x + 1}
\] |
Applied egg-rr93.5%
[Start]30.0% | \[ \frac{x + \frac{y \cdot z - x}{z \cdot t - x}}{x + 1}
\] |
|---|---|
+-commutative [=>]30.0% | \[ \frac{\color{blue}{\frac{y \cdot z - x}{z \cdot t - x} + x}}{x + 1}
\] |
div-sub [=>]30.0% | \[ \frac{\color{blue}{\left(\frac{y \cdot z}{z \cdot t - x} - \frac{x}{z \cdot t - x}\right)} + x}{x + 1}
\] |
associate-+l- [=>]30.0% | \[ \frac{\color{blue}{\frac{y \cdot z}{z \cdot t - x} - \left(\frac{x}{z \cdot t - x} - x\right)}}{x + 1}
\] |
*-commutative [=>]30.0% | \[ \frac{\frac{\color{blue}{z \cdot y}}{z \cdot t - x} - \left(\frac{x}{z \cdot t - x} - x\right)}{x + 1}
\] |
*-un-lft-identity [=>]30.0% | \[ \frac{\frac{z \cdot y}{\color{blue}{1 \cdot \left(z \cdot t - x\right)}} - \left(\frac{x}{z \cdot t - x} - x\right)}{x + 1}
\] |
times-frac [=>]93.5% | \[ \frac{\color{blue}{\frac{z}{1} \cdot \frac{y}{z \cdot t - x}} - \left(\frac{x}{z \cdot t - x} - x\right)}{x + 1}
\] |
fma-neg [=>]93.5% | \[ \frac{\color{blue}{\mathsf{fma}\left(\frac{z}{1}, \frac{y}{z \cdot t - x}, -\left(\frac{x}{z \cdot t - x} - x\right)\right)}}{x + 1}
\] |
Simplified93.5%
[Start]93.5% | \[ \frac{\mathsf{fma}\left(\frac{z}{1}, \frac{y}{z \cdot t - x}, -\left(\frac{x}{z \cdot t - x} - x\right)\right)}{x + 1}
\] |
|---|---|
fma-udef [=>]93.5% | \[ \frac{\color{blue}{\frac{z}{1} \cdot \frac{y}{z \cdot t - x} + \left(-\left(\frac{x}{z \cdot t - x} - x\right)\right)}}{x + 1}
\] |
unsub-neg [=>]93.5% | \[ \frac{\color{blue}{\frac{z}{1} \cdot \frac{y}{z \cdot t - x} - \left(\frac{x}{z \cdot t - x} - x\right)}}{x + 1}
\] |
/-rgt-identity [=>]93.5% | \[ \frac{\color{blue}{z} \cdot \frac{y}{z \cdot t - x} - \left(\frac{x}{z \cdot t - x} - x\right)}{x + 1}
\] |
*-commutative [=>]93.5% | \[ \frac{z \cdot \frac{y}{\color{blue}{t \cdot z} - x} - \left(\frac{x}{z \cdot t - x} - x\right)}{x + 1}
\] |
*-commutative [=>]93.5% | \[ \frac{z \cdot \frac{y}{t \cdot z - x} - \left(\frac{x}{\color{blue}{t \cdot z} - x} - x\right)}{x + 1}
\] |
Applied egg-rr93.6%
[Start]93.5% | \[ \frac{z \cdot \frac{y}{t \cdot z - x} - \left(\frac{x}{t \cdot z - x} - x\right)}{x + 1}
\] |
|---|---|
clear-num [=>]93.6% | \[ \frac{z \cdot \color{blue}{\frac{1}{\frac{t \cdot z - x}{y}}} - \left(\frac{x}{t \cdot z - x} - x\right)}{x + 1}
\] |
inv-pow [=>]93.6% | \[ \frac{z \cdot \color{blue}{{\left(\frac{t \cdot z - x}{y}\right)}^{-1}} - \left(\frac{x}{t \cdot z - x} - x\right)}{x + 1}
\] |
*-commutative [=>]93.6% | \[ \frac{z \cdot {\left(\frac{\color{blue}{z \cdot t} - x}{y}\right)}^{-1} - \left(\frac{x}{t \cdot z - x} - x\right)}{x + 1}
\] |
fma-neg [=>]93.6% | \[ \frac{z \cdot {\left(\frac{\color{blue}{\mathsf{fma}\left(z, t, -x\right)}}{y}\right)}^{-1} - \left(\frac{x}{t \cdot z - x} - x\right)}{x + 1}
\] |
Simplified93.6%
[Start]93.6% | \[ \frac{z \cdot {\left(\frac{\mathsf{fma}\left(z, t, -x\right)}{y}\right)}^{-1} - \left(\frac{x}{t \cdot z - x} - x\right)}{x + 1}
\] |
|---|---|
unpow-1 [=>]93.6% | \[ \frac{z \cdot \color{blue}{\frac{1}{\frac{\mathsf{fma}\left(z, t, -x\right)}{y}}} - \left(\frac{x}{t \cdot z - x} - x\right)}{x + 1}
\] |
fma-neg [<=]93.6% | \[ \frac{z \cdot \frac{1}{\frac{\color{blue}{z \cdot t - x}}{y}} - \left(\frac{x}{t \cdot z - x} - x\right)}{x + 1}
\] |
Taylor expanded in x around inf 93.6%
if -inf.0 < (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1)) < 5.00000000000000022e263Initial program 99.3%
if 5.00000000000000022e263 < (/.f64 (+.f64 x (/.f64 (-.f64 (*.f64 y z) x) (-.f64 (*.f64 t z) x))) (+.f64 x 1)) Initial program 17.9%
Simplified17.9%
[Start]17.9% | \[ \frac{x + \frac{y \cdot z - x}{t \cdot z - x}}{x + 1}
\] |
|---|---|
*-commutative [=>]17.9% | \[ \frac{x + \frac{y \cdot z - x}{\color{blue}{z \cdot t} - x}}{x + 1}
\] |
Taylor expanded in t around inf 87.9%
Final simplification97.6%
| Alternative 1 | |
|---|---|
| Accuracy | 97.2% |
| Cost | 3784 |
| Alternative 2 | |
|---|---|
| Accuracy | 96.5% |
| Cost | 3400 |
| Alternative 3 | |
|---|---|
| Accuracy | 97.2% |
| Cost | 3400 |
| Alternative 4 | |
|---|---|
| Accuracy | 97.2% |
| Cost | 3400 |
| Alternative 5 | |
|---|---|
| Accuracy | 86.2% |
| Cost | 1488 |
| Alternative 6 | |
|---|---|
| Accuracy | 67.8% |
| Cost | 1236 |
| Alternative 7 | |
|---|---|
| Accuracy | 83.4% |
| Cost | 1234 |
| Alternative 8 | |
|---|---|
| Accuracy | 67.5% |
| Cost | 978 |
| Alternative 9 | |
|---|---|
| Accuracy | 55.7% |
| Cost | 849 |
| Alternative 10 | |
|---|---|
| Accuracy | 77.3% |
| Cost | 841 |
| Alternative 11 | |
|---|---|
| Accuracy | 77.3% |
| Cost | 840 |
| Alternative 12 | |
|---|---|
| Accuracy | 77.3% |
| Cost | 840 |
| Alternative 13 | |
|---|---|
| Accuracy | 55.6% |
| Cost | 592 |
| Alternative 14 | |
|---|---|
| Accuracy | 62.2% |
| Cost | 585 |
| Alternative 15 | |
|---|---|
| Accuracy | 54.3% |
| Cost | 64 |
herbie shell --seed 2023165
(FPCore (x y z t)
:name "Diagrams.Trail:splitAtParam from diagrams-lib-1.3.0.3, A"
:precision binary64
:herbie-target
(/ (+ x (- (/ y (- t (/ x z))) (/ x (- (* t z) x)))) (+ x 1.0))
(/ (+ x (/ (- (* y z) x) (- (* t z) x))) (+ x 1.0)))