00001
00002
00003
00004
00005
00006
00007
00008
00009
00010 #ifndef __UTIL_IMMUTABLETREE_H__
00011 #define __UTIL_IMMUTABLETREE_H__
00012
00013 #include <cassert>
00014 #include <vector>
00015
00016 namespace klee {
00017 template<class K, class V, class KOV, class CMP>
00018 class ImmutableTree {
00019 public:
00020 static unsigned allocated;
00021 class iterator;
00022
00023 typedef K key_type;
00024 typedef V value_type;
00025 typedef KOV key_of_value;
00026 typedef CMP key_compare;
00027
00028 public:
00029 ImmutableTree();
00030 ImmutableTree(const ImmutableTree &s);
00031 ~ImmutableTree();
00032
00033 ImmutableTree &operator=(const ImmutableTree &s);
00034
00035 bool empty() const;
00036
00037 unsigned count(const key_type &key) const;
00038 const value_type *lookup(const key_type &key) const;
00039
00040
00041
00042 const value_type *lookup_previous(const key_type &key) const;
00043
00044 const value_type &min() const;
00045 const value_type &max() const;
00046 unsigned size() const;
00047
00048 ImmutableTree insert(const value_type &value) const;
00049 ImmutableTree replace(const value_type &value) const;
00050 ImmutableTree remove(const key_type &key) const;
00051 ImmutableTree popMin(value_type &valueOut) const;
00052 ImmutableTree popMax(value_type &valueOut) const;
00053
00054 iterator begin() const;
00055 iterator end() const;
00056 iterator find(const key_type &key) const;
00057 iterator lower_bound(const key_type &key) const;
00058 iterator upper_bound(const key_type &key) const;
00059
00060 static unsigned getAllocated() { return allocated; }
00061
00062 private:
00063 class Node;
00064
00065 Node *node;
00066 ImmutableTree(Node *_node);
00067 };
00068
00069
00070
00071 template<class K, class V, class KOV, class CMP>
00072 class ImmutableTree<K,V,KOV,CMP>::Node {
00073 public:
00074 static Node terminator;
00075 Node *left, *right;
00076 value_type value;
00077 unsigned height, references;
00078
00079 protected:
00080 Node();
00081 static Node *balance(Node *left, const value_type &value, Node *right);
00082
00083 public:
00084
00085 Node(Node *_left, Node *_right, const value_type &_value);
00086 ~Node();
00087
00088 void decref();
00089 Node *incref();
00090
00091 bool isTerminator();
00092
00093 unsigned size();
00094 Node *popMin(value_type &valueOut);
00095 Node *popMax(value_type &valueOut);
00096 Node *insert(const value_type &v);
00097 Node *replace(const value_type &v);
00098 Node *remove(const key_type &k);
00099 };
00100
00101
00102 template<typename T>
00103 class FixedStack {
00104 unsigned pos, max;
00105 T *elts;
00106
00107 public:
00108 FixedStack(unsigned _max) : pos(0),
00109 max(_max),
00110 elts(new T[max]) {}
00111 FixedStack(const FixedStack &b) : pos(b.pos),
00112 max(b.max),
00113 elts(new T[b.max]) {
00114 std::copy(b.elts, b.elts+pos, elts);
00115 }
00116 ~FixedStack() { delete[] elts; }
00117
00118 void push_back(const T &elt) { elts[pos++] = elt; }
00119 void pop_back() { --pos; }
00120 bool empty() { return pos==0; }
00121 T &back() { return elts[pos-1]; }
00122
00123
00124 FixedStack &operator=(const FixedStack &b) {
00125 assert(max == b.max);
00126 pos = b.pos;
00127 std::copy(b.elts, b.elts+pos, elts);
00128 return *this;
00129 }
00130
00131 bool operator==(const FixedStack &b) {
00132 return (pos == b.pos &&
00133 std::equal(elts, elts+pos, b.elts));
00134 }
00135 bool operator!=(const FixedStack &b) { return !(*this==b); }
00136 };
00137
00138 template<class K, class V, class KOV, class CMP>
00139 class ImmutableTree<K,V,KOV,CMP>::iterator {
00140 friend class ImmutableTree<K,V,KOV,CMP>;
00141 private:
00142 Node *root;
00143 FixedStack<Node*> stack;
00144
00145 public:
00146 iterator(Node *_root, bool atBeginning) : root(_root->incref()),
00147 stack(root->height) {
00148 if (atBeginning) {
00149 for (Node *n=root; !n->isTerminator(); n=n->left)
00150 stack.push_back(n);
00151 }
00152 }
00153 iterator(const iterator &i) : root(i.root->incref()),
00154 stack(i.stack) {
00155 }
00156 ~iterator() {
00157 root->decref();
00158 }
00159
00160 iterator &operator=(const iterator &b) {
00161 b.root->incref();
00162 root->decref();
00163 root = b.root;
00164 stack = b.stack;
00165 return *this;
00166 }
00167
00168 const value_type &operator*() {
00169 Node *n = stack.back();
00170 return n->value;
00171 }
00172
00173 const value_type *operator->() {
00174 Node *n = stack.back();
00175 return &n->value;
00176 }
00177
00178 bool operator==(const iterator &b) {
00179 return stack==b.stack;
00180 }
00181 bool operator!=(const iterator &b) {
00182 return stack!=b.stack;
00183 }
00184
00185 iterator &operator--() {
00186 if (stack.empty()) {
00187 for (Node *n=root; !n->isTerminator(); n=n->right)
00188 stack.push_back(n);
00189 } else {
00190 Node *n = stack.back();
00191 if (n->left->isTerminator()) {
00192 for (;;) {
00193 Node *prev = n;
00194 stack.pop_back();
00195 if (stack.empty()) {
00196 break;
00197 } else {
00198 n = stack.back();
00199 if (prev==n->right)
00200 break;
00201 }
00202 }
00203 } else {
00204 stack.push_back(n->left);
00205 for (n=n->left->right; !n->isTerminator(); n=n->right)
00206 stack.push_back(n);
00207 }
00208 }
00209 return *this;
00210 }
00211
00212 iterator &operator++() {
00213 assert(!stack.empty());
00214 Node *n = stack.back();
00215 if (n->right->isTerminator()) {
00216 for (;;) {
00217 Node *prev = n;
00218 stack.pop_back();
00219 if (stack.empty()) {
00220 break;
00221 } else {
00222 n = stack.back();
00223 if (prev==n->left)
00224 break;
00225 }
00226 }
00227 } else {
00228 stack.push_back(n->right);
00229 for (n=n->right->left; !n->isTerminator(); n=n->left)
00230 stack.push_back(n);
00231 }
00232 return *this;
00233 }
00234 };
00235
00236
00237
00238 template<class K, class V, class KOV, class CMP>
00239 typename ImmutableTree<K,V,KOV,CMP>::Node
00240 ImmutableTree<K,V,KOV,CMP>::Node::terminator;
00241
00242 template<class K, class V, class KOV, class CMP>
00243 unsigned ImmutableTree<K,V,KOV,CMP>::allocated = 0;
00244
00245 template<class K, class V, class KOV, class CMP>
00246 ImmutableTree<K,V,KOV,CMP>::Node::Node()
00247 : left(&terminator),
00248 right(&terminator),
00249 height(0),
00250 references(3) {
00251 assert(this==&terminator);
00252 }
00253
00254 template<class K, class V, class KOV, class CMP>
00255 ImmutableTree<K,V,KOV,CMP>::Node::Node(Node *_left, Node *_right, const value_type &_value)
00256 : left(_left),
00257 right(_right),
00258 value(_value),
00259 height(std::max(left->height, right->height) + 1),
00260 references(1)
00261 {
00262 ++allocated;
00263 }
00264
00265 template<class K, class V, class KOV, class CMP>
00266 ImmutableTree<K,V,KOV,CMP>::Node::~Node() {
00267 left->decref();
00268 right->decref();
00269 --allocated;
00270 }
00271
00272 template<class K, class V, class KOV, class CMP>
00273 inline void ImmutableTree<K,V,KOV,CMP>::Node::decref() {
00274 --references;
00275 if (references==0) delete this;
00276 }
00277
00278 template<class K, class V, class KOV, class CMP>
00279 inline typename ImmutableTree<K,V,KOV,CMP>::Node *ImmutableTree<K,V,KOV,CMP>::Node::incref() {
00280 ++references;
00281 return this;
00282 }
00283
00284 template<class K, class V, class KOV, class CMP>
00285 inline bool ImmutableTree<K,V,KOV,CMP>::Node::isTerminator() {
00286 return this==&terminator;
00287 }
00288
00289
00290
00291 template<class K, class V, class KOV, class CMP>
00292 typename ImmutableTree<K,V,KOV,CMP>::Node *
00293 ImmutableTree<K,V,KOV,CMP>::Node::balance(Node *left, const value_type &value, Node *right) {
00294 if (left->height > right->height + 2) {
00295 Node *ll = left->left;
00296 Node *lr = left->right;
00297 if (ll->height >= lr->height) {
00298 Node *nlr = new Node(lr->incref(), right, value);
00299 Node *res = new Node(ll->incref(), nlr, left->value);
00300 left->decref();
00301 return res;
00302 } else {
00303 Node *lrl = lr->left;
00304 Node *lrr = lr->right;
00305 Node *nll = new Node(ll->incref(), lrl->incref(), left->value);
00306 Node *nlr = new Node(lrr->incref(), right, value);
00307 Node *res = new Node(nll, nlr, lr->value);
00308 left->decref();
00309 return res;
00310 }
00311 } else if (right->height > left->height + 2) {
00312 Node *rl = right->left;
00313 Node *rr = right->right;
00314 if (rr->height >= rl->height) {
00315 Node *nrl = new Node(left, rl->incref(), value);
00316 Node *res = new Node(nrl, rr->incref(), right->value);
00317 right->decref();
00318 return res;
00319 } else {
00320 Node *rll = rl->left;
00321 Node *rlr = rl->right;
00322 Node *nrl = new Node(left, rll->incref(), value);
00323 Node *nrr = new Node(rlr->incref(), rr->incref(), right->value);
00324 Node *res = new Node(nrl, nrr, rl->value);
00325 right->decref();
00326 return res;
00327 }
00328 } else {
00329 return new Node(left, right, value);
00330 }
00331 }
00332
00333 template<class K, class V, class KOV, class CMP>
00334 unsigned ImmutableTree<K,V,KOV,CMP>::Node::size() {
00335 if (isTerminator()) {
00336 return 0;
00337 } else {
00338 return left->size() + 1 + right->size();
00339 }
00340 }
00341
00342 template<class K, class V, class KOV, class CMP>
00343 typename ImmutableTree<K,V,KOV,CMP>::Node *
00344 ImmutableTree<K,V,KOV,CMP>::Node::popMin(value_type &valueOut) {
00345 if (left->isTerminator()) {
00346 valueOut = value;
00347 return right->incref();
00348 } else {
00349 return balance(left->popMin(valueOut), value, right->incref());
00350 }
00351 }
00352
00353 template<class K, class V, class KOV, class CMP>
00354 typename ImmutableTree<K,V,KOV,CMP>::Node *
00355 ImmutableTree<K,V,KOV,CMP>::Node::popMax(value_type &valueOut) {
00356 if (right->isTerminator()) {
00357 valueOut = value;
00358 return left->incref();
00359 } else {
00360 return balance(left->incref(), value, right->popMax(valueOut));
00361 }
00362 }
00363
00364 template<class K, class V, class KOV, class CMP>
00365 typename ImmutableTree<K,V,KOV,CMP>::Node *
00366 ImmutableTree<K,V,KOV,CMP>::Node::insert(const value_type &v) {
00367 if (isTerminator()) {
00368 return new Node(terminator.incref(), terminator.incref(), v);
00369 } else {
00370 if (key_compare()(key_of_value()(v), key_of_value()(value))) {
00371 return balance(left->insert(v), value, right->incref());
00372 } else if (key_compare()(key_of_value()(value), key_of_value()(v))) {
00373 return balance(left->incref(), value, right->insert(v));
00374 } else {
00375 return incref();
00376 }
00377 }
00378 }
00379
00380 template<class K, class V, class KOV, class CMP>
00381 typename ImmutableTree<K,V,KOV,CMP>::Node *
00382 ImmutableTree<K,V,KOV,CMP>::Node::replace(const value_type &v) {
00383 if (isTerminator()) {
00384 return new Node(terminator.incref(), terminator.incref(), v);
00385 } else {
00386 if (key_compare()(key_of_value()(v), key_of_value()(value))) {
00387 return balance(left->replace(v), value, right->incref());
00388 } else if (key_compare()(key_of_value()(value), key_of_value()(v))) {
00389 return balance(left->incref(), value, right->replace(v));
00390 } else {
00391 return new Node(left->incref(), right->incref(), v);
00392 }
00393 }
00394 }
00395
00396 template<class K, class V, class KOV, class CMP>
00397 typename ImmutableTree<K,V,KOV,CMP>::Node *
00398 ImmutableTree<K,V,KOV,CMP>::Node::remove(const key_type &k) {
00399 if (isTerminator()) {
00400 return incref();
00401 } else {
00402 if (key_compare()(k, key_of_value()(value))) {
00403 return balance(left->remove(k), value, right->incref());
00404 } else if (key_compare()(key_of_value()(value), k)) {
00405 return balance(left->incref(), value, right->remove(k));
00406 } else {
00407 if (left->isTerminator()) {
00408 return right->incref();
00409 } else if (right->isTerminator()) {
00410 return left->incref();
00411 } else {
00412 value_type min;
00413 Node *nr = right->popMin(min);
00414 return balance(left->incref(), min, nr);
00415 }
00416 }
00417 }
00418 }
00419
00420
00421
00422 template<class K, class V, class KOV, class CMP>
00423 ImmutableTree<K,V,KOV,CMP>::ImmutableTree()
00424 : node(Node::terminator.incref()) {
00425 }
00426
00427 template<class K, class V, class KOV, class CMP>
00428 ImmutableTree<K,V,KOV,CMP>::ImmutableTree(Node *_node)
00429 : node(_node) {
00430 }
00431
00432 template<class K, class V, class KOV, class CMP>
00433 ImmutableTree<K,V,KOV,CMP>::ImmutableTree(const ImmutableTree &s)
00434 : node(s.node->incref()) {
00435 }
00436
00437 template<class K, class V, class KOV, class CMP>
00438 ImmutableTree<K,V,KOV,CMP>::~ImmutableTree() {
00439 node->decref();
00440 }
00441
00442 template<class K, class V, class KOV, class CMP>
00443 ImmutableTree<K,V,KOV,CMP> &ImmutableTree<K,V,KOV,CMP>::operator=(const ImmutableTree &s) {
00444 Node *n = s.node->incref();
00445 node->decref();
00446 node = n;
00447 return *this;
00448 }
00449
00450 template<class K, class V, class KOV, class CMP>
00451 bool ImmutableTree<K,V,KOV,CMP>::empty() const {
00452 return node->isTerminator();
00453 }
00454
00455 template<class K, class V, class KOV, class CMP>
00456 unsigned ImmutableTree<K,V,KOV,CMP>::count(const key_type &k) const {
00457 Node *n = node;
00458 while (!n->isTerminator()) {
00459 key_type key = key_of_value()(n->value);
00460 if (key_compare()(k, key)) {
00461 n = n->left;
00462 } else if (key_compare()(key, k)) {
00463 n = n->right;
00464 } else {
00465 return 1;
00466 }
00467 }
00468 return 0;
00469 }
00470
00471 template<class K, class V, class KOV, class CMP>
00472 const typename ImmutableTree<K,V,KOV,CMP>::value_type *
00473 ImmutableTree<K,V,KOV,CMP>::lookup(const key_type &k) const {
00474 Node *n = node;
00475 while (!n->isTerminator()) {
00476 key_type key = key_of_value()(n->value);
00477 if (key_compare()(k, key)) {
00478 n = n->left;
00479 } else if (key_compare()(key, k)) {
00480 n = n->right;
00481 } else {
00482 return &n->value;
00483 }
00484 }
00485 return 0;
00486 }
00487
00488 template<class K, class V, class KOV, class CMP>
00489 const typename ImmutableTree<K,V,KOV,CMP>::value_type *
00490 ImmutableTree<K,V,KOV,CMP>::lookup_previous(const key_type &k) const {
00491 Node *n = node;
00492 Node *result = 0;
00493 while (!n->isTerminator()) {
00494 key_type key = key_of_value()(n->value);
00495 if (key_compare()(k, key)) {
00496 n = n->left;
00497 } else if (key_compare()(key, k)) {
00498 result = n;
00499 n = n->right;
00500 } else {
00501 return &n->value;
00502 }
00503 }
00504 return result ? &result->value : 0;
00505 }
00506
00507 template<class K, class V, class KOV, class CMP>
00508 const typename ImmutableTree<K,V,KOV,CMP>::value_type &
00509 ImmutableTree<K,V,KOV,CMP>::min() const {
00510 Node *n = node;
00511 assert(!n->isTerminator());
00512 while (!n->left->isTerminator()) n = n->left;
00513 return n->value;
00514 }
00515
00516 template<class K, class V, class KOV, class CMP>
00517 const typename ImmutableTree<K,V,KOV,CMP>::value_type &
00518 ImmutableTree<K,V,KOV,CMP>::max() const {
00519 Node *n = node;
00520 assert(!n->isTerminator());
00521 while (!n->right->isTerminator()) n = n->right;
00522 return n->value;
00523 }
00524
00525 template<class K, class V, class KOV, class CMP>
00526 unsigned ImmutableTree<K,V,KOV,CMP>::size() const {
00527 return node->size();
00528 }
00529
00530 template<class K, class V, class KOV, class CMP>
00531 ImmutableTree<K,V,KOV,CMP>
00532 ImmutableTree<K,V,KOV,CMP>::insert(const value_type &value) const {
00533 return ImmutableTree(node->insert(value));
00534 }
00535
00536 template<class K, class V, class KOV, class CMP>
00537 ImmutableTree<K,V,KOV,CMP>
00538 ImmutableTree<K,V,KOV,CMP>::replace(const value_type &value) const {
00539 return ImmutableTree(node->replace(value));
00540 }
00541
00542 template<class K, class V, class KOV, class CMP>
00543 ImmutableTree<K,V,KOV,CMP>
00544 ImmutableTree<K,V,KOV,CMP>::remove(const key_type &key) const {
00545 return ImmutableTree(node->remove(key));
00546 }
00547
00548 template<class K, class V, class KOV, class CMP>
00549 ImmutableTree<K,V,KOV,CMP>
00550 ImmutableTree<K,V,KOV,CMP>::popMin(value_type &valueOut) const {
00551 return ImmutableTree(node->popMin(valueOut));
00552 }
00553
00554 template<class K, class V, class KOV, class CMP>
00555 ImmutableTree<K,V,KOV,CMP>
00556 ImmutableTree<K,V,KOV,CMP>::popMax(value_type &valueOut) const {
00557 return ImmutableTree(node->popMax(valueOut));
00558 }
00559
00560 template<class K, class V, class KOV, class CMP>
00561 inline typename ImmutableTree<K,V,KOV,CMP>::iterator
00562 ImmutableTree<K,V,KOV,CMP>::begin() const {
00563 return iterator(node, true);
00564 }
00565
00566 template<class K, class V, class KOV, class CMP>
00567 inline typename ImmutableTree<K,V,KOV,CMP>::iterator
00568 ImmutableTree<K,V,KOV,CMP>::end() const {
00569 return iterator(node, false);
00570 }
00571
00572 template<class K, class V, class KOV, class CMP>
00573 inline typename ImmutableTree<K,V,KOV,CMP>::iterator
00574 ImmutableTree<K,V,KOV,CMP>::find(const key_type &key) const {
00575 iterator end(node,false), it = lower_bound(key);
00576 if (it==end || key_compare()(key,key_of_value()(*it))) {
00577 return end;
00578 } else {
00579 return it;
00580 }
00581 }
00582
00583 template<class K, class V, class KOV, class CMP>
00584 inline typename ImmutableTree<K,V,KOV,CMP>::iterator
00585 ImmutableTree<K,V,KOV,CMP>::lower_bound(const key_type &k) const {
00586
00587 iterator it(node,false);
00588 for (Node *root=node; !root->isTerminator();) {
00589 it.stack.push_back(root);
00590 if (key_compare()(k, key_of_value()(root->value))) {
00591 root = root->left;
00592 } else if (key_compare()(key_of_value()(root->value), k)) {
00593 root = root->right;
00594 } else {
00595 return it;
00596 }
00597 }
00598
00599 if (!it.stack.empty()) {
00600 Node *last = it.stack.back();
00601 if (key_compare()(key_of_value()(last->value), k))
00602 ++it;
00603 }
00604 return it;
00605 }
00606
00607 template<class K, class V, class KOV, class CMP>
00608 typename ImmutableTree<K,V,KOV,CMP>::iterator
00609 ImmutableTree<K,V,KOV,CMP>::upper_bound(const key_type &key) const {
00610 iterator end(node,false),it = lower_bound(key);
00611 if (it!=end &&
00612 !key_compare()(key,key_of_value()(*it)))
00613 ++it;
00614 return it;
00615 }
00616
00617 }
00618
00619 #endif