klee
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 KLEE_IMMUTABLETREE_H
11#define KLEE_IMMUTABLETREE_H
12
13#include <cassert>
14#include <vector>
15
16namespace klee {
17 template<class K, class V, class KOV, class CMP>
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:
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;
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
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:
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>
105 unsigned pos, max;
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 {
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>
564 return iterator(node, true);
565 }
566
567 template<class K, class V, class KOV, class CMP>
570 return iterator(node, false);
571 }
572
573 template<class K, class V, class KOV, class CMP>
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>
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 /* KLEE_IMMUTABLETREE_H */
FixedStack(unsigned _max)
void push_back(const T &elt)
FixedStack & operator=(const FixedStack &b)
bool operator!=(const FixedStack &b)
bool operator==(const FixedStack &b)
FixedStack(const FixedStack &b)
Node * popMax(value_type &valueOut)
static Node * balance(Node *left, const value_type &value, Node *right)
Node * popMin(value_type &valueOut)
Node * remove(const key_type &k)
Node * replace(const value_type &v)
Node * insert(const value_type &v)
bool operator==(const iterator &b)
const value_type & operator*()
bool operator!=(const iterator &b)
iterator & operator=(const iterator &b)
FixedStack< Node * > stack
iterator(Node *_root, bool atBeginning)
const value_type * operator->()
iterator(const iterator &i)
ImmutableTree popMin(value_type &valueOut) const
iterator end() const
ImmutableTree(const ImmutableTree &s)
const value_type & max() const
ImmutableTree remove(const key_type &key) const
const value_type * lookup(const key_type &key) const
bool empty() const
iterator find(const key_type &key) const
ImmutableTree popMax(value_type &valueOut) const
size_t count(const key_type &key) const
size_t size() const
ImmutableTree insert(const value_type &value) const
static size_t getAllocated()
Definition: ImmutableTree.h:60
ImmutableTree replace(const value_type &value) const
iterator lower_bound(const key_type &key) const
ImmutableTree(Node *_node)
const value_type * lookup_previous(const key_type &key) const
static size_t allocated
Definition: ImmutableTree.h:20
iterator begin() const
iterator upper_bound(const key_type &key) const
ImmutableTree & operator=(const ImmutableTree &s)
const value_type & min() const
Definition: main.cpp:291