SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Map.h
Go to the documentation of this file.
1 /*******************************************************************************************[Map.h]
2 Copyright (c) 2006-2010, Niklas Sorensson
3 
4 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
5 associated documentation files (the "Software"), to deal in the Software without restriction,
6 including without limitation the rights to use, copy, modify, merge, publish, distribute,
7 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
8 furnished to do so, subject to the following conditions:
9 
10 The above copyright notice and this permission notice shall be included in all copies or
11 substantial portions of the Software.
12 
13 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
14 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
15 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
16 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
17 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
18 **************************************************************************************************/
19 
20 #ifndef Minisat_Map_h
21 #define Minisat_Map_h
22 
23 #include "IntTypes.h"
24 #include "Vec.h"
25 
26 namespace Minisat {
27 
28 //=================================================================================================
29 // Default hash/equals functions
30 //
31 
32 static inline uint32_t hash(uint32_t x){ return x; }
33 static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
34 static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
35 static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
36 
37 template<class K> struct Hash { uint32_t operator()(const K& k) const { return hash(k); } };
38 template<class K> struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } };
39 
40 template<class K> struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } };
41 template<class K> struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } };
42 
43 
44 
45 //=================================================================================================
46 // Some primes
47 //
48 
49 static const int nprimes = 25;
50 static const int primes [nprimes] = { 31, 73, 151, 313, 643, 1291, 2593, 5233, 10501, 21013, 42073, 84181, 168451, 337219, 674701, 1349473, 2699299, 5398891, 10798093, 21596719, 43193641, 86387383, 172775299, 345550609, 691101253 };
51 
52 //=================================================================================================
53 // Hash table implementation of Maps
54 //
55 
56 template<class K, class D, class H = Hash<K>, class E = Equal<K> >
57 class Map {
58  public:
59  struct Pair { K key; D data; };
60 
61  private:
62  H hash;
63  E equals;
64 
66  int cap;
67  int size;
68 
69  // Don't allow copying (error prone):
71  Map (Map<K,D,H,E>&) { assert(0); }
72 
73  bool checkCap(int new_size) const { return new_size > cap; }
74 
75  int32_t index (const K& k) const { return hash(k) % cap; }
76  void _insert (const K& k, const D& d) {
77  vec<Pair>& ps = table[index(k)];
78  ps.push(); ps.last().key = k; ps.last().data = d; }
79 
80  void rehash () {
81  const vec<Pair>* old = table;
82 
83  int old_cap = cap;
84  int newsize = primes[0];
85  for (int i = 1; newsize <= cap && i < nprimes; i++)
86  newsize = primes[i];
87 
88  table = new vec<Pair>[newsize];
89  cap = newsize;
90 
91  for (int i = 0; i < old_cap; i++){
92  for (int j = 0; j < old[i].size(); j++){
93  _insert(old[i][j].key, old[i][j].data); }}
94 
95  delete [] old;
96 
97  // printf(" --- rehashing, old-cap=%d, new-cap=%d\n", cap, newsize);
98  }
99 
100 
101  public:
102 
103  Map () : table(NULL), cap(0), size(0) {}
104  Map (const H& h, const E& e) : hash(h), equals(e), table(NULL), cap(0), size(0){}
105  ~Map () { delete [] table; }
106 
107  // PRECONDITION: the key must already exist in the map.
108  const D& operator [] (const K& k) const
109  {
110  assert(size != 0);
111  const D* res = NULL;
112  const vec<Pair>& ps = table[index(k)];
113  for (int i = 0; i < ps.size(); i++)
114  if (equals(ps[i].key, k))
115  res = &ps[i].data;
116  assert(res != NULL);
117  return *res;
118  }
119 
120  // PRECONDITION: the key must already exist in the map.
121  D& operator [] (const K& k)
122  {
123  assert(size != 0);
124  D* res = NULL;
125  vec<Pair>& ps = table[index(k)];
126  for (int i = 0; i < ps.size(); i++)
127  if (equals(ps[i].key, k))
128  res = &ps[i].data;
129  assert(res != NULL);
130  return *res;
131  }
132 
133  // PRECONDITION: the key must *NOT* exist in the map.
134  void insert (const K& k, const D& d) { if (checkCap(size+1)) rehash(); _insert(k, d); size++; }
135  bool peek (const K& k, D& d) const {
136  if (size == 0) return false;
137  const vec<Pair>& ps = table[index(k)];
138  for (int i = 0; i < ps.size(); i++)
139  if (equals(ps[i].key, k)){
140  d = ps[i].data;
141  return true; }
142  return false;
143  }
144 
145  bool has (const K& k) const {
146  if (size == 0) return false;
147  const vec<Pair>& ps = table[index(k)];
148  for (int i = 0; i < ps.size(); i++)
149  if (equals(ps[i].key, k))
150  return true;
151  return false;
152  }
153 
154  // PRECONDITION: the key must exist in the map.
155  void remove(const K& k) {
156  assert(table != NULL);
157  vec<Pair>& ps = table[index(k)];
158  int j = 0;
159  for (; j < ps.size() && !equals(ps[j].key, k); j++);
160  assert(j < ps.size());
161  ps[j] = ps.last();
162  ps.pop();
163  size--;
164  }
165 
166  void clear () {
167  cap = size = 0;
168  delete [] table;
169  table = NULL;
170  }
171 
172  int elems() const { return size; }
173  int bucket_count() const { return cap; }
174 
175  // NOTE: the hash and equality objects are not moved by this method:
176  void moveTo(Map& other){
177  delete [] other.table;
178 
179  other.table = table;
180  other.cap = cap;
181  other.size = size;
182 
183  table = NULL;
184  size = cap = 0;
185  }
186 
187  // NOTE: given a bit more time, I could make a more C++-style iterator out of this:
188  const vec<Pair>& bucket(int i) const { return table[i]; }
189 };
190 
191 //=================================================================================================
192 }
193 
194 #endif
void insert(const K &k, const D &d)
Definition: Map.h:134
void moveTo(Map &other)
Definition: Map.h:176
int bucket_count() const
Definition: Map.h:173
~Map()
Definition: Map.h:105
Map(const H &h, const E &e)
Definition: Map.h:104
Map< K, D, H, E > & operator=(Map< K, D, H, E > &)
Definition: Map.h:70
H hash
Definition: Map.h:62
const vec< Pair > & bucket(int i) const
Definition: Map.h:188
vec< Pair > * table
Definition: Map.h:65
int32_t index(const K &k) const
Definition: Map.h:75
bool checkCap(int new_size) const
Definition: Map.h:73
void remove(const K &k)
Definition: Map.h:155
Map(Map< K, D, H, E > &)
Definition: Map.h:71
int size
Definition: Map.h:67
void rehash()
Definition: Map.h:80
int elems() const
Definition: Map.h:172
bool peek(const K &k, D &d) const
Definition: Map.h:135
void _insert(const K &k, const D &d)
Definition: Map.h:76
const D & operator[](const K &k) const
Definition: Map.h:108
bool has(const K &k) const
Definition: Map.h:145
int cap
Definition: Map.h:66
E equals
Definition: Map.h:63
void clear()
Definition: Map.h:166
int size(void) const
Definition: Vec.h:118
const T & last(void) const
Definition: Vec.h:178
T * data
Definition: Vec.h:41
void push(void)
Definition: Vec.h:147
void pop(void)
Definition: Vec.h:168
Definition: Alg.h:27
static const int primes[nprimes]
Definition: Map.h:50
static const int nprimes
Definition: Map.h:49
static uint32_t hash(uint32_t x)
Definition: Map.h:32
bool operator()(const K *k1, const K *k2) const
Definition: Map.h:41
uint32_t operator()(const K *k) const
Definition: Map.h:40
bool operator()(const K &k1, const K &k2) const
Definition: Map.h:38
uint32_t operator()(const K &k) const
Definition: Map.h:37