| Alternative 1 | |
|---|---|
| Accuracy | 97.9% |
| Cost | 704 |
\[\frac{\frac{v}{t1 + u}}{-1 - \frac{u}{t1}}
\]

(FPCore (u v t1) :precision binary64 (/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))
(FPCore (u v t1) :precision binary64 (/ (/ v (+ t1 u)) (- -1.0 (/ u t1))))
double code(double u, double v, double t1) {
return (-t1 * v) / ((t1 + u) * (t1 + u));
}
double code(double u, double v, double t1) {
return (v / (t1 + u)) / (-1.0 - (u / t1));
}
real(8) function code(u, v, t1)
real(8), intent (in) :: u
real(8), intent (in) :: v
real(8), intent (in) :: t1
code = (-t1 * v) / ((t1 + u) * (t1 + u))
end function
real(8) function code(u, v, t1)
real(8), intent (in) :: u
real(8), intent (in) :: v
real(8), intent (in) :: t1
code = (v / (t1 + u)) / ((-1.0d0) - (u / t1))
end function
public static double code(double u, double v, double t1) {
return (-t1 * v) / ((t1 + u) * (t1 + u));
}
public static double code(double u, double v, double t1) {
return (v / (t1 + u)) / (-1.0 - (u / t1));
}
def code(u, v, t1): return (-t1 * v) / ((t1 + u) * (t1 + u))
def code(u, v, t1): return (v / (t1 + u)) / (-1.0 - (u / t1))
function code(u, v, t1) return Float64(Float64(Float64(-t1) * v) / Float64(Float64(t1 + u) * Float64(t1 + u))) end
function code(u, v, t1) return Float64(Float64(v / Float64(t1 + u)) / Float64(-1.0 - Float64(u / t1))) end
function tmp = code(u, v, t1) tmp = (-t1 * v) / ((t1 + u) * (t1 + u)); end
function tmp = code(u, v, t1) tmp = (v / (t1 + u)) / (-1.0 - (u / t1)); end
code[u_, v_, t1_] := N[(N[((-t1) * v), $MachinePrecision] / N[(N[(t1 + u), $MachinePrecision] * N[(t1 + u), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
code[u_, v_, t1_] := N[(N[(v / N[(t1 + u), $MachinePrecision]), $MachinePrecision] / N[(-1.0 - N[(u / t1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}
\frac{\frac{v}{t1 + u}}{-1 - \frac{u}{t1}}
Herbie found 9 alternatives:
| Alternative | Accuracy | Speedup |
|---|
Results
Initial program 75.1%
Simplified99.2%
[Start]75.1% | \[ \frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}
\] |
|---|---|
*-commutative [=>]75.1% | \[ \frac{\color{blue}{v \cdot \left(-t1\right)}}{\left(t1 + u\right) \cdot \left(t1 + u\right)}
\] |
times-frac [=>]99.2% | \[ \color{blue}{\frac{v}{t1 + u} \cdot \frac{-t1}{t1 + u}}
\] |
neg-mul-1 [=>]99.2% | \[ \frac{v}{t1 + u} \cdot \frac{\color{blue}{-1 \cdot t1}}{t1 + u}
\] |
associate-/l* [=>]99.2% | \[ \frac{v}{t1 + u} \cdot \color{blue}{\frac{-1}{\frac{t1 + u}{t1}}}
\] |
associate-*r/ [=>]99.2% | \[ \color{blue}{\frac{\frac{v}{t1 + u} \cdot -1}{\frac{t1 + u}{t1}}}
\] |
associate-/l* [=>]99.2% | \[ \color{blue}{\frac{\frac{v}{t1 + u}}{\frac{\frac{t1 + u}{t1}}{-1}}}
\] |
associate-/l/ [=>]99.2% | \[ \frac{\frac{v}{t1 + u}}{\color{blue}{\frac{t1 + u}{-1 \cdot t1}}}
\] |
neg-mul-1 [<=]99.2% | \[ \frac{\frac{v}{t1 + u}}{\frac{t1 + u}{\color{blue}{-t1}}}
\] |
*-lft-identity [<=]99.2% | \[ \frac{\frac{v}{t1 + u}}{\color{blue}{1 \cdot \frac{t1 + u}{-t1}}}
\] |
metadata-eval [<=]99.2% | \[ \frac{\frac{v}{t1 + u}}{\color{blue}{\frac{-1}{-1}} \cdot \frac{t1 + u}{-t1}}
\] |
times-frac [<=]99.2% | \[ \frac{\frac{v}{t1 + u}}{\color{blue}{\frac{-1 \cdot \left(t1 + u\right)}{-1 \cdot \left(-t1\right)}}}
\] |
neg-mul-1 [<=]99.2% | \[ \frac{\frac{v}{t1 + u}}{\frac{-1 \cdot \left(t1 + u\right)}{\color{blue}{-\left(-t1\right)}}}
\] |
remove-double-neg [=>]99.2% | \[ \frac{\frac{v}{t1 + u}}{\frac{-1 \cdot \left(t1 + u\right)}{\color{blue}{t1}}}
\] |
neg-mul-1 [<=]99.2% | \[ \frac{\frac{v}{t1 + u}}{\frac{\color{blue}{-\left(t1 + u\right)}}{t1}}
\] |
sub0-neg [<=]99.2% | \[ \frac{\frac{v}{t1 + u}}{\frac{\color{blue}{0 - \left(t1 + u\right)}}{t1}}
\] |
associate--r+ [=>]99.2% | \[ \frac{\frac{v}{t1 + u}}{\frac{\color{blue}{\left(0 - t1\right) - u}}{t1}}
\] |
neg-sub0 [<=]99.2% | \[ \frac{\frac{v}{t1 + u}}{\frac{\color{blue}{\left(-t1\right)} - u}{t1}}
\] |
div-sub [=>]99.2% | \[ \frac{\frac{v}{t1 + u}}{\color{blue}{\frac{-t1}{t1} - \frac{u}{t1}}}
\] |
distribute-frac-neg [=>]99.2% | \[ \frac{\frac{v}{t1 + u}}{\color{blue}{\left(-\frac{t1}{t1}\right)} - \frac{u}{t1}}
\] |
*-inverses [=>]99.2% | \[ \frac{\frac{v}{t1 + u}}{\left(-\color{blue}{1}\right) - \frac{u}{t1}}
\] |
metadata-eval [=>]99.2% | \[ \frac{\frac{v}{t1 + u}}{\color{blue}{-1} - \frac{u}{t1}}
\] |
Final simplification99.2%
| Alternative 1 | |
|---|---|
| Accuracy | 97.9% |
| Cost | 704 |
| Alternative 2 | |
|---|---|
| Accuracy | 78.0% |
| Cost | 1042 |
| Alternative 3 | |
|---|---|
| Accuracy | 77.3% |
| Cost | 1040 |
| Alternative 4 | |
|---|---|
| Accuracy | 77.4% |
| Cost | 1040 |
| Alternative 5 | |
|---|---|
| Accuracy | 76.8% |
| Cost | 777 |
| Alternative 6 | |
|---|---|
| Accuracy | 68.6% |
| Cost | 713 |
| Alternative 7 | |
|---|---|
| Accuracy | 58.4% |
| Cost | 521 |
| Alternative 8 | |
|---|---|
| Accuracy | 61.5% |
| Cost | 384 |
| Alternative 9 | |
|---|---|
| Accuracy | 53.9% |
| Cost | 256 |
herbie shell --seed 2023178
(FPCore (u v t1)
:name "Rosa's DopplerBench"
:precision binary64
(/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))