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