klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ImmutableTree.h
Go to the documentation of this file.
1 //===-- ImmutableTree.h -----------------------------------------*- C++ -*-===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #ifndef __UTIL_IMMUTABLETREE_H__
11 #define __UTIL_IMMUTABLETREE_H__
12 
13 #include <cassert>
14 #include <vector>
15 
16 namespace klee {
17  template<class K, class V, class KOV, class CMP>
18  class ImmutableTree {
19  public:
20  static size_t allocated;
21  class iterator;
22 
23  typedef K key_type;
24  typedef V value_type;
25  typedef KOV key_of_value;
26  typedef CMP key_compare;
27 
28  public:
29  ImmutableTree();
30  ImmutableTree(const ImmutableTree &s);
32 
34 
35  bool empty() const;
36 
37  size_t count(const key_type &key) const; // always 0 or 1
38  const value_type *lookup(const key_type &key) const;
39 
40  // find the last value less than or equal to key, or null if
41  // no such value exists
42  const value_type *lookup_previous(const key_type &key) const;
43 
44  const value_type &min() const;
45  const value_type &max() const;
46  size_t size() const;
47 
48  ImmutableTree insert(const value_type &value) const;
49  ImmutableTree replace(const value_type &value) const;
50  ImmutableTree remove(const key_type &key) const;
51  ImmutableTree popMin(value_type &valueOut) const;
52  ImmutableTree popMax(value_type &valueOut) const;
53 
54  iterator begin() const;
55  iterator end() const;
56  iterator find(const key_type &key) const;
57  iterator lower_bound(const key_type &key) const;
58  iterator upper_bound(const key_type &key) const;
59 
60  static size_t getAllocated() { return allocated; }
61 
62  private:
63  class Node;
64 
65  Node *node;
66  ImmutableTree(Node *_node);
67  };
68 
69  /***/
70 
71  template<class K, class V, class KOV, class CMP>
72  class ImmutableTree<K,V,KOV,CMP>::Node {
73  public:
74  static Node terminator;
75  Node *left, *right;
77  unsigned height, references;
78 
79  protected:
80  Node(); // solely for creating the terminator node
81  static Node *balance(Node *left, const value_type &value, Node *right);
82 
83  public:
84 
85  Node(Node *_left, Node *_right, const value_type &_value);
86  ~Node();
87 
88  void decref();
89  Node *incref();
90 
91  bool isTerminator();
92 
93  size_t size();
94  Node *popMin(value_type &valueOut);
95  Node *popMax(value_type &valueOut);
96  Node *insert(const value_type &v);
97  Node *replace(const value_type &v);
98  Node *remove(const key_type &k);
99  };
100 
101  // Should live somewhere else, this is a simple stack with maximum (dynamic)
102  // size.
103  template<typename T>
104  class FixedStack {
105  unsigned pos, max;
106  T *elts;
107 
108  public:
109  FixedStack(unsigned _max) : pos(0),
110  max(_max),
111  elts(new T[max]) {}
112  FixedStack(const FixedStack &b) : pos(b.pos),
113  max(b.max),
114  elts(new T[b.max]) {
115  std::copy(b.elts, b.elts+pos, elts);
116  }
117  ~FixedStack() { delete[] elts; }
118 
119  void push_back(const T &elt) { elts[pos++] = elt; }
120  void pop_back() { --pos; }
121  bool empty() { return pos==0; }
122  T &back() { return elts[pos-1]; }
123 
124 
126  assert(max == b.max);
127  pos = b.pos;
128  std::copy(b.elts, b.elts+pos, elts);
129  return *this;
130  }
131 
132  bool operator==(const FixedStack &b) {
133  return (pos == b.pos &&
134  std::equal(elts, elts+pos, b.elts));
135  }
136  bool operator!=(const FixedStack &b) { return !(*this==b); }
137  };
138 
139  template<class K, class V, class KOV, class CMP>
140  class ImmutableTree<K,V,KOV,CMP>::iterator {
141  friend class ImmutableTree<K,V,KOV,CMP>;
142  private:
143  Node *root; // so can back up from end
145 
146  public:
147  iterator(Node *_root, bool atBeginning) : root(_root->incref()),
148  stack(root->height) {
149  if (atBeginning) {
150  for (Node *n=root; !n->isTerminator(); n=n->left)
151  stack.push_back(n);
152  }
153  }
154  iterator(const iterator &i) : root(i.root->incref()),
155  stack(i.stack) {
156  }
158  root->decref();
159  }
160 
162  b.root->incref();
163  root->decref();
164  root = b.root;
165  stack = b.stack;
166  return *this;
167  }
168 
170  Node *n = stack.back();
171  return n->value;
172  }
173 
175  Node *n = stack.back();
176  return &n->value;
177  }
178 
179  bool operator==(const iterator &b) {
180  return stack==b.stack;
181  }
182  bool operator!=(const iterator &b) {
183  return stack!=b.stack;
184  }
185 
187  if (stack.empty()) {
188  for (Node *n=root; !n->isTerminator(); n=n->right)
189  stack.push_back(n);
190  } else {
191  Node *n = stack.back();
192  if (n->left->isTerminator()) {
193  for (;;) {
194  Node *prev = n;
195  stack.pop_back();
196  if (stack.empty()) {
197  break;
198  } else {
199  n = stack.back();
200  if (prev==n->right)
201  break;
202  }
203  }
204  } else {
205  stack.push_back(n->left);
206  for (n=n->left->right; !n->isTerminator(); n=n->right)
207  stack.push_back(n);
208  }
209  }
210  return *this;
211  }
212 
214  assert(!stack.empty());
215  Node *n = stack.back();
216  if (n->right->isTerminator()) {
217  for (;;) {
218  Node *prev = n;
219  stack.pop_back();
220  if (stack.empty()) {
221  break;
222  } else {
223  n = stack.back();
224  if (prev==n->left)
225  break;
226  }
227  }
228  } else {
229  stack.push_back(n->right);
230  for (n=n->right->left; !n->isTerminator(); n=n->left)
231  stack.push_back(n);
232  }
233  return *this;
234  }
235  };
236 
237  /***/
238 
239  template<class K, class V, class KOV, class CMP>
242 
243  template<class K, class V, class KOV, class CMP>
245 
246  template<class K, class V, class KOV, class CMP>
248  : left(&terminator),
249  right(&terminator),
250  height(0),
251  references(3) {
252  assert(this==&terminator);
253  }
254 
255  template<class K, class V, class KOV, class CMP>
257  : left(_left),
258  right(_right),
259  value(_value),
260  height(std::max(left->height, right->height) + 1),
261  references(1)
262  {
263  ++allocated;
264  }
265 
266  template<class K, class V, class KOV, class CMP>
268  left->decref();
269  right->decref();
270  --allocated;
271  }
272 
273  template<class K, class V, class KOV, class CMP>
275  --references;
276  if (references==0) delete this;
277  }
278 
279  template<class K, class V, class KOV, class CMP>
281  ++references;
282  return this;
283  }
284 
285  template<class K, class V, class KOV, class CMP>
287  return this==&terminator;
288  }
289 
290  /***/
291 
292  template<class K, class V, class KOV, class CMP>
295  if (left->height > right->height + 2) {
296  Node *ll = left->left;
297  Node *lr = left->right;
298  if (ll->height >= lr->height) {
299  Node *nlr = new Node(lr->incref(), right, value);
300  Node *res = new Node(ll->incref(), nlr, left->value);
301  left->decref();
302  return res;
303  } else {
304  Node *lrl = lr->left;
305  Node *lrr = lr->right;
306  Node *nll = new Node(ll->incref(), lrl->incref(), left->value);
307  Node *nlr = new Node(lrr->incref(), right, value);
308  Node *res = new Node(nll, nlr, lr->value);
309  left->decref();
310  return res;
311  }
312  } else if (right->height > left->height + 2) {
313  Node *rl = right->left;
314  Node *rr = right->right;
315  if (rr->height >= rl->height) {
316  Node *nrl = new Node(left, rl->incref(), value);
317  Node *res = new Node(nrl, rr->incref(), right->value);
318  right->decref();
319  return res;
320  } else {
321  Node *rll = rl->left;
322  Node *rlr = rl->right;
323  Node *nrl = new Node(left, rll->incref(), value);
324  Node *nrr = new Node(rlr->incref(), rr->incref(), right->value);
325  Node *res = new Node(nrl, nrr, rl->value);
326  right->decref();
327  return res;
328  }
329  } else {
330  return new Node(left, right, value);
331  }
332  }
333 
334  template<class K, class V, class KOV, class CMP>
336  if (isTerminator()) {
337  return 0;
338  } else {
339  return left->size() + 1 + right->size();
340  }
341  }
342 
343  template<class K, class V, class KOV, class CMP>
346  if (left->isTerminator()) {
347  valueOut = value;
348  return right->incref();
349  } else {
350  return balance(left->popMin(valueOut), value, right->incref());
351  }
352  }
353 
354  template<class K, class V, class KOV, class CMP>
357  if (right->isTerminator()) {
358  valueOut = value;
359  return left->incref();
360  } else {
361  return balance(left->incref(), value, right->popMax(valueOut));
362  }
363  }
364 
365  template<class K, class V, class KOV, class CMP>
368  if (isTerminator()) {
369  return new Node(terminator.incref(), terminator.incref(), v);
370  } else {
371  if (key_compare()(key_of_value()(v), key_of_value()(value))) {
372  return balance(left->insert(v), value, right->incref());
373  } else if (key_compare()(key_of_value()(value), key_of_value()(v))) {
374  return balance(left->incref(), value, right->insert(v));
375  } else {
376  return incref();
377  }
378  }
379  }
380 
381  template<class K, class V, class KOV, class CMP>
384  if (isTerminator()) {
385  return new Node(terminator.incref(), terminator.incref(), v);
386  } else {
387  if (key_compare()(key_of_value()(v), key_of_value()(value))) {
388  return balance(left->replace(v), value, right->incref());
389  } else if (key_compare()(key_of_value()(value), key_of_value()(v))) {
390  return balance(left->incref(), value, right->replace(v));
391  } else {
392  return new Node(left->incref(), right->incref(), v);
393  }
394  }
395  }
396 
397  template<class K, class V, class KOV, class CMP>
400  if (isTerminator()) {
401  return incref();
402  } else {
403  if (key_compare()(k, key_of_value()(value))) {
404  return balance(left->remove(k), value, right->incref());
405  } else if (key_compare()(key_of_value()(value), k)) {
406  return balance(left->incref(), value, right->remove(k));
407  } else {
408  if (left->isTerminator()) {
409  return right->incref();
410  } else if (right->isTerminator()) {
411  return left->incref();
412  } else {
413  value_type min;
414  Node *nr = right->popMin(min);
415  return balance(left->incref(), min, nr);
416  }
417  }
418  }
419  }
420 
421  /***/
422 
423  template<class K, class V, class KOV, class CMP>
425  : node(Node::terminator.incref()) {
426  }
427 
428  template<class K, class V, class KOV, class CMP>
430  : node(_node) {
431  }
432 
433  template<class K, class V, class KOV, class CMP>
435  : node(s.node->incref()) {
436  }
437 
438  template<class K, class V, class KOV, class CMP>
440  node->decref();
441  }
442 
443  template<class K, class V, class KOV, class CMP>
445  Node *n = s.node->incref();
446  node->decref();
447  node = n;
448  return *this;
449  }
450 
451  template<class K, class V, class KOV, class CMP>
453  return node->isTerminator();
454  }
455 
456  template<class K, class V, class KOV, class CMP>
458  Node *n = node;
459  while (!n->isTerminator()) {
460  key_type key = key_of_value()(n->value);
461  if (key_compare()(k, key)) {
462  n = n->left;
463  } else if (key_compare()(key, k)) {
464  n = n->right;
465  } else {
466  return 1;
467  }
468  }
469  return 0;
470  }
471 
472  template<class K, class V, class KOV, class CMP>
475  Node *n = node;
476  while (!n->isTerminator()) {
477  key_type key = key_of_value()(n->value);
478  if (key_compare()(k, key)) {
479  n = n->left;
480  } else if (key_compare()(key, k)) {
481  n = n->right;
482  } else {
483  return &n->value;
484  }
485  }
486  return 0;
487  }
488 
489  template<class K, class V, class KOV, class CMP>
492  Node *n = node;
493  Node *result = 0;
494  while (!n->isTerminator()) {
495  key_type key = key_of_value()(n->value);
496  if (key_compare()(k, key)) {
497  n = n->left;
498  } else if (key_compare()(key, k)) {
499  result = n;
500  n = n->right;
501  } else {
502  return &n->value;
503  }
504  }
505  return result ? &result->value : 0;
506  }
507 
508  template<class K, class V, class KOV, class CMP>
511  Node *n = node;
512  assert(!n->isTerminator());
513  while (!n->left->isTerminator()) n = n->left;
514  return n->value;
515  }
516 
517  template<class K, class V, class KOV, class CMP>
520  Node *n = node;
521  assert(!n->isTerminator());
522  while (!n->right->isTerminator()) n = n->right;
523  return n->value;
524  }
525 
526  template<class K, class V, class KOV, class CMP>
528  return node->size();
529  }
530 
531  template<class K, class V, class KOV, class CMP>
534  return ImmutableTree(node->insert(value));
535  }
536 
537  template<class K, class V, class KOV, class CMP>
540  return ImmutableTree(node->replace(value));
541  }
542 
543  template<class K, class V, class KOV, class CMP>
546  return ImmutableTree(node->remove(key));
547  }
548 
549  template<class K, class V, class KOV, class CMP>
552  return ImmutableTree(node->popMin(valueOut));
553  }
554 
555  template<class K, class V, class KOV, class CMP>
558  return ImmutableTree(node->popMax(valueOut));
559  }
560 
561  template<class K, class V, class KOV, class CMP>
562  inline typename ImmutableTree<K,V,KOV,CMP>::iterator
564  return iterator(node, true);
565  }
566 
567  template<class K, class V, class KOV, class CMP>
568  inline typename ImmutableTree<K,V,KOV,CMP>::iterator
570  return iterator(node, false);
571  }
572 
573  template<class K, class V, class KOV, class CMP>
574  inline typename ImmutableTree<K,V,KOV,CMP>::iterator
576  iterator end(node,false), it = lower_bound(key);
577  if (it==end || key_compare()(key,key_of_value()(*it))) {
578  return end;
579  } else {
580  return it;
581  }
582  }
583 
584  template<class K, class V, class KOV, class CMP>
585  inline typename ImmutableTree<K,V,KOV,CMP>::iterator
587  // XXX ugh this doesn't have to be so ugly does it?
588  iterator it(node,false);
589  for (Node *root=node; !root->isTerminator();) {
590  it.stack.push_back(root);
591  if (key_compare()(k, key_of_value()(root->value))) {
592  root = root->left;
593  } else if (key_compare()(key_of_value()(root->value), k)) {
594  root = root->right;
595  } else {
596  return it;
597  }
598  }
599  // it is now beginning or first element < k
600  if (!it.stack.empty()) {
601  Node *last = it.stack.back();
602  if (key_compare()(key_of_value()(last->value), k))
603  ++it;
604  }
605  return it;
606  }
607 
608  template<class K, class V, class KOV, class CMP>
611  iterator end(node,false),it = lower_bound(key);
612  if (it!=end &&
613  !key_compare()(key,key_of_value()(*it))) // no need to loop, no duplicates
614  ++it;
615  return it;
616  }
617 
618 }
619 
620 #endif
iterator end() const
ImmutableTree remove(const key_type &key) const
iterator begin() const
ImmutableTree insert(const value_type &value) const
bool operator!=(const iterator &b)
Node * popMax(value_type &valueOut)
iterator lower_bound(const key_type &key) const
iterator(const iterator &i)
ImmutableTree popMin(value_type &valueOut) const
const value_type * lookup_previous(const key_type &key) const
Node * insert(const value_type &v)
Node * popMin(value_type &valueOut)
ImmutableTree & operator=(const ImmutableTree &s)
void push_back(const T &elt)
static size_t getAllocated()
Definition: ImmutableTree.h:60
const value_type * lookup(const key_type &key) const
ImmutableTree replace(const value_type &value) const
const value_type & max() const
ImmutableTree popMax(value_type &valueOut) const
static Node * balance(Node *left, const value_type &value, Node *right)
size_t size() const
FixedStack(unsigned _max)
bool operator==(const iterator &b)
iterator find(const key_type &key) const
bool operator==(const FixedStack &b)
const value_type * operator->()
Node * replace(const value_type &v)
Node * remove(const key_type &k)
static size_t allocated
Definition: ImmutableTree.h:20
FixedStack & operator=(const FixedStack &b)
bool operator!=(const FixedStack &b)
const value_type & operator*()
FixedStack< Node * > stack
iterator(Node *_root, bool atBeginning)
bool empty() const
FixedStack(const FixedStack &b)
const value_type & min() const
iterator upper_bound(const key_type &key) const
iterator & operator=(const iterator &b)
size_t count(const key_type &key) const