| 433 | } |
| 434 | |
| 435 | unsigned Statistics::getAveragePivotTimeInMicro() const |
| 436 | { |
| 437 | if ( _longAttributes[NUM_TABLEAU_PIVOTS] == 0 ) |
| 438 | return 0; |
| 439 | |
| 440 | return _longAttributes[TIME_PIVOTS_MICRO] / _longAttributes[NUM_TABLEAU_PIVOTS]; |
| 441 | } |
| 442 | |
| 443 | void Statistics::timeout() |
| 444 | { |