+
+// A simple chunked vector class--this is a subset of std::vector
+// which stores memory in chunks. We don't provide iterators, because
+// we don't need them.
+
+template<typename Element>
+class Chunked_vector
+{
+ public:
+ Chunked_vector()
+ : chunks_()
+ { }
+
+ // Clear the elements.
+ void
+ clear()
+ { this->chunks_.clear(); }
+
+ // Reserve elements.
+ void
+ reserve(unsigned int n)
+ {
+ n += chunk_size - 1;
+ while (n >= chunk_size)
+ {
+ this->chunks_.push_back(Element_vector());
+ this->chunks_.back().reserve(chunk_size);
+ n -= chunk_size;
+ }
+ }
+
+ // Get the number of elements.
+ size_t
+ size() const
+ {
+ if (this->chunks_.empty())
+ return 0;
+ else
+ return ((this->chunks_.size() - 1) * chunk_size
+ + this->chunks_.back().size());
+ }
+
+ // Push a new element on the back of the vector.
+ void
+ push_back(const Element& element)
+ {
+ if (this->chunks_.empty() || this->chunks_.back().size() == chunk_size)
+ {
+ this->chunks_.push_back(Element_vector());
+ this->chunks_.back().reserve(chunk_size);
+ }
+ this->chunks_.back().push_back(element);
+ }
+
+ // Return a reference to an entry in the vector.
+ Element&
+ operator[](size_t i)
+ { return this->chunks_[i / chunk_size][i % chunk_size]; }
+
+ const Element&
+ operator[](size_t i) const
+ { return this->chunks_[i / chunk_size][i % chunk_size]; }
+
+ private:
+ static const unsigned int chunk_size = 8192;
+
+ typedef std::vector<Element> Element_vector;
+ typedef std::vector<Element_vector> Chunk_vector;
+
+ Chunk_vector chunks_;
+};
+
+