10#ifndef KLEE_IMMUTABLETREE_H
11#define KLEE_IMMUTABLETREE_H
17 template<
class K,
class V,
class KOV,
class CMP>
71 template<
class K,
class V,
class KOV,
class CMP>
81 static Node *balance(Node *left,
const value_type &value, Node *right);
85 Node(Node *_left, Node *_right,
const value_type &_value);
139 template<
class K,
class V,
class KOV,
class CMP>
148 stack(root->height) {
180 return stack==b.
stack;
183 return stack!=b.
stack;
214 assert(!stack.
empty());
239 template<
class K,
class V,
class KOV,
class CMP>
243 template<
class K,
class V,
class KOV,
class CMP>
246 template<
class K,
class V,
class KOV,
class CMP>
255 template<
class K,
class V,
class KOV,
class CMP>
260 height(std::
max(left->height, right->height) + 1),
266 template<
class K,
class V,
class KOV,
class CMP>
273 template<
class K,
class V,
class KOV,
class CMP>
276 if (references==0)
delete this;
279 template<
class K,
class V,
class KOV,
class CMP>
285 template<
class K,
class V,
class KOV,
class CMP>
287 return this==&terminator;
292 template<
class K,
class V,
class KOV,
class CMP>
330 return new Node(left, right, value);
334 template<
class K,
class V,
class KOV,
class CMP>
336 if (isTerminator()) {
339 return left->size() + 1 + right->size();
343 template<
class K,
class V,
class KOV,
class CMP>
346 if (left->isTerminator()) {
350 return balance(left->popMin(valueOut), value, right->incref());
354 template<
class K,
class V,
class KOV,
class CMP>
357 if (right->isTerminator()) {
361 return balance(left->incref(), value, right->popMax(valueOut));
365 template<
class K,
class V,
class KOV,
class CMP>
368 if (isTerminator()) {
369 return new Node(terminator.incref(), terminator.incref(), v);
372 return balance(left->insert(v), value, right->incref());
374 return balance(left->incref(), value, right->insert(v));
381 template<
class K,
class V,
class KOV,
class CMP>
384 if (isTerminator()) {
385 return new Node(terminator.incref(), terminator.incref(), v);
388 return balance(left->replace(v), value, right->incref());
390 return balance(left->incref(), value, right->replace(v));
392 return new Node(left->incref(), right->incref(), v);
397 template<
class K,
class V,
class KOV,
class CMP>
400 if (isTerminator()) {
404 return balance(left->remove(k), value, right->incref());
406 return balance(left->incref(), value, right->remove(k));
408 if (left->isTerminator()) {
409 return right->incref();
410 }
else if (right->isTerminator()) {
411 return left->incref();
415 return balance(left->incref(),
min, nr);
423 template<
class K,
class V,
class KOV,
class CMP>
428 template<
class K,
class V,
class KOV,
class CMP>
433 template<
class K,
class V,
class KOV,
class CMP>
435 : node(s.node->incref()) {
438 template<
class K,
class V,
class KOV,
class CMP>
443 template<
class K,
class V,
class KOV,
class CMP>
451 template<
class K,
class V,
class KOV,
class CMP>
453 return node->isTerminator();
456 template<
class K,
class V,
class KOV,
class CMP>
472 template<
class K,
class V,
class KOV,
class CMP>
489 template<
class K,
class V,
class KOV,
class CMP>
505 return result ? &result->
value : 0;
508 template<
class K,
class V,
class KOV,
class CMP>
517 template<
class K,
class V,
class KOV,
class CMP>
526 template<
class K,
class V,
class KOV,
class CMP>
531 template<
class K,
class V,
class KOV,
class CMP>
537 template<
class K,
class V,
class KOV,
class CMP>
543 template<
class K,
class V,
class KOV,
class CMP>
549 template<
class K,
class V,
class KOV,
class CMP>
555 template<
class K,
class V,
class KOV,
class CMP>
561 template<
class K,
class V,
class KOV,
class CMP>
567 template<
class K,
class V,
class KOV,
class CMP>
573 template<
class K,
class V,
class KOV,
class CMP>
576 iterator end(node,
false), it = lower_bound(key);
584 template<
class K,
class V,
class KOV,
class CMP>
590 it.
stack.push_back(root);
600 if (!it.
stack.empty()) {
608 template<
class K,
class V,
class KOV,
class CMP>
611 iterator end(node,
false),it = lower_bound(key);
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
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
iterator find(const key_type &key) const
ImmutableTree popMax(value_type &valueOut) const
size_t count(const key_type &key) const
ImmutableTree insert(const value_type &value) const
static size_t getAllocated()
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
iterator upper_bound(const key_type &key) const
ImmutableTree & operator=(const ImmutableTree &s)
const value_type & min() const