Removed the Internal directory from include/klee

9 files changed, 1795 insertions, 0 deletions

diff --git a/include/klee/ADT/DiscretePDF.h b/include/klee/ADT/DiscretePDF.h
new file mode 100644
index 00000000..74a1ce9e
--- /dev/null
+++ b/include/klee/ADT/DiscretePDF.h
@@ -0,0 +1,52 @@
+//===-- DiscretePDF.h -------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_DISCRETEPDF_H
+#define KLEE_DISCRETEPDF_H
+
+namespace klee {
+  template <class T>
+  class DiscretePDF {
+    // not perfectly parameterized, but float/double/int should work ok,
+    // although it would be better to have choose argument range from 0
+    // to queryable max.
+    typedef double weight_type;
+
+  public:
+    DiscretePDF();
+    ~DiscretePDF();
+
+    bool empty() const;
+    void insert(T item, weight_type weight);
+    void update(T item, weight_type newWeight);
+    void remove(T item);
+    bool inTree(T item);
+    weight_type getWeight(T item);
+	
+    /* pick a tree element according to its
+     * weight. p should be in [0,1).
+     */
+    T choose(double p);
+    
+  private:
+    class Node;
+    Node *m_root;
+    
+    Node **lookup(T item, Node **parent_out);
+    void split(Node *node);
+    void rotate(Node *node);
+    void lengthen(Node *node);
+    void propogateSumsUp(Node *n);
+  };
+
+}
+
+#include "DiscretePDF.inc"
+
+#endif /* KLEE_DISCRETEPDF_H */
diff --git a/include/klee/ADT/DiscretePDF.inc b/include/klee/ADT/DiscretePDF.inc
new file mode 100644
index 00000000..743a69b5
--- /dev/null
+++ b/include/klee/ADT/DiscretePDF.inc
@@ -0,0 +1,347 @@
+//===- DiscretePDF.inc - --*- C++ -*---------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <cassert>
+namespace klee {
+
+template <class T>
+class DiscretePDF<T>::Node
+{
+private:
+  bool m_mark;
+
+public:
+  Node *parent, *left, *right;
+  T key;
+  weight_type weight, sumWeights;
+
+public:
+  Node(T key_, weight_type weight_, Node *parent_);
+  ~Node();
+
+  Node *sibling() { return this==parent->left?parent->right:parent->left; }
+
+  void markRed() { m_mark = true; }
+  void markBlack() { m_mark = false; }
+  bool isBlack() { return !m_mark; }
+  bool leftIsBlack() { return !left || left->isBlack(); }
+  bool rightIsBlack() { return !right || right->isBlack(); }
+  void setSum() { 
+    sumWeights = weight;
+    if (left) sumWeights += left->sumWeights;
+    if (right) sumWeights += right->sumWeights;
+  }
+};
+
+  ///
+
+template <class T>
+DiscretePDF<T>::Node::Node(T key_, weight_type weight_, Node *parent_) {
+  m_mark = false;
+
+  key = key_;
+  weight = weight_;
+  sumWeights = 0;
+  left = right = 0;
+  parent = parent_;
+}
+
+template <class T>
+DiscretePDF<T>::Node::~Node() {
+  delete left;
+  delete right;
+}
+
+//
+
+template <class T>
+DiscretePDF<T>::DiscretePDF() {
+  m_root = 0;
+}
+
+template <class T>
+DiscretePDF<T>::~DiscretePDF() {
+  delete m_root;
+}
+
+template <class T>
+bool DiscretePDF<T>::empty() const {
+  return m_root == 0;
+}
+
+template <class T>
+void DiscretePDF<T>::insert(T item, weight_type weight) {
+  Node *p=0, *n=m_root;
+
+  while (n) {
+    if (!n->leftIsBlack() && !n->rightIsBlack())
+      split(n);
+
+    p = n;
+    if (n->key==item) {
+      assert(0 && "insert: argument(item) already in tree");
+    } else {
+      n = (item<n->key)?n->left:n->right;
+    }
+  }
+
+  n = new Node(item, weight, p);
+
+  if (!p) {
+    m_root = n;
+  } else {
+    if (item<p->key) {
+      p->left = n;
+    } else {
+      p->right = n;
+    }
+
+    split(n);
+  }
+
+  propogateSumsUp(n);
+}
+
+template <class T>
+void DiscretePDF<T>::remove(T item) {
+  Node **np = lookup(item, 0);
+  Node *child, *n = *np;
+
+  if (!n) {
+    assert(0 && "remove: argument(item) not in tree");
+  } else {
+    if (n->left) {
+      Node **leftMaxp = &n->left;
+
+      while ((*leftMaxp)->right)
+        leftMaxp = &(*leftMaxp)->right;
+
+      n->key = (*leftMaxp)->key;
+      n->weight = (*leftMaxp)->weight;
+
+      np = leftMaxp;
+      n = *np;
+    }
+
+    // node now has at most one child
+
+    child = n->left?n->left:n->right;
+    *np = child;
+
+    if (child) {
+      child->parent = n->parent;
+
+      if (n->isBlack()) {
+        lengthen(child);
+      }
+    }
+
+    propogateSumsUp(n->parent);
+
+    n->left = n->right = 0;
+    delete n;
+  }
+}
+
+template <class T>
+void DiscretePDF<T>::update(T item, weight_type weight) {
+  Node *n = *lookup(item, 0);
+
+  if (!n) {
+    assert(0 && "update: argument(item) not in tree");
+  } else {
+    n->weight = weight;
+    propogateSumsUp(n);
+  }
+}
+
+template <class T>
+T DiscretePDF<T>::choose(double p) {
+  assert (!((p < 0.0) || (p >= 1.0)) && "choose: argument(p) outside valid range");
+
+  if (!m_root)
+    assert(0 && "choose: choose() called on empty tree");
+
+  weight_type w = (weight_type) (m_root->sumWeights * p);
+  Node *n = m_root;
+
+  while (1) {
+    if (n->left) {
+      if (w<n->left->sumWeights) {
+	n = n->left;
+	continue;
+      } else {
+	w -= n->left->sumWeights;
+      }
+    }
+    if (w<n->weight || !n->right) {
+      break; // !n->right condition shouldn't be necessary, just sanity check
+    }
+    w -= n->weight;
+    n = n->right;
+  }
+
+  return n->key;
+}
+
+template <class T>
+bool DiscretePDF<T>::inTree(T item) {
+  Node *n = *lookup(item, 0);
+
+  return !!n;
+}
+
+template <class T>
+typename DiscretePDF<T>::weight_type DiscretePDF<T>::getWeight(T item) {
+  Node *n = *lookup(item, 0);
+  assert(n);
+  return n->weight;
+}
+
+//
+
+template <class T>
+typename DiscretePDF<T>::Node **
+DiscretePDF<T>::lookup(T item, Node **parent_out) {
+  Node *n, *p=0, **np=&m_root;
+
+  while ((n = *np)) {
+    if (n->key==item) {
+      break;
+    } else {
+      p = n;
+      if (item<n->key) {
+        np = &n->left;
+      } else {
+        np = &n->right;
+      }
+    }
+  }
+
+  if (parent_out)
+    *parent_out = p;
+  return np;
+}
+
+template <class T>
+void DiscretePDF<T>::split(Node *n) {
+  if (n->left) n->left->markBlack();
+  if (n->right) n->right->markBlack();
+
+  if (n->parent) {
+    Node *p = n->parent;
+
+    n->markRed();
+
+    if (!p->isBlack()) {
+      p->parent->markRed();
+
+      // not same direction
+      if (!((n==p->left && p==p->parent->left) || 
+            (n==p->right && p==p->parent->right))) {
+        rotate(n);
+        p = n;
+      }
+
+      rotate(p);
+      p->markBlack();
+    }
+  }
+}
+
+template <class T>
+void DiscretePDF<T>::rotate(Node *n) {
+  Node *p=n->parent, *pp=p->parent;
+
+  n->parent = pp;
+  p->parent = n;
+
+  if (n==p->left) {
+    p->left = n->right;
+    n->right = p;
+    if (p->left) p->left->parent = p;
+  } else {
+    p->right = n->left;
+    n->left = p;
+    if (p->right) p->right->parent = p;
+  }
+
+  n->setSum();
+  p->setSum();
+	
+  if (!pp) {
+    m_root = n;
+  } else {
+    if (p==pp->left) {
+      pp->left = n;
+    } else {
+      pp->right = n;
+    }
+  }
+}
+
+template <class T>
+void DiscretePDF<T>::lengthen(Node *n) {
+  if (!n->isBlack()) {
+    n->markBlack();
+  } else if (n->parent) {
+    Node *sibling = n->sibling();
+
+    if (sibling && !sibling->isBlack()) {
+      n->parent->markRed();
+      sibling->markBlack();
+
+      rotate(sibling); // node sibling is now old sibling child, must be black
+      sibling = n->sibling();
+    }
+
+    // sibling is black
+
+    if (!sibling) {
+      lengthen(n->parent);
+    } else if (sibling->leftIsBlack() && sibling->rightIsBlack()) {
+      if (n->parent->isBlack()) {
+        sibling->markRed();
+        lengthen(n->parent);
+      } else {
+        sibling->markRed();
+        n->parent->markBlack();
+      }
+    } else {
+      if (n==n->parent->left && sibling->rightIsBlack()) {
+        rotate(sibling->left); // sibling->left must be red
+        sibling->markRed();
+        sibling->parent->markBlack();
+        sibling = sibling->parent;
+      } else if (n==n->parent->right && sibling->leftIsBlack()) {
+        rotate(sibling->right); // sibling->right must be red
+        sibling->markRed();
+        sibling->parent->markBlack();
+        sibling = sibling->parent;
+      }
+
+      // sibling is black, and sibling's far child is red
+
+      rotate(sibling);
+      if (!n->parent->isBlack()) 
+        sibling->markRed();
+      sibling->left->markBlack();
+      sibling->right->markBlack();
+    }
+  }
+}
+
+template <class T>
+void DiscretePDF<T>::propogateSumsUp(Node *n) {
+  for (; n; n=n->parent)
+    n->setSum();
+}
+
+}
+
diff --git a/include/klee/ADT/ImmutableMap.h b/include/klee/ADT/ImmutableMap.h
new file mode 100644
index 00000000..a7a18a89
--- /dev/null
+++ b/include/klee/ADT/ImmutableMap.h
@@ -0,0 +1,104 @@
+//===-- ImmutableMap.h ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_IMMUTABLEMAP_H
+#define KLEE_IMMUTABLEMAP_H
+
+#include <functional>
+
+#include "ImmutableTree.h"
+
+namespace klee {
+  template<class V, class D>
+  struct _Select1st {
+    D &operator()(V &a) const { return a.first; }
+    const D &operator()(const V &a) const { return a.first; }
+  };
+  
+  template<class K, class D, class CMP=std::less<K> >
+  class ImmutableMap {
+  public:
+    typedef K key_type;
+    typedef std::pair<K,D> value_type;
+
+    typedef ImmutableTree<K, value_type, _Select1st<value_type,key_type>, CMP> Tree;
+    typedef typename Tree::iterator iterator;
+
+  private:
+    Tree elts;
+
+    ImmutableMap(const Tree &b): elts(b) {}
+
+  public:
+    ImmutableMap() {}
+    ImmutableMap(const ImmutableMap &b) : elts(b.elts) {}
+    ~ImmutableMap() {}
+
+    ImmutableMap &operator=(const ImmutableMap &b) { elts = b.elts; return *this; }
+    
+    bool empty() const { 
+      return elts.empty(); 
+    }
+    size_t count(const key_type &key) const { 
+      return elts.count(key); 
+    }
+    const value_type *lookup(const key_type &key) const { 
+      return elts.lookup(key); 
+    }
+    const value_type *lookup_previous(const key_type &key) const { 
+      return elts.lookup_previous(key); 
+    }
+    const value_type &min() const { 
+      return elts.min(); 
+    }
+    const value_type &max() const { 
+      return elts.max(); 
+    }
+    size_t size() const { 
+      return elts.size(); 
+    }
+
+    ImmutableMap insert(const value_type &value) const { 
+      return elts.insert(value); 
+    }
+    ImmutableMap replace(const value_type &value) const { 
+      return elts.replace(value); 
+    }
+    ImmutableMap remove(const key_type &key) const { 
+      return elts.remove(key); 
+    }
+    ImmutableMap popMin(const value_type &valueOut) const { 
+      return elts.popMin(valueOut); 
+    }
+    ImmutableMap popMax(const value_type &valueOut) const { 
+      return elts.popMax(valueOut); 
+    }
+
+    iterator begin() const { 
+      return elts.begin(); 
+    }
+    iterator end() const { 
+      return elts.end(); 
+    }
+    iterator find(const key_type &key) const { 
+      return elts.find(key); 
+    }
+    iterator lower_bound(const key_type &key) const { 
+      return elts.lower_bound(key); 
+    }
+    iterator upper_bound(const key_type &key) const { 
+      return elts.upper_bound(key); 
+    }
+
+    static size_t getAllocated() { return Tree::allocated; }
+  };
+
+}
+
+#endif /* KLEE_IMMUTABLEMAP_H */
diff --git a/include/klee/ADT/ImmutableSet.h b/include/klee/ADT/ImmutableSet.h
new file mode 100644
index 00000000..1618e559
--- /dev/null
+++ b/include/klee/ADT/ImmutableSet.h
@@ -0,0 +1,101 @@
+//===-- ImmutableSet.h ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_IMMUTABLESET_H
+#define KLEE_IMMUTABLESET_H
+
+#include <functional>
+
+#include "ImmutableTree.h"
+
+namespace klee {
+  template<class T>
+  struct _Identity {
+    T &operator()(T &a) const { return a; }
+    const T &operator()(const T &a) const { return a; }
+  };
+  
+  template<class T, class CMP=std::less<T> >
+  class ImmutableSet {
+  public:
+    typedef T key_type;
+    typedef T value_type;
+
+    typedef ImmutableTree<T, T, _Identity<T>, CMP> Tree;
+    typedef typename Tree::iterator iterator;
+
+  private:
+    Tree elts;
+
+    ImmutableSet(const Tree &b): elts(b) {}
+
+  public:
+    ImmutableSet() {}
+    ImmutableSet(const ImmutableSet &b) : elts(b.elts) {}
+    ~ImmutableSet() {}
+
+    ImmutableSet &operator=(const ImmutableSet &b) { elts = b.elts; return *this; }
+    
+    bool empty() const { 
+      return elts.empty(); 
+    }
+    size_t count(const key_type &key) const { 
+      return elts.count(key); 
+    }
+    const value_type *lookup(const key_type &key) const { 
+      return elts.lookup(key); 
+    }
+    const value_type &min() const { 
+      return elts.min(); 
+    }
+    const value_type &max() const { 
+      return elts.max(); 
+    }
+    size_t size() { 
+      return elts.size(); 
+    }
+
+    ImmutableSet insert(const value_type &value) const {
+      return elts.insert(value); 
+    }
+    ImmutableSet replace(const value_type &value) const {
+      return elts.replace(value); 
+    }
+    ImmutableSet remove(const key_type &key) const { 
+      return elts.remove(key); 
+    }
+    ImmutableSet popMin(const value_type &valueOut) const { 
+      return elts.popMin(valueOut); 
+    }
+    ImmutableSet popMax(const value_type &valueOut) const { 
+      return elts.popMax(valueOut); 
+    }
+
+    iterator begin() const { 
+      return elts.begin(); 
+    }
+    iterator end() const { 
+      return elts.end(); 
+    }
+    iterator find(const key_type &key) const { 
+      return elts.find(key); 
+    }
+    iterator lower_bound(const key_type &key) const { 
+      return elts.lower_bound(key); 
+    }
+    iterator upper_bound(const key_type &key) const { 
+      return elts.upper_bound(key); 
+    }
+
+    static size_t getAllocated() { return Tree::allocated; }
+  };
+
+}
+
+#endif /* KLEE_IMMUTABLESET_H */
diff --git a/include/klee/ADT/ImmutableTree.h b/include/klee/ADT/ImmutableTree.h
new file mode 100644
index 00000000..ada3c211
--- /dev/null
+++ b/include/klee/ADT/ImmutableTree.h
@@ -0,0 +1,620 @@
+//===-- ImmutableTree.h -----------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_IMMUTABLETREE_H
+#define KLEE_IMMUTABLETREE_H
+
+#include <cassert>
+#include <vector>
+
+namespace klee {
+  template<class K, class V, class KOV, class CMP>
+  class ImmutableTree {
+  public:
+    static size_t allocated;
+    class iterator;
+
+    typedef K key_type;
+    typedef V value_type;
+    typedef KOV key_of_value;
+    typedef CMP key_compare;
+
+  public:
+    ImmutableTree();
+    ImmutableTree(const ImmutableTree &s);
+    ~ImmutableTree();
+
+    ImmutableTree &operator=(const ImmutableTree &s);
+
+    bool empty() const;
+
+    size_t count(const key_type &key) const; // always 0 or 1
+    const value_type *lookup(const key_type &key) const;
+
+    // find the last value less than or equal to key, or null if
+    // no such value exists
+    const value_type *lookup_previous(const key_type &key) const;
+
+    const value_type &min() const;
+    const value_type &max() const;
+    size_t size() const;
+
+    ImmutableTree insert(const value_type &value) const;
+    ImmutableTree replace(const value_type &value) const;
+    ImmutableTree remove(const key_type &key) const;
+    ImmutableTree popMin(value_type &valueOut) const;
+    ImmutableTree popMax(value_type &valueOut) const;
+
+    iterator begin() const;
+    iterator end() const;
+    iterator find(const key_type &key) const;
+    iterator lower_bound(const key_type &key) const;
+    iterator upper_bound(const key_type &key) const;
+
+    static size_t getAllocated() { return allocated; }
+
+  private:
+    class Node;
+
+    Node *node;
+    ImmutableTree(Node *_node);
+  };
+
+  /***/
+
+  template<class K, class V, class KOV, class CMP>
+  class ImmutableTree<K,V,KOV,CMP>::Node {
+  public:
+    static Node terminator;
+    Node *left, *right;
+    value_type value;
+    unsigned height, references;
+
+  protected:
+    Node(); // solely for creating the terminator node
+    static Node *balance(Node *left, const value_type &value, Node *right);
+
+  public:
+
+    Node(Node *_left, Node *_right, const value_type &_value);
+    ~Node();
+
+    void decref();
+    Node *incref();
+
+    bool isTerminator();
+
+    size_t size();
+    Node *popMin(value_type &valueOut);
+    Node *popMax(value_type &valueOut);
+    Node *insert(const value_type &v);
+    Node *replace(const value_type &v);
+    Node *remove(const key_type &k);
+  };
+
+  // Should live somewhere else, this is a simple stack with maximum (dynamic)
+  // size.
+  template<typename T>
+  class FixedStack {
+    unsigned pos, max;
+    T *elts;
+
+  public:
+    FixedStack(unsigned _max) : pos(0),
+                                max(_max),
+                                elts(new T[max]) {}
+    FixedStack(const FixedStack &b) : pos(b.pos),
+                                      max(b.max),
+                                      elts(new T[b.max]) {
+      std::copy(b.elts, b.elts+pos, elts);
+    }
+    ~FixedStack() { delete[] elts; }
+
+    void push_back(const T &elt) { elts[pos++] = elt; }
+    void pop_back() { --pos; }
+    bool empty() { return pos==0; }
+    T &back() { return elts[pos-1]; }
+
+
+    FixedStack &operator=(const FixedStack &b) {
+      assert(max == b.max); 
+      pos = b.pos;
+      std::copy(b.elts, b.elts+pos, elts);
+      return *this;
+    }
+
+    bool operator==(const FixedStack &b) {
+      return (pos == b.pos &&
+              std::equal(elts, elts+pos, b.elts));
+    }
+    bool operator!=(const FixedStack &b) { return !(*this==b); }
+  };
+
+  template<class K, class V, class KOV, class CMP>
+  class ImmutableTree<K,V,KOV,CMP>::iterator {
+    friend class ImmutableTree<K,V,KOV,CMP>;
+  private:
+    Node *root; // so can back up from end
+    FixedStack<Node*> stack;
+    
+  public:
+    iterator(Node *_root, bool atBeginning) : root(_root->incref()),
+                                              stack(root->height) {
+      if (atBeginning) {
+        for (Node *n=root; !n->isTerminator(); n=n->left)
+          stack.push_back(n);
+      }
+    }
+    iterator(const iterator &i) : root(i.root->incref()),
+                                  stack(i.stack) {
+    }
+    ~iterator() {
+      root->decref();
+    }
+
+    iterator &operator=(const iterator &b) {
+      b.root->incref();
+      root->decref();
+      root = b.root;
+      stack = b.stack;
+      return *this;
+    }
+
+    const value_type &operator*() {
+      Node *n = stack.back();
+      return n->value;
+    }
+
+    const value_type *operator->() {
+      Node *n = stack.back();
+      return &n->value;
+    }
+
+    bool operator==(const iterator &b) {
+      return stack==b.stack;
+    }
+    bool operator!=(const iterator &b) {
+      return stack!=b.stack;
+    }
+    
+    iterator &operator--() {
+      if (stack.empty()) {
+        for (Node *n=root; !n->isTerminator(); n=n->right)
+          stack.push_back(n);
+      } else {
+        Node *n = stack.back();
+        if (n->left->isTerminator()) {
+          for (;;) {
+            Node *prev = n;
+            stack.pop_back();
+            if (stack.empty()) {
+              break;
+            } else {
+              n = stack.back();
+              if (prev==n->right)
+                break;
+            }
+          }
+        } else {
+          stack.push_back(n->left);
+          for (n=n->left->right; !n->isTerminator(); n=n->right)
+            stack.push_back(n);
+        }
+      }
+      return *this;
+    }
+
+    iterator &operator++() {
+      assert(!stack.empty());
+      Node *n = stack.back();
+      if (n->right->isTerminator()) {
+        for (;;) {
+          Node *prev = n;
+          stack.pop_back();
+          if (stack.empty()) {
+            break;
+          } else {
+            n = stack.back();
+            if (prev==n->left)
+              break;
+          }
+        }
+      } else {
+        stack.push_back(n->right);
+        for (n=n->right->left; !n->isTerminator(); n=n->left)
+          stack.push_back(n);
+      }
+      return *this;
+    }
+  };
+
+  /***/
+
+  template<class K, class V, class KOV, class CMP> 
+  typename ImmutableTree<K,V,KOV,CMP>::Node 
+  ImmutableTree<K,V,KOV,CMP>::Node::terminator;
+
+  template<class K, class V, class KOV, class CMP> 
+  size_t ImmutableTree<K,V,KOV,CMP>::allocated = 0;
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP>::Node::Node() 
+    : left(&terminator), 
+      right(&terminator), 
+      height(0), 
+      references(3) { 
+    assert(this==&terminator);
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP>::Node::Node(Node *_left, Node *_right, const value_type &_value)
+    : left(_left), 
+      right(_right), 
+      value(_value), 
+      height(std::max(left->height, right->height) + 1),
+      references(1) 
+  {
+    ++allocated;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP>::Node::~Node() {
+    left->decref();
+    right->decref();
+    --allocated;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  inline void ImmutableTree<K,V,KOV,CMP>::Node::decref() {
+    --references;
+    if (references==0) delete this;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  inline typename ImmutableTree<K,V,KOV,CMP>::Node *ImmutableTree<K,V,KOV,CMP>::Node::incref() {
+    ++references;
+    return this;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  inline bool ImmutableTree<K,V,KOV,CMP>::Node::isTerminator() {
+    return this==&terminator;
+  }
+
+  /***/
+
+  template<class K, class V, class KOV, class CMP>
+  typename ImmutableTree<K,V,KOV,CMP>::Node *
+  ImmutableTree<K,V,KOV,CMP>::Node::balance(Node *left, const value_type &value, Node *right) {
+    if (left->height > right->height + 2) {
+      Node *ll = left->left;
+      Node *lr = left->right;
+      if (ll->height >= lr->height) {
+        Node *nlr = new Node(lr->incref(), right, value);
+        Node *res = new Node(ll->incref(), nlr, left->value);
+        left->decref();
+        return res;
+      } else {
+        Node *lrl = lr->left;
+        Node *lrr = lr->right;
+        Node *nll = new Node(ll->incref(), lrl->incref(), left->value);
+        Node *nlr = new Node(lrr->incref(), right, value);
+        Node *res = new Node(nll, nlr, lr->value);
+        left->decref();
+        return res;
+      }
+    } else if (right->height > left->height + 2) {
+      Node *rl = right->left;
+      Node *rr = right->right;
+      if (rr->height >= rl->height) {
+        Node *nrl = new Node(left, rl->incref(), value);
+        Node *res = new Node(nrl, rr->incref(), right->value);
+        right->decref();
+        return res;
+      } else {
+        Node *rll = rl->left;
+        Node *rlr = rl->right;
+        Node *nrl = new Node(left, rll->incref(), value);
+        Node *nrr = new Node(rlr->incref(), rr->incref(), right->value);
+        Node *res = new Node(nrl, nrr, rl->value);
+        right->decref();
+        return res;
+      }
+    } else {
+      return new Node(left, right, value);
+    }
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  size_t ImmutableTree<K,V,KOV,CMP>::Node::size() {
+    if (isTerminator()) {
+      return 0;
+    } else {
+      return left->size() + 1 + right->size();
+    }
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  typename ImmutableTree<K,V,KOV,CMP>::Node *
+  ImmutableTree<K,V,KOV,CMP>::Node::popMin(value_type &valueOut) {
+    if (left->isTerminator()) {
+      valueOut = value;
+      return right->incref();
+    } else {
+      return balance(left->popMin(valueOut), value, right->incref());
+    }
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  typename ImmutableTree<K,V,KOV,CMP>::Node *
+  ImmutableTree<K,V,KOV,CMP>::Node::popMax(value_type &valueOut) {
+    if (right->isTerminator()) {
+      valueOut = value;
+      return left->incref();
+    } else {
+      return balance(left->incref(), value, right->popMax(valueOut));
+    }
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  typename ImmutableTree<K,V,KOV,CMP>::Node *
+  ImmutableTree<K,V,KOV,CMP>::Node::insert(const value_type &v) {
+    if (isTerminator()) {
+      return new Node(terminator.incref(), terminator.incref(), v);
+    } else {
+      if (key_compare()(key_of_value()(v), key_of_value()(value))) {
+        return balance(left->insert(v), value, right->incref());
+      } else if (key_compare()(key_of_value()(value), key_of_value()(v))) {
+        return balance(left->incref(), value, right->insert(v));
+      } else {
+        return incref();
+      }
+    }
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  typename ImmutableTree<K,V,KOV,CMP>::Node *
+  ImmutableTree<K,V,KOV,CMP>::Node::replace(const value_type &v) {
+    if (isTerminator()) {
+      return new Node(terminator.incref(), terminator.incref(), v);
+    } else {
+      if (key_compare()(key_of_value()(v), key_of_value()(value))) {
+        return balance(left->replace(v), value, right->incref());
+      } else if (key_compare()(key_of_value()(value), key_of_value()(v))) {
+        return balance(left->incref(), value, right->replace(v));
+      } else {
+        return new Node(left->incref(), right->incref(), v);
+      }
+    }
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  typename ImmutableTree<K,V,KOV,CMP>::Node *
+  ImmutableTree<K,V,KOV,CMP>::Node::remove(const key_type &k) {
+    if (isTerminator()) {
+      return incref();
+    } else {
+      if (key_compare()(k, key_of_value()(value))) {
+        return balance(left->remove(k), value, right->incref());
+      } else if (key_compare()(key_of_value()(value), k)) {
+        return balance(left->incref(), value, right->remove(k));
+      } else {
+        if (left->isTerminator()) {
+          return right->incref();
+        } else if (right->isTerminator()) {
+          return left->incref();
+        } else {
+          value_type min;
+          Node *nr = right->popMin(min);
+          return balance(left->incref(), min, nr);
+        }
+      }
+    }
+  }
+
+  /***/
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP>::ImmutableTree() 
+    : node(Node::terminator.incref()) {
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP>::ImmutableTree(Node *_node) 
+    : node(_node) {
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP>::ImmutableTree(const ImmutableTree &s) 
+    : node(s.node->incref()) {
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP>::~ImmutableTree() {
+    node->decref(); 
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP> &ImmutableTree<K,V,KOV,CMP>::operator=(const ImmutableTree &s) {
+    Node *n = s.node->incref();
+    node->decref();
+    node = n;
+    return *this;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  bool ImmutableTree<K,V,KOV,CMP>::empty() const {
+    return node->isTerminator();
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  size_t ImmutableTree<K,V,KOV,CMP>::count(const key_type &k) const {
+    Node *n = node;
+    while (!n->isTerminator()) {
+      key_type key = key_of_value()(n->value);
+      if (key_compare()(k, key)) {
+        n = n->left;
+      } else if (key_compare()(key, k)) {
+        n = n->right;
+      } else {
+        return 1;
+      }
+    }
+    return 0;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  const typename ImmutableTree<K,V,KOV,CMP>::value_type *
+  ImmutableTree<K,V,KOV,CMP>::lookup(const key_type &k) const {
+    Node *n = node;
+    while (!n->isTerminator()) {
+      key_type key = key_of_value()(n->value);
+      if (key_compare()(k, key)) {
+        n = n->left;
+      } else if (key_compare()(key, k)) {
+        n = n->right;
+      } else {
+        return &n->value;
+      }
+    }
+    return 0;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  const typename ImmutableTree<K,V,KOV,CMP>::value_type *
+  ImmutableTree<K,V,KOV,CMP>::lookup_previous(const key_type &k) const {
+    Node *n = node;
+    Node *result = 0;
+    while (!n->isTerminator()) {
+      key_type key = key_of_value()(n->value);
+      if (key_compare()(k, key)) {
+        n = n->left;
+      } else if (key_compare()(key, k)) {
+        result = n;
+        n = n->right;
+      } else {
+        return &n->value;
+      }
+    }
+    return result ? &result->value : 0;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  const typename ImmutableTree<K,V,KOV,CMP>::value_type &
+  ImmutableTree<K,V,KOV,CMP>::min() const { 
+    Node *n = node;
+    assert(!n->isTerminator());
+    while (!n->left->isTerminator()) n = n->left;
+    return n->value;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  const typename ImmutableTree<K,V,KOV,CMP>::value_type &
+  ImmutableTree<K,V,KOV,CMP>::max() const {
+    Node *n = node;
+    assert(!n->isTerminator());
+    while (!n->right->isTerminator()) n = n->right;
+    return n->value;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  size_t ImmutableTree<K,V,KOV,CMP>::size() const {
+    return node->size();
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP> 
+  ImmutableTree<K,V,KOV,CMP>::insert(const value_type &value) const { 
+    return ImmutableTree(node->insert(value)); 
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP> 
+  ImmutableTree<K,V,KOV,CMP>::replace(const value_type &value) const { 
+    return ImmutableTree(node->replace(value)); 
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP> 
+  ImmutableTree<K,V,KOV,CMP>::remove(const key_type &key) const { 
+    return ImmutableTree(node->remove(key)); 
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP> 
+  ImmutableTree<K,V,KOV,CMP>::popMin(value_type &valueOut) const { 
+    return ImmutableTree(node->popMin(valueOut)); 
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  ImmutableTree<K,V,KOV,CMP> 
+  ImmutableTree<K,V,KOV,CMP>::popMax(value_type &valueOut) const { 
+    return ImmutableTree(node->popMax(valueOut)); 
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  inline typename ImmutableTree<K,V,KOV,CMP>::iterator 
+  ImmutableTree<K,V,KOV,CMP>::begin() const {
+    return iterator(node, true);
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  inline typename ImmutableTree<K,V,KOV,CMP>::iterator 
+  ImmutableTree<K,V,KOV,CMP>::end() const {
+    return iterator(node, false);
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  inline typename ImmutableTree<K,V,KOV,CMP>::iterator 
+  ImmutableTree<K,V,KOV,CMP>::find(const key_type &key) const {
+    iterator end(node,false), it = lower_bound(key);
+    if (it==end || key_compare()(key,key_of_value()(*it))) {
+      return end;
+    } else {
+      return it;
+    }
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  inline typename ImmutableTree<K,V,KOV,CMP>::iterator 
+  ImmutableTree<K,V,KOV,CMP>::lower_bound(const key_type &k) const {
+    // XXX ugh this doesn't have to be so ugly does it?
+    iterator it(node,false);
+    for (Node *root=node; !root->isTerminator();) {
+      it.stack.push_back(root);
+      if (key_compare()(k, key_of_value()(root->value))) {
+        root = root->left;
+      } else if (key_compare()(key_of_value()(root->value), k)) {
+        root = root->right;
+      } else {
+        return it;
+      }
+    }
+    // it is now beginning or first element < k
+    if (!it.stack.empty()) {
+      Node *last = it.stack.back();
+      if (key_compare()(key_of_value()(last->value), k))
+        ++it;
+    }
+    return it;
+  }
+
+  template<class K, class V, class KOV, class CMP>
+  typename ImmutableTree<K,V,KOV,CMP>::iterator 
+  ImmutableTree<K,V,KOV,CMP>::upper_bound(const key_type &key) const {
+    iterator end(node,false),it = lower_bound(key);
+    if (it!=end && 
+        !key_compare()(key,key_of_value()(*it))) // no need to loop, no duplicates
+      ++it;
+    return it;
+  }
+
+}
+
+#endif /* KLEE_IMMUTABLETREE_H */
diff --git a/include/klee/ADT/KTest.h b/include/klee/ADT/KTest.h
new file mode 100644
index 00000000..5b5c45ef
--- /dev/null
+++ b/include/klee/ADT/KTest.h
@@ -0,0 +1,61 @@
+//===-- KTest.h --------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_KTEST_H
+#define KLEE_KTEST_H
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+  typedef struct KTestObject KTestObject;
+  struct KTestObject {
+    char *name;
+    unsigned numBytes;
+    unsigned char *bytes;
+  };
+  
+  typedef struct KTest KTest;
+  struct KTest {
+    /* file format version */
+    unsigned version; 
+    
+    unsigned numArgs;
+    char **args;
+
+    unsigned symArgvs;
+    unsigned symArgvLen;
+
+    unsigned numObjects;
+    KTestObject *objects;
+  };
+
+  
+  /* returns the current .ktest file format version */
+  unsigned kTest_getCurrentVersion();
+  
+  /* return true iff file at path matches KTest header */
+  int   kTest_isKTestFile(const char *path);
+
+  /* returns NULL on (unspecified) error */
+  KTest* kTest_fromFile(const char *path);
+
+  /* returns 1 on success, 0 on (unspecified) error */
+  int   kTest_toFile(KTest *, const char *path);
+  
+  /* returns total number of object bytes */
+  unsigned kTest_numBytes(KTest *);
+
+  void  kTest_free(KTest *);
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif /* KLEE_KTEST_H */
diff --git a/include/klee/ADT/MapOfSets.h b/include/klee/ADT/MapOfSets.h
new file mode 100644
index 00000000..b30934d8
--- /dev/null
+++ b/include/klee/ADT/MapOfSets.h
@@ -0,0 +1,384 @@
+//===-- MapOfSets.h ---------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_MAPOFSETS_H
+#define KLEE_MAPOFSETS_H
+
+#include <cassert>
+#include <vector>
+#include <set>
+#include <map>
+
+// This should really be broken down into TreeOfSets on top of which
+// SetOfSets and MapOfSets are easily implemeted. It should also be
+// parameterized on the underlying set type. Neither are hard to do,
+// just not worth it at the moment.
+//
+// I also broke some STLish conventions because I was bored.
+
+namespace klee {
+
+  /** This implements the UBTree data structure (see Hoffmann and
+      Koehler, "A New Method to Index and Query Sets", IJCAI 1999) */
+  template<class K, class V>
+  class MapOfSets {
+  public:
+    class iterator;
+
+  public:
+    MapOfSets();
+
+    void clear();
+
+    void insert(const std::set<K> &set, const V &value);
+
+    V *lookup(const std::set<K> &set);
+
+    iterator begin();
+    iterator end();
+
+    void subsets(const std::set<K> &set, 
+                 std::vector< std::pair<std::set<K>, V> > &resultOut);
+    void supersets(const std::set<K> &set, 
+                   std::vector< std::pair<std::set<K>, V> > &resultOut);
+    
+    template<class Predicate>
+    V *findSuperset(const std::set<K> &set, const Predicate &p);
+    template<class Predicate>
+    V *findSubset(const std::set<K> &set, const Predicate &p);
+
+  private:
+    class Node;
+
+    Node root;
+
+    template<class Iterator, class Vector>
+    void findSubsets(Node *n, 
+                     const std::set<K> &accum,
+                     Iterator begin, 
+                     Iterator end,
+                     Vector &resultsOut);
+    template<class Iterator, class Vector>
+    void findSupersets(Node *n, 
+                       const std::set<K> &accum,
+                       Iterator begin, 
+                       Iterator end,
+                       Vector &resultsOut);
+    template<class Predicate>
+    V *findSuperset(Node *n, 
+                    typename std::set<K>::iterator begin, 
+                    typename std::set<K>::iterator end,
+                    const Predicate &p);
+    template<class Predicate>
+    V *findSubset(Node *n, 
+                  typename std::set<K>::iterator begin, 
+                  typename std::set<K>::iterator end,
+                  const Predicate &p);
+  };
+
+  /***/
+
+  template<class K, class V>
+  class MapOfSets<K,V>::Node {
+    friend class MapOfSets<K,V>;
+    friend class MapOfSets<K,V>::iterator;
+
+  public:
+    typedef std::map<K, Node> children_ty;
+
+    V value;
+
+  private:
+    bool isEndOfSet;
+    std::map<K, Node> children;
+    
+  public:
+    Node() : value(), isEndOfSet(false) {}
+  };
+  
+  template<class K, class V>
+  class MapOfSets<K,V>::iterator {
+    typedef std::vector< typename std::map<K, Node>::iterator > stack_ty;
+    friend class MapOfSets<K,V>;
+  private:
+    Node *root;
+    bool onEntry;
+    stack_ty stack;
+
+    void step() {
+      if (onEntry) {
+        onEntry = false;
+        Node *n = stack.empty() ? root : &stack.back()->second;
+        while (!n->children.empty()) {
+          stack.push_back(n->children.begin());
+          n = &stack.back()->second;
+          if (n->isEndOfSet) {
+            onEntry = true;
+            return;
+          }
+        } 
+      }
+
+      while (!stack.empty()) {
+        unsigned size = stack.size();
+        Node *at = size==1 ? root : &stack[size-2]->second;
+        typename std::map<K,Node>::iterator &cur = stack.back();
+        ++cur;
+        if (cur==at->children.end()) {
+          stack.pop_back();
+        } else {
+          Node *n = &cur->second;
+
+          while (!n->isEndOfSet) {
+            assert(!n->children.empty());
+            stack.push_back(n->children.begin());
+            n = &stack.back()->second;
+          }
+
+          onEntry = true;
+          break;
+        }
+      } 
+    }
+
+  public:
+    // end()
+    iterator() : onEntry(false) {} 
+    // begin()
+    iterator(Node *_n) : root(_n), onEntry(true) {
+      if (!root->isEndOfSet)
+        step();
+    }
+
+    const std::pair<const std::set<K>, const V> operator*() {
+      assert(onEntry || !stack.empty());
+      std::set<K> s;
+      for (typename stack_ty::iterator it = stack.begin(), ie = stack.end();
+           it != ie; ++it)
+        s.insert((*it)->first);
+      Node *n = stack.empty() ? root : &stack.back()->second;
+      return std::make_pair(s, n->value);
+    }
+
+    bool operator==(const iterator &b) {
+      return onEntry==b.onEntry && stack==b.stack;
+    }
+    bool operator!=(const iterator &b) {
+      return !(*this==b);
+    }
+
+    iterator &operator++() {
+      step();
+      return *this;
+    }
+  };
+
+  /***/
+
+  template<class K, class V>
+  MapOfSets<K,V>::MapOfSets() {}  
+
+  template<class K, class V>
+  void MapOfSets<K,V>::insert(const std::set<K> &set, const V &value) {
+    Node *n = &root;
+    for (auto const& element : set) {
+      n = &n->children.insert(std::make_pair(element, Node())).first->second;
+    }
+    n->isEndOfSet = true;
+    n->value = value;
+  }
+
+  template<class K, class V>
+  V *MapOfSets<K,V>::lookup(const std::set<K> &set) {
+    Node *n = &root;
+    for (typename std::set<K>::const_iterator it = set.begin(), ie = set.end();
+         it != ie; ++it) {
+      typename Node::children_ty::iterator kit = n->children.find(*it);
+      if (kit==n->children.end()) {
+        return 0;
+      } else {
+        n = &kit->second;
+      }
+    }
+    if (n->isEndOfSet) {
+      return &n->value;
+    } else {
+      return 0;
+    }
+  }
+
+  template<class K, class V>
+  typename MapOfSets<K,V>::iterator 
+  MapOfSets<K,V>::begin() { return iterator(&root); }
+  
+  template<class K, class V>
+  typename MapOfSets<K,V>::iterator 
+  MapOfSets<K,V>::end() { return iterator(); }
+
+  template<class K, class V>
+  template<class Iterator, class Vector>
+  void MapOfSets<K,V>::findSubsets(Node *n, 
+                                  const std::set<K> &accum,
+                                  Iterator begin, 
+                                  Iterator end,
+                                  Vector &resultsOut) {
+    if (n->isEndOfSet) {
+      resultsOut.push_back(std::make_pair(accum, n->value));
+    }
+    
+    for (Iterator it=begin; it!=end;) {
+      K elt = *it;
+      typename Node::children_ty::iterator kit = n->children.find(elt);
+      it++;
+      if (kit!=n->children.end()) {
+        std::set<K> nacc = accum;
+        nacc.insert(elt);
+        findSubsets(&kit->second, nacc, it, end, resultsOut);
+      }
+    }
+  }
+
+  template<class K, class V>
+  void MapOfSets<K,V>::subsets(const std::set<K> &set,
+                               std::vector< std::pair<std::set<K>, 
+                                                      V> > &resultOut) {
+    findSubsets(&root, std::set<K>(), set.begin(), set.end(), resultOut);
+  }
+
+  template<class K, class V>
+  template<class Iterator, class Vector>
+  void MapOfSets<K,V>::findSupersets(Node *n, 
+                                     const std::set<K> &accum,
+                                     Iterator begin, 
+                                     Iterator end,
+                                     Vector &resultsOut) {
+    if (begin==end) {
+      if (n->isEndOfSet)
+        resultsOut.push_back(std::make_pair(accum, n->value));
+      for (typename Node::children_ty::iterator it = n->children.begin(),
+             ie = n->children.end(); it != ie; ++it) {
+        std::set<K> nacc = accum;
+        nacc.insert(it->first);
+        findSupersets(&it->second, nacc, begin, end, resultsOut);
+      }
+    } else {
+      K elt = *begin;
+      Iterator next = begin;
+      ++next;
+      for (typename Node::children_ty::iterator it = n->children.begin(),
+             ie = n->children.end(); it != ie; ++it) {
+        std::set<K> nacc = accum;
+        nacc.insert(it->first);
+        if (elt==it->first) {
+          findSupersets(&it->second, nacc, next, end, resultsOut);
+        } else if (it->first<elt) {
+          findSupersets(&it->second, nacc, begin, end, resultsOut);
+        } else {
+          break;
+        }
+      }
+    }
+  }
+
+  template<class K, class V>
+  void MapOfSets<K,V>::supersets(const std::set<K> &set,
+                               std::vector< std::pair<std::set<K>, V> > &resultOut) {
+    findSupersets(&root, std::set<K>(), set.begin(), set.end(), resultOut);
+  }
+
+  template<class K, class V>
+  template<class Predicate>
+  V *MapOfSets<K,V>::findSubset(Node *n, 
+                                typename std::set<K>::iterator begin, 
+                                typename std::set<K>::iterator end,
+                                const Predicate &p) {   
+    if (n->isEndOfSet && p(n->value)) {
+      return &n->value;
+    } else if (begin==end) {
+      return 0;
+    } else {
+      typename Node::children_ty::iterator kend = n->children.end();
+      typename Node::children_ty::iterator 
+        kbegin = n->children.lower_bound(*begin);
+      typename std::set<K>::iterator it = begin;
+      if (kbegin==kend)
+        return 0;
+      for (;;) { // kbegin!=kend && *it <= kbegin->first
+        while (*it < kbegin->first) {
+          ++it;
+          if (it==end)
+            return 0;
+        }
+        if (*it == kbegin->first) {
+          ++it;
+          V *res = findSubset(&kbegin->second, it, end, p);
+          if (res || it==end)
+            return res;
+        }
+        while (kbegin->first < *it) {
+          ++kbegin;
+          if (kbegin==kend)
+            return 0;
+        }
+      }
+    }
+  }
+  
+  template<class K, class V>
+  template<class Predicate>
+  V *MapOfSets<K,V>::findSuperset(Node *n, 
+                                  typename std::set<K>::iterator begin, 
+                                  typename std::set<K>::iterator end,
+                                  const Predicate &p) {   
+    if (begin==end) {
+      if (n->isEndOfSet && p(n->value))
+        return &n->value;
+      for (typename Node::children_ty::iterator it = n->children.begin(),
+             ie = n->children.end(); it != ie; ++it) {
+        V *res = findSuperset(&it->second, begin, end, p);
+        if (res) return res;
+      }
+    } else {
+      typename Node::children_ty::iterator kmid = 
+        n->children.lower_bound(*begin);
+      for (typename Node::children_ty::iterator it = n->children.begin(),
+             ie = n->children.end(); it != ie; ++it) {
+        V *res = findSuperset(&it->second, begin, end, p);
+        if (res) return res;
+      }
+      if (kmid!=n->children.end() && *begin==kmid->first) {
+        V *res = findSuperset(&kmid->second, ++begin, end, p);
+        if (res) return res;
+      }
+    }
+    return 0;
+  }
+
+  template<class K, class V>
+  template<class Predicate>
+  V *MapOfSets<K,V>::findSuperset(const std::set<K> &set, const Predicate &p) {    
+    return findSuperset(&root, set.begin(), set.end(), p);
+  }
+
+  template<class K, class V>
+  template<class Predicate>
+  V *MapOfSets<K,V>::findSubset(const std::set<K> &set, const Predicate &p) {    
+    return findSubset(&root, set.begin(), set.end(), p);
+  }
+
+  template<class K, class V>
+  void MapOfSets<K,V>::clear() {
+    root.isEndOfSet = false;
+    root.value = V();
+    root.children.clear();
+  }
+
+}
+
+#endif /* KLEE_MAPOFSETS_H */
diff --git a/include/klee/ADT/RNG.h b/include/klee/ADT/RNG.h
new file mode 100644
index 00000000..5ea375b5
--- /dev/null
+++ b/include/klee/ADT/RNG.h
@@ -0,0 +1,50 @@
+//===-- RNG.h ---------------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_RNG_H
+#define KLEE_RNG_H
+
+namespace klee {
+  class RNG {
+  private:
+    /* Period parameters */  
+    static const int N = 624;
+    static const int M = 397;
+    static const unsigned int MATRIX_A = 0x9908b0dfUL;   /* constant vector a */
+    static const unsigned int UPPER_MASK = 0x80000000UL; /* most significant w-r bits */
+    static const unsigned int LOWER_MASK = 0x7fffffffUL; /* least significant r bits */
+      
+  private:
+    unsigned int mt[N]; /* the array for the state vector  */
+    int mti;
+    
+  public:
+    RNG(unsigned int seed=5489UL);
+  
+    void seed(unsigned int seed);
+    
+    /* generates a random number on [0,0xffffffff]-interval */
+    unsigned int getInt32();
+    /* generates a random number on [0,0x7fffffff]-interval */
+    int getInt31();
+    /* generates a random number on [0,1]-real-interval */
+    double getDoubleLR();
+    float getFloatLR();
+    /* generates a random number on [0,1)-real-interval */
+    double getDoubleL();
+    float getFloatL();
+    /* generates a random number on (0,1)-real-interval */
+    double getDouble();
+    float getFloat();
+    /* generators a random flop */
+    bool getBool();
+  };
+}
+
+#endif /* KLEE_RNG_H */
diff --git a/include/klee/ADT/TreeStream.h b/include/klee/ADT/TreeStream.h
new file mode 100644
index 00000000..32c856c9
--- /dev/null
+++ b/include/klee/ADT/TreeStream.h
@@ -0,0 +1,76 @@
+//===-- TreeStream.h --------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_TREESTREAM_H
+#define KLEE_TREESTREAM_H
+
+#include <string>
+#include <vector>
+
+namespace klee {
+
+  typedef unsigned TreeStreamID;
+  class TreeOStream;
+
+  class TreeStreamWriter {
+    static const unsigned bufferSize = 4*4096;
+
+    friend class TreeOStream;
+
+  private:
+    char buffer[bufferSize];
+    unsigned lastID, bufferCount;
+
+    std::string path;
+    std::ofstream *output;
+    unsigned ids;
+
+    void write(TreeOStream &os, const char *s, unsigned size);
+    void flushBuffer();
+
+  public:
+    TreeStreamWriter(const std::string &_path);
+    ~TreeStreamWriter();
+
+    bool good();
+
+    TreeOStream open();
+    TreeOStream open(const TreeOStream &node);
+
+    void flush();
+
+    // hack, to be replace by proper stream capabilities
+    void readStream(TreeStreamID id,
+                    std::vector<unsigned char> &out);
+  };
+
+  class TreeOStream {
+    friend class TreeStreamWriter;
+
+  private:
+    TreeStreamWriter *writer;
+    unsigned id;
+    
+    TreeOStream(TreeStreamWriter &_writer, unsigned _id);
+
+  public:
+    TreeOStream();
+    ~TreeOStream();
+
+    unsigned getID() const;
+
+    void write(const char *buffer, unsigned size);
+
+    TreeOStream &operator<<(const std::string &s);
+
+    void flush();
+  };
+}
+
+#endif /* KLEE_TREESTREAM_H */