00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042
00043
00044
00045
00046
00047
00048
00049
00050 #ifndef _cvc3__hash__hash_table_h_
00051 #define _cvc3__hash__hash_table_h_
00052
00053 #include <vector>
00054 #include <string>
00055 #include <functional>
00056 #include <algorithm>
00057 #include "hash_fun.h"
00058 #include "os.h"
00059
00060
00061
00062 #ifdef _CVC3_DEBUG_MODE
00063 #define DebugAssert(cond, str) if(!(cond)) \
00064 CVC3::debugError(__FILE__, __LINE__, #cond, str)
00065 namespace CVC3 {
00066 extern CVC_DLL void debugError(const std::string& file, int line,
00067 const std::string& cond, const std::string& msg);
00068 }
00069 #else
00070 #define DebugAssert(cond, str)
00071 #endif
00072
00073 namespace Hash {
00074
00075 typedef size_t size_type;
00076
00077
00078
00079
00080 const size_type num_primes = 28;
00081
00082 static const size_type prime_list[num_primes] = {
00083 53ul, 97ul, 193ul, 389ul, 769ul,
00084 1543ul, 3079ul, 6151ul, 12289ul, 24593ul,
00085 49157ul, 98317ul, 196613ul, 393241ul, 786433ul,
00086 1572869ul, 3145739ul, 6291469ul, 12582917ul, 25165843ul,
00087 50331653ul, 100663319ul, 201326611ul, 402653189ul, 805306457ul,
00088 1610612741ul, 3221225473ul, 4294967291ul
00089 };
00090
00091 inline size_type next_prime(size_type n)
00092 {
00093 const size_type* first = prime_list;
00094 const size_type* last = prime_list + (size_type)num_primes;
00095 const size_type* pos = std::lower_bound(first, last, n);
00096 return pos == last ? *(last - 1) : *pos;
00097 }
00098
00099
00100
00101
00102
00103
00104
00105
00106
00107
00108
00109
00110
00111
00112
00113
00114
00115
00116
00117
00118
00119 template <class _Key, class _Value,
00120 class _HashFcn, class _EqualKey, class _ExtractKey>
00121 class hash_table {
00122
00123
00124
00125 public:
00126
00127 typedef Hash::size_type size_type;
00128 typedef _Key key_type;
00129 typedef _Value value_type;
00130 typedef _HashFcn hasher;
00131 typedef _EqualKey key_equal;
00132
00133 protected:
00134
00135
00136
00137
00138
00139
00140 struct BucketNode {
00141 BucketNode(BucketNode* next, const value_type& value)
00142 : d_next(next), d_value(value)
00143 { };
00144 BucketNode* d_next;
00145 value_type d_value;
00146 };
00147 typedef BucketNode Bucket;
00148
00149
00150 typedef std::vector<Bucket*> Data;
00151 typedef typename Data::iterator data_iter;
00152 typedef typename Data::const_iterator data_const_iter;
00153
00154
00155 public:
00156
00157 class iterator;
00158 friend class iterator;
00159 class const_iterator;
00160 friend class const_iterator;
00161
00162
00163
00164
00165
00166 protected:
00167
00168
00169
00170 hasher d_hash;
00171
00172
00173 key_equal d_equal;
00174
00175
00176 _ExtractKey d_extractKey;
00177
00178
00179
00180 size_type d_size;
00181
00182
00183 Data d_data;
00184
00185
00186
00187
00188 protected:
00189
00190
00191
00192
00193
00194 size_type hash(const key_type& key) const {
00195 return d_hash(key);
00196 }
00197
00198
00199 bool equal(const key_type& key1, const key_type& key2) const {
00200 return d_equal(key1, key2);
00201 }
00202
00203
00204 const key_type& extractKey(const value_type& value) const {
00205 return d_extractKey(value);
00206 }
00207
00208
00209
00210
00211
00212
00213 size_type getBucketIndex(const key_type& key) const {
00214 return (hash(key) % d_data.size());
00215 }
00216
00217 Bucket* getBucketByKey(const key_type& key) {
00218 return getBucketByIndex(getBucketIndex(key));
00219 }
00220
00221 const Bucket* getBucketByKey(const key_type& key) const {
00222 return getBucketByIndex(getBucketIndex(key));
00223 }
00224
00225 Bucket* getBucketByIndex(const size_type index) {
00226 DebugAssert(index < d_data.size(),"hash_table::getBucketByIndex");
00227 return d_data.at(index);
00228 }
00229
00230 const Bucket* getBucketByIndex(const size_type index) const {
00231 DebugAssert(index < d_data.size(),"hash_table::getBucketByIndex (const)");
00232 return d_data.at(index);
00233 }
00234
00235
00236
00237
00238
00239
00240 void resize() {
00241 if (load_factor() > 1) {
00242
00243
00244
00245
00246
00247 size_type size = next_prime(d_data.size() + 1);
00248 Data copy(size, NULL);
00249
00250
00251 for (size_type i = 0; i < d_data.size(); ++i) {
00252
00253 BucketNode* bucket = d_data[i];
00254 while (bucket != NULL) {
00255
00256 BucketNode* current = bucket;
00257 bucket = bucket->d_next;
00258
00259
00260 size_type new_index = hash(extractKey(current->d_value)) % size;
00261 BucketNode* new_bucket = copy[new_index];
00262 current->d_next = new_bucket;
00263 copy[new_index] = current;
00264 }
00265 d_data[i] = NULL;
00266 }
00267
00268 d_data.swap(copy);
00269 }
00270 }
00271
00272
00273 public:
00274
00275
00276
00277 hash_table() :
00278 d_hash(_HashFcn()), d_equal(_EqualKey()), d_extractKey(_ExtractKey()),
00279 d_size(0), d_data(16)
00280 {
00281 init();
00282 };
00283
00284
00285 hash_table(size_type initial_capacity) :
00286 d_hash(_HashFcn()), d_equal(_EqualKey()), d_extractKey(_ExtractKey()),
00287 d_size(0), d_data(initial_capacity)
00288 {
00289 init();
00290 };
00291
00292
00293 hash_table(size_type initial_capacity, const _HashFcn& hash) :
00294 d_hash(hash), d_equal(_EqualKey()), d_extractKey(_ExtractKey()),
00295 d_size(0), d_data(initial_capacity)
00296 {
00297 init();
00298 };
00299
00300
00301 hash_table(size_type initial_capacity,
00302 const _HashFcn& hash, const _EqualKey& equal) :
00303 d_hash(hash), d_equal(equal), d_extractKey(_ExtractKey()),
00304 d_size(0), d_data(initial_capacity)
00305 {
00306 init();
00307 };
00308
00309
00310 hash_table(const hash_table& other) :
00311 d_hash(other.d_hash), d_equal(other.d_equal), d_extractKey(other.d_extractKey),
00312 d_size(other.d_size), d_data(0)
00313 {
00314 assignTable(other.d_data);
00315 };
00316
00317 ~hash_table() {
00318 clear();
00319 }
00320
00321
00322 hash_table& operator=(const hash_table& other) {
00323 if (this != &other) {
00324 clear();
00325
00326 d_hash = other.d_hash;
00327 d_equal = other.d_equal;
00328 d_extractKey = other.d_extractKey;
00329 d_size = other.d_size;
00330 assignTable(other.d_data);
00331 }
00332
00333 return *this;
00334 }
00335
00336
00337
00338 void assignTable(const Data& data) {
00339
00340
00341
00342
00343
00344 Data tmp(data.size());
00345 d_data.swap(tmp);
00346
00347
00348 for (size_type i = 0; i < data.size(); ++i) {
00349
00350 DebugAssert(i < d_data.size(),"hash_table::operator=");
00351
00352
00353 Bucket* source = data[i];
00354 if (source != NULL) {
00355
00356 Bucket* target = new BucketNode(NULL, source->d_value);
00357 d_data[i] = target;
00358 source = source->d_next;
00359
00360
00361 while (source != NULL) {
00362 target->d_next = new BucketNode(NULL, source->d_value);
00363 target = target->d_next;
00364 source = source->d_next;
00365 }
00366 }
00367 }
00368 }
00369
00370 void swap(hash_table& other) {
00371 std::swap(d_hash, other.d_hash);
00372 std::swap(d_equal, other.d_equal);
00373 std::swap(d_extractKey, other.d_extractKey);
00374 std::swap(d_size, other.d_size);
00375 d_data.swap(other.d_data);
00376 }
00377
00378
00379 void init() {
00380 for (size_type i = 0; i < d_data.size(); ++i) {
00381 d_data[i] = NULL;
00382 }
00383 }
00384
00385
00386 void clear() {
00387 d_size = 0;
00388
00389 for (size_type i = 0; i < d_data.size(); ++i) {
00390 BucketNode* head = d_data[i];
00391 while (head != NULL) {
00392 BucketNode* next = head->d_next;
00393 delete head;
00394 head = next;
00395 }
00396 d_data[i] = NULL;
00397 }
00398 }
00399
00400
00401
00402
00403
00404
00405
00406 iterator find(const key_type& key) {
00407 for (BucketNode* node = getBucketByKey(key); node != NULL; node = node->d_next) {
00408 if (equal(extractKey(node->d_value), key)) {
00409 return iterator(this, node);
00410 }
00411 }
00412 return end();
00413 }
00414
00415
00416 const_iterator find(const key_type& key) const {
00417 for (const BucketNode* node = getBucketByKey(key); node != NULL; node = node->d_next) {
00418 if (equal(extractKey(node->d_value), key)) {
00419 return const_iterator(this, node);
00420 }
00421 }
00422 return end();
00423 }
00424
00425
00426
00427
00428 std::pair<iterator, bool> insert(const value_type& value) {
00429
00430 resize();
00431
00432 const key_type& key = extractKey(value);
00433 size_type index = getBucketIndex(key);
00434
00435
00436 for (BucketNode* node = d_data[index]; node != NULL; node = node->d_next) {
00437 if (equal(extractKey(node->d_value), key)) {
00438 return std::make_pair(end(), false);
00439 }
00440 }
00441
00442
00443 ++d_size;
00444 d_data[index] = new BucketNode(d_data[index], value);
00445 return std::make_pair(iterator(this, d_data[index]), true);
00446 }
00447
00448
00449
00450
00451 value_type& find_or_insert(const value_type& value) {
00452
00453 resize();
00454
00455 const key_type& key = extractKey(value);
00456 size_type index = getBucketIndex(key);
00457
00458
00459 for (BucketNode* node = d_data[index]; node != NULL; node = node->d_next) {
00460 if (equal(extractKey(node->d_value), key)) {
00461 return node->d_value;
00462 }
00463 }
00464
00465
00466 ++d_size;
00467 d_data[index] = new BucketNode(d_data[index], value);
00468 return d_data[index]->d_value;
00469 }
00470
00471
00472
00473
00474
00475 size_type erase(const key_type& key) {
00476 size_type index = getBucketIndex(key);
00477
00478
00479 BucketNode* prev = NULL;
00480 for (BucketNode* node = d_data[index]; node != NULL; node = node->d_next) {
00481 if (equal(extractKey(node->d_value), key)) {
00482 --d_size;
00483
00484
00485 if (prev == NULL) {
00486 d_data[index] = node->d_next;
00487 }
00488
00489 else {
00490 prev->d_next = node->d_next;
00491 }
00492 delete node;
00493 return 1;
00494 }
00495
00496 prev = node;
00497 }
00498
00499 return 0;
00500 }
00501
00502
00503
00504 const_iterator erase(const const_iterator& iter) {
00505 const_iterator next(iter);
00506 ++next;
00507
00508 const key_type& key = extractKey(*iter);
00509 size_type index = getBucketIndex(key);
00510
00511
00512 BucketNode* prev = NULL;
00513 for (BucketNode* node = d_data[index]; node != NULL; node = node->d_next) {
00514 if (equal(extractKey(node->d_value), key)) {
00515 --d_size;
00516
00517
00518 if (prev == NULL) {
00519 d_data[index] = node->d_next;
00520 }
00521
00522 else {
00523 prev->d_next = node->d_next;
00524 }
00525 delete node;
00526 return next;
00527 }
00528
00529 prev = node;
00530 }
00531
00532 return next;
00533 }
00534
00535
00536
00537
00538
00539 bool contains(const key_type& key) const {
00540 return (find(key) != end());
00541 }
00542
00543
00544
00545 size_type count(const _Key& key) const {
00546 if (contains(key)) {
00547 return 1;
00548 }
00549 else {
00550 return 0;
00551 }
00552 }
00553
00554
00555 bool empty() const {
00556 return (d_size == 0);
00557 }
00558
00559
00560 size_type size() const {
00561 return d_size;
00562 }
00563
00564
00565 size_type bucket_count() const {
00566 return d_data.size();
00567 }
00568
00569
00570 float load_factor() const {
00571 return (float(d_size) / float(d_data.size()));
00572 }
00573
00574
00575
00576
00577
00578
00579 iterator begin() {
00580 if (d_size > 0) {
00581
00582 size_type index = 0;
00583 while (d_data[index] == NULL) {
00584 ++index;
00585 }
00586
00587 return iterator(this, d_data[index]);
00588 }
00589 else {
00590 return end();
00591 }
00592 }
00593
00594
00595 const_iterator begin() const {
00596 if (d_size > 0) {
00597
00598 size_type index = 0;
00599 while (d_data[index] == NULL) {
00600 ++index;
00601 }
00602
00603 return const_iterator(this, d_data[index]);
00604 }
00605 else {
00606 return end();
00607 }
00608 }
00609
00610
00611
00612 iterator end() {
00613 return iterator(this, NULL);
00614 }
00615
00616
00617 const_iterator end() const {
00618 return const_iterator(this, NULL);
00619 }
00620
00621
00622
00623
00624
00625
00626
00627
00628
00629
00630
00631
00632
00633 class iterator {
00634 friend class hash_table;
00635 friend class const_iterator;
00636
00637
00638
00639 protected:
00640
00641 hash_table* d_hash_table;
00642
00643 BucketNode* d_node;
00644
00645
00646
00647 protected:
00648
00649 iterator(hash_table* hash_table, BucketNode* node)
00650 : d_hash_table(hash_table), d_node(node)
00651 { }
00652
00653 public:
00654
00655
00656 iterator()
00657 : d_hash_table(NULL), d_node(NULL)
00658 { }
00659
00660
00661 iterator(const iterator& other)
00662 : d_hash_table(other.d_hash_table), d_node(other.d_node)
00663 { }
00664
00665
00666 iterator& operator=(const iterator& other) {
00667 if (this != &other) {
00668 d_hash_table = other.d_hash_table;
00669 d_node = other.d_node;
00670 }
00671
00672 return *this;
00673 }
00674
00675
00676 iterator& operator++() {
00677
00678 DebugAssert(d_node != NULL, "hash operator++");
00679
00680
00681 size_type index = d_hash_table->getBucketIndex(d_hash_table->extractKey(d_node->d_value));
00682
00683
00684 d_node = d_node->d_next;
00685
00686
00687 while (d_node == NULL) {
00688
00689 ++index;
00690
00691
00692 if (index == d_hash_table->d_data.size()) {
00693
00694
00695 *this = d_hash_table->end();
00696 return *this;
00697 }
00698 DebugAssert(index < d_hash_table->d_data.size(),
00699 "hash operator++ 2");
00700
00701 d_node = d_hash_table->getBucketByIndex(index);
00702 }
00703
00704 return *this;
00705 };
00706
00707
00708 iterator operator++(int) {
00709 iterator tmp = *this;
00710 ++(*this);
00711 return tmp;
00712 }
00713
00714 value_type& operator*() const {
00715 return d_node->d_value;
00716 }
00717
00718 value_type* operator->() const {
00719 return &(operator*());
00720 }
00721
00722
00723 bool operator==(const iterator& other) const {
00724
00725 DebugAssert(d_node == NULL || d_node != other.d_node || d_hash_table == other.d_hash_table, "hash operator==");
00726 return (d_node == other.d_node);
00727 }
00728
00729
00730 bool operator!=(const iterator& other) const {
00731 return !(*this == other);
00732 }
00733 };
00734
00735
00736
00737
00738
00739
00740
00741
00742 class const_iterator {
00743 friend class hash_table;
00744
00745
00746
00747 protected:
00748
00749 const hash_table* d_hash_table;
00750
00751 const BucketNode* d_node;
00752
00753
00754
00755 protected:
00756
00757 const_iterator(hash_table const* hash_table, const BucketNode* node)
00758 : d_hash_table(hash_table), d_node(node)
00759 { }
00760
00761 public:
00762
00763
00764 const_iterator()
00765 : d_hash_table(NULL), d_node(NULL)
00766 { }
00767
00768
00769 const_iterator(const const_iterator& other)
00770 : d_hash_table(other.d_hash_table), d_node(other.d_node)
00771 { }
00772
00773
00774 const_iterator(const iterator& other)
00775 : d_hash_table(other.d_hash_table), d_node(other.d_node)
00776 { }
00777
00778
00779 const_iterator& operator=(const const_iterator& other) {
00780 if (this != &other) {
00781 d_hash_table = other.d_hash_table;
00782 d_node = other.d_node;
00783 }
00784
00785 return *this;
00786 }
00787
00788
00789 const_iterator& operator++() {
00790
00791 DebugAssert(d_node != NULL, "");
00792
00793
00794 size_type index = d_hash_table->getBucketIndex(d_hash_table->extractKey(d_node->d_value));
00795
00796
00797 d_node = d_node->d_next;
00798
00799
00800 while (d_node == NULL) {
00801
00802 ++index;
00803
00804
00805 if (index == d_hash_table->d_data.size()) {
00806
00807
00808 *this = d_hash_table->end();
00809 return *this;
00810 }
00811 DebugAssert(index < d_hash_table->d_data.size(),"");
00812
00813 d_node = d_hash_table->getBucketByIndex(index);
00814 }
00815
00816 return *this;
00817 };
00818
00819
00820 const_iterator operator++(int) {
00821 const_iterator tmp = *this;
00822 ++(*this);
00823 return tmp;
00824 }
00825
00826 const value_type& operator*() const {
00827 return d_node->d_value;
00828 }
00829
00830 const value_type* operator->() const {
00831 return &(operator*());
00832 }
00833
00834
00835 bool operator==(const const_iterator& other) const {
00836
00837 DebugAssert(d_node == NULL || d_node != other.d_node || d_hash_table == other.d_hash_table,"");
00838 return (d_node == other.d_node);
00839 }
00840
00841
00842 bool operator!=(const const_iterator& other) const {
00843 return !(*this == other);
00844 }
00845 };
00846 };
00847
00848 }
00849
00850 #endif