00001
00002
00003
00004
00005
00006
00007
00008
00009
00010 #ifndef __UTIL_MAPOFSETS_H__
00011 #define __UTIL_MAPOFSETS_H__
00012
00013 #include <cassert>
00014 #include <vector>
00015 #include <set>
00016 #include <map>
00017
00018
00019
00020
00021
00022
00023
00024
00025 namespace klee {
00026
00029 template<class K, class V>
00030 class MapOfSets {
00031 public:
00032 class iterator;
00033
00034 public:
00035 MapOfSets();
00036
00037 void clear();
00038
00039 void insert(const std::set<K> &set, const V &value);
00040
00041 V *lookup(const std::set<K> &set);
00042
00043 iterator begin();
00044 iterator end();
00045
00046 void subsets(const std::set<K> &set,
00047 std::vector< std::pair<std::set<K>, V> > &resultOut);
00048 void supersets(const std::set<K> &set,
00049 std::vector< std::pair<std::set<K>, V> > &resultOut);
00050
00051 template<class Predicate>
00052 V *findSuperset(const std::set<K> &set, const Predicate &p);
00053 template<class Predicate>
00054 V *findSubset(const std::set<K> &set, const Predicate &p);
00055
00056 private:
00057 class Node;
00058
00059 Node root;
00060
00061 template<class Iterator, class Vector>
00062 void findSubsets(Node *n,
00063 const std::set<K> &accum,
00064 Iterator begin,
00065 Iterator end,
00066 Vector &resultsOut);
00067 template<class Iterator, class Vector>
00068 void findSupersets(Node *n,
00069 const std::set<K> &accum,
00070 Iterator begin,
00071 Iterator end,
00072 Vector &resultsOut);
00073 template<class Predicate>
00074 V *findSuperset(Node *n,
00075 typename std::set<K>::iterator begin,
00076 typename std::set<K>::iterator end,
00077 const Predicate &p);
00078 template<class Predicate>
00079 V *findSubset(Node *n,
00080 typename std::set<K>::iterator begin,
00081 typename std::set<K>::iterator end,
00082 const Predicate &p);
00083 };
00084
00085
00086
00087 template<class K, class V>
00088 class MapOfSets<K,V>::Node {
00089 friend class MapOfSets<K,V>;
00090 friend class MapOfSets<K,V>::iterator;
00091
00092 public:
00093 typedef std::map<K, Node> children_ty;
00094
00095 V value;
00096
00097 private:
00098 bool isEndOfSet;
00099 std::map<K, Node> children;
00100
00101 public:
00102 Node() : isEndOfSet(false) {}
00103 };
00104
00105 template<class K, class V>
00106 class MapOfSets<K,V>::iterator {
00107 typedef std::vector< typename std::map<K, Node>::iterator > stack_ty;
00108 friend class MapOfSets<K,V>;
00109 private:
00110 Node *root;
00111 bool onEntry;
00112 stack_ty stack;
00113
00114 void step() {
00115 if (onEntry) {
00116 onEntry = false;
00117 Node *n = stack.empty() ? root : &stack.back()->second;
00118 while (!n->children.empty()) {
00119 stack.push_back(n->children.begin());
00120 n = &stack.back()->second;
00121 if (n->isEndOfSet) {
00122 onEntry = true;
00123 return;
00124 }
00125 }
00126 }
00127
00128 while (!stack.empty()) {
00129 unsigned size = stack.size();
00130 Node *at = size==1 ? root : &stack[size-2]->second;
00131 typename std::map<K,Node>::iterator &cur = stack.back();
00132 ++cur;
00133 if (cur==at->children.end()) {
00134 stack.pop_back();
00135 } else {
00136 Node *n = &cur->second;
00137
00138 while (!n->isEndOfSet) {
00139 assert(!n->children.empty());
00140 stack.push_back(n->children.begin());
00141 n = &stack.back()->second;
00142 }
00143
00144 onEntry = true;
00145 break;
00146 }
00147 }
00148 }
00149
00150 public:
00151
00152 iterator() : onEntry(false) {}
00153
00154 iterator(Node *_n) : root(_n), onEntry(true) {
00155 if (!root->isEndOfSet)
00156 step();
00157 }
00158
00159 const std::pair<const std::set<K>, const V> operator*() {
00160 assert(onEntry || !stack.empty());
00161 std::set<K> s;
00162 for (typename stack_ty::iterator it = stack.begin(), ie = stack.end();
00163 it != ie; ++it)
00164 s.insert((*it)->first);
00165 Node *n = stack.empty() ? root : &stack.back()->second;
00166 return std::make_pair(s, n->value);
00167 }
00168
00169 bool operator==(const iterator &b) {
00170 return onEntry==b.onEntry && stack==b.stack;
00171 }
00172 bool operator!=(const iterator &b) {
00173 return !(*this==b);
00174 }
00175
00176 iterator &operator++() {
00177 step();
00178 return *this;
00179 }
00180 };
00181
00182
00183
00184 template<class K, class V>
00185 MapOfSets<K,V>::MapOfSets() {}
00186
00187 template<class K, class V>
00188 void MapOfSets<K,V>::insert(const std::set<K> &set, const V &value) {
00189 Node *n = &root;
00190 for (typename std::set<K>::const_iterator it = set.begin(), ie = set.end();
00191 it != ie; ++it)
00192 n = &n->children.insert(std::make_pair(*it, Node())).first->second;
00193 n->isEndOfSet = true;
00194 n->value = value;
00195 }
00196
00197 template<class K, class V>
00198 V *MapOfSets<K,V>::lookup(const std::set<K> &set) {
00199 Node *n = &root;
00200 for (typename std::set<K>::const_iterator it = set.begin(), ie = set.end();
00201 it != ie; ++it) {
00202 typename Node::children_ty::iterator kit = n->children.find(*it);
00203 if (kit==n->children.end()) {
00204 return 0;
00205 } else {
00206 n = &kit->second;
00207 }
00208 }
00209 if (n->isEndOfSet) {
00210 return &n->value;
00211 } else {
00212 return 0;
00213 }
00214 }
00215
00216 template<class K, class V>
00217 typename MapOfSets<K,V>::iterator
00218 MapOfSets<K,V>::begin() { return iterator(&root); }
00219
00220 template<class K, class V>
00221 typename MapOfSets<K,V>::iterator
00222 MapOfSets<K,V>::end() { return iterator(); }
00223
00224 template<class K, class V>
00225 template<class Iterator, class Vector>
00226 void MapOfSets<K,V>::findSubsets(Node *n,
00227 const std::set<K> &accum,
00228 Iterator begin,
00229 Iterator end,
00230 Vector &resultsOut) {
00231 if (n->isEndOfSet) {
00232 resultsOut.push_back(std::make_pair(accum, n->value));
00233 }
00234
00235 for (Iterator it=begin; it!=end;) {
00236 K elt = *it;
00237 typename Node::children_ty::iterator kit = n->children.find(elt);
00238 it++;
00239 if (kit!=n->children.end()) {
00240 std::set<K> nacc = accum;
00241 nacc.insert(elt);
00242 findSubsets(&kit->second, nacc, it, end, resultsOut);
00243 }
00244 }
00245 }
00246
00247 template<class K, class V>
00248 void MapOfSets<K,V>::subsets(const std::set<K> &set,
00249 std::vector< std::pair<std::set<K>,
00250 V> > &resultOut) {
00251 findSubsets(&root, std::set<K>(), set.begin(), set.end(), resultOut);
00252 }
00253
00254 template<class K, class V>
00255 template<class Iterator, class Vector>
00256 void MapOfSets<K,V>::findSupersets(Node *n,
00257 const std::set<K> &accum,
00258 Iterator begin,
00259 Iterator end,
00260 Vector &resultsOut) {
00261 if (begin==end) {
00262 if (n->isEndOfSet)
00263 resultsOut.push_back(std::make_pair(accum, n->value));
00264 for (typename Node::children_ty::iterator it = n->children.begin(),
00265 ie = n->children.end(); it != ie; ++it) {
00266 std::set<K> nacc = accum;
00267 nacc.insert(it->first);
00268 findSupersets(&it->second, nacc, begin, end, resultsOut);
00269 }
00270 } else {
00271 K elt = *begin;
00272 Iterator next = begin;
00273 ++next;
00274 for (typename Node::children_ty::iterator it = n->children.begin(),
00275 ie = n->children.end(); it != ie; ++it) {
00276 std::set<K> nacc = accum;
00277 nacc.insert(it->first);
00278 if (elt==it->first) {
00279 findSupersets(&it->second, nacc, next, end, resultsOut);
00280 } else if (it->first<elt) {
00281 findSupersets(&it->second, nacc, begin, end, resultsOut);
00282 } else {
00283 break;
00284 }
00285 }
00286 }
00287 }
00288
00289 template<class K, class V>
00290 void MapOfSets<K,V>::supersets(const std::set<K> &set,
00291 std::vector< std::pair<std::set<K>, V> > &resultOut) {
00292 findSupersets(&root, std::set<K>(), set.begin(), set.end(), resultOut);
00293 }
00294
00295 template<class K, class V>
00296 template<class Predicate>
00297 V *MapOfSets<K,V>::findSubset(Node *n,
00298 typename std::set<K>::iterator begin,
00299 typename std::set<K>::iterator end,
00300 const Predicate &p) {
00301 if (n->isEndOfSet && p(n->value)) {
00302 return &n->value;
00303 } else if (begin==end) {
00304 return 0;
00305 } else {
00306 typename Node::children_ty::iterator kend = n->children.end();
00307 typename Node::children_ty::iterator
00308 kbegin = n->children.lower_bound(*begin);
00309 typename std::set<K>::iterator it = begin;
00310 if (kbegin==kend)
00311 return 0;
00312 for (;;) {
00313 while (*it < kbegin->first) {
00314 ++it;
00315 if (it==end)
00316 return 0;
00317 }
00318 if (*it == kbegin->first) {
00319 ++it;
00320 V *res = findSubset(&kbegin->second, it, end, p);
00321 if (res || it==end)
00322 return res;
00323 }
00324 while (kbegin->first < *it) {
00325 ++kbegin;
00326 if (kbegin==kend)
00327 return 0;
00328 }
00329 }
00330 }
00331 }
00332
00333 template<class K, class V>
00334 template<class Predicate>
00335 V *MapOfSets<K,V>::findSuperset(Node *n,
00336 typename std::set<K>::iterator begin,
00337 typename std::set<K>::iterator end,
00338 const Predicate &p) {
00339 if (begin==end) {
00340 if (n->isEndOfSet && p(n->value))
00341 return &n->value;
00342 for (typename Node::children_ty::iterator it = n->children.begin(),
00343 ie = n->children.end(); it != ie; ++it) {
00344 V *res = findSuperset(&it->second, begin, end, p);
00345 if (res) return res;
00346 }
00347 } else {
00348 typename Node::children_ty::iterator kbegin = n->children.begin();
00349 typename Node::children_ty::iterator kmid =
00350 n->children.lower_bound(*begin);
00351 for (typename Node::children_ty::iterator it = n->children.begin(),
00352 ie = n->children.end(); it != ie; ++it) {
00353 V *res = findSuperset(&it->second, begin, end, p);
00354 if (res) return res;
00355 }
00356 if (kmid!=n->children.end() && *begin==kmid->first) {
00357 V *res = findSuperset(&kmid->second, ++begin, end, p);
00358 if (res) return res;
00359 }
00360 }
00361 return 0;
00362 }
00363
00364 template<class K, class V>
00365 template<class Predicate>
00366 V *MapOfSets<K,V>::findSuperset(const std::set<K> &set, const Predicate &p) {
00367 return findSuperset(&root, set.begin(), set.end(), p);
00368 }
00369
00370 template<class K, class V>
00371 template<class Predicate>
00372 V *MapOfSets<K,V>::findSubset(const std::set<K> &set, const Predicate &p) {
00373 return findSubset(&root, set.begin(), set.end(), p);
00374 }
00375
00376 template<class K, class V>
00377 void MapOfSets<K,V>::clear() {
00378 root.isEndOfSet = false;
00379 root.value = V();
00380 root.children.clear();
00381 }
00382
00383 }
00384
00385 #endif