Remove CDChunkList (#1414)

2 files changed, 0 insertions, 496 deletions

diff --git a/src/context/cdchunk_list.h b/src/context/cdchunk_list.h
deleted file mode 100644
index d13c6ab90..000000000
--- a/src/context/cdchunk_list.h
+++ /dev/null
@@ -1,495 +0,0 @@
-/*********************                                                        */
-/*! \file cdchunk_list.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Context-dependent list class designed for use with a
- ** context memory allocator.
- **
- ** Context-dependent list class designed for use with a context
- ** memory allocator.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__CONTEXT__CDCHUNK_LIST_H
-#define __CVC4__CONTEXT__CDCHUNK_LIST_H
-
-#include <iterator>
-#include <memory>
-
-#include "base/cvc4_assert.h"
-#include "context/context.h"
-#include "context/context_mm.h"
-
-
-namespace CVC4 {
-namespace context {
-
-/**
- * Generic context-dependent dynamic array.  Like the usual CDList<>,
- * but allocates all memory from context memory.  Elements are kept in
- * cascading "list segments."  Access to elements by operator[] is not O(1) but
- * O(log n).  As with CDList<>, update is not permitted, only
- * appending to the end of the list.
- */
-template <class T>
-class CDChunkList : public ContextObj {
-public:
-
-  /** The value type with which this CDChunkList<> was instantiated. */
-  typedef T value_type;
-  /** The allocator type with which this CDChunkList<> was instantiated. */
-  typedef ContextMemoryAllocator<T> Allocator;
-
-protected:
-
-  static const size_t INITIAL_SEGMENT_SIZE = 10;
-  static const size_t INCREMENTAL_GROWTH_FACTOR = 2;
-
-  /**
-   * ListSegment is itself allocated in Context memory, but it is
-   * never updated; it serves as information about the d_list segment
-   * pointer it contains only.
-   */
-  class ListSegment {
-    ListSegment* d_nextSegment;
-    size_t d_segmentSize;
-    T* d_list;
-  public:
-    ListSegment() :
-      d_nextSegment(NULL),
-      d_segmentSize(0),
-      d_list(NULL) {
-    }
-    void initialize(T* list) {
-      Assert( d_nextSegment == NULL &&
-              d_segmentSize == 0 &&
-              d_list == NULL,
-              "Double-initialization of ListSegment not permitted" );
-      d_list = list;
-    }
-    void linkTo(ListSegment* nextSegment) {
-      Assert( d_nextSegment == NULL,
-              "Double-linking of ListSegment not permitted" );
-      d_nextSegment = nextSegment;
-    }
-    void cutLink() {
-      d_nextSegment = NULL;
-    }
-    ListSegment* getNextSegment() const { return d_nextSegment; }
-    size_t& size() { return d_segmentSize; }
-    size_t size() const { return d_segmentSize; }
-    const T* list() const { return d_list; }
-    T& operator[](size_t i) { return d_list[i]; }
-    const T& operator[](size_t i) const { return d_list[i]; }
-  };/* struct CDChunkList<T>::ListSegment */
-
-  /**
-   * The first segment of list memory.
-   */
-  ListSegment d_headSegment;
-
-  /**
-   * A pointer to the final segment of list memory.
-   */
-  ListSegment* d_tailSegment;
-
-  /**
-   * Whether to call the destructor when items are popped from the
-   * list.  True by default, but can be set to false by setting the
-   * second argument in the constructor to false.
-   */
-  bool d_callDestructor;
-
-  /**
-   * Number of objects in list across all segments.
-   */
-  size_t d_size;
-
-  /**
-   * Total allocated size across all segments.
-   */
-  size_t d_totalSizeAlloc;
-
-  /**
-   * Our allocator.
-   */
-  Allocator d_allocator;
-
-  /**
-   * Lightweight save object for CDChunkList<T, ContextMemoryAllocator<T> >.
-   */
-  struct CDChunkListSave : public ContextObj {
-    ListSegment* d_tail;
-    size_t d_tailSize, d_size, d_sizeAlloc;
-    CDChunkListSave(const CDChunkList<T>& list, ListSegment* tail,
-               size_t size, size_t sizeAlloc) :
-      ContextObj(list),
-      d_tail(tail),
-      d_tailSize(tail->size()),
-      d_size(size),
-      d_sizeAlloc(sizeAlloc) {
-    }
-    ~CDChunkListSave() {
-      this->destroy();
-    }
-    ContextObj* save(ContextMemoryManager* pCMM) {
-      // This type of object _is_ the save/restore object.  It isn't
-      // itself saved or restored.
-      Unreachable();
-    }
-    void restore(ContextObj* data) {
-      // This type of object _is_ the save/restore object.  It isn't
-      // itself saved or restored.
-      Unreachable();
-    }
-  };/* struct CDChunkList<T>::CDChunkListSave */
-
-  /**
-   * Private copy constructor undefined (no copy permitted).
-   */
-  CDChunkList(const CDChunkList<T>& l) CVC4_UNDEFINED;
-
-  /**
-   * Allocate the first list segment.
-   */
-  void allocateHeadSegment() {
-    Assert(d_headSegment.list() == NULL);
-    Assert(d_totalSizeAlloc == 0 && d_size == 0);
-
-    // Allocate an initial list if one does not yet exist
-    size_t newSize = INITIAL_SEGMENT_SIZE;
-    Debug("cdlist:cmm") << "initial grow of cdlist " << this
-                        << " level " << getContext()->getLevel()
-                        << " to " << newSize << std::endl;
-    if(newSize > d_allocator.max_size()) {
-      newSize = d_allocator.max_size();
-    }
-    T* newList = d_allocator.allocate(newSize);
-    if(newList == NULL) {
-      throw std::bad_alloc();
-    }
-    d_totalSizeAlloc = newSize;
-    d_headSegment.initialize(newList);
-  }
-
-  /**
-   * Allocate a new segment with more space.
-   * Throws bad_alloc if memory allocation fails.
-   */
-  void grow() {
-    Assert(d_totalSizeAlloc == d_size);
-
-    // Allocate a new segment
-    typedef typename Allocator::template rebind<ListSegment>::other
-      SegmentAllocator;
-    ContextMemoryManager* cmm = d_allocator.getCMM();
-    SegmentAllocator segAllocator = SegmentAllocator(cmm);
-    ListSegment* newSegment = segAllocator.allocate(1);
-    if(newSegment == NULL) {
-      throw std::bad_alloc();
-    }
-    segAllocator.construct(newSegment, ListSegment());
-    size_t newSize = INCREMENTAL_GROWTH_FACTOR * d_totalSizeAlloc;
-    if(newSize > d_allocator.max_size()) {
-      newSize = d_allocator.max_size();
-    }
-    T* newList = d_allocator.allocate(newSize);
-    Debug("cdlist:cmm") << "new segment of cdlistcontext " << this
-                        << " level " << getContext()->getLevel()
-                        << " to " << newSize
-                        << " (from " << d_tailSegment->list()
-                        << " to " << newList << ")" << std::endl;
-    if(newList == NULL) {
-      throw std::bad_alloc();
-    }
-    d_tailSegment->linkTo(newSegment);
-    d_tailSegment = newSegment;
-    d_tailSegment->initialize(newList);
-    d_totalSizeAlloc += newSize;
-  }
-
-  /**
-   * Implementation of mandatory ContextObj method save: simply copies the
-   * current size to a copy using the copy constructor (the pointer and the
-   * allocated size are *not* copied as they are not restored on a pop).
-   * The saved information is allocated using the ContextMemoryManager.
-   */
-  ContextObj* save(ContextMemoryManager* pCMM) {
-    ContextObj* data = new(pCMM) CDChunkListSave(*this, d_tailSegment,
-                                            d_size, d_totalSizeAlloc);
-    Debug("cdlist:cmm") << "save " << this
-                        << " at level " << this->getContext()->getLevel()
-                        << " size at " << this->d_size
-                        << " totalSizeAlloc at " << this->d_totalSizeAlloc
-                        << " data:" << data << std::endl;
-    return data;
-  }
-
-  /**
-   * Implementation of mandatory ContextObj method restore: simply restores the
-   * previous size.  Note that the list pointer and the allocated size are not
-   * changed.
-   */
-  void restore(ContextObj* data) {
-    CDChunkListSave* save = static_cast<CDChunkListSave*>(data);
-    Debug("cdlist:cmm") << "restore " << this
-                        << " level " << this->getContext()->getLevel()
-                        << " data == " << data
-                        << " call dtor == " << this->d_callDestructor
-                        << " d_tail == " << this->d_tailSegment << std::endl;
-    if(this->d_callDestructor) {
-      ListSegment* seg = &d_headSegment;
-      size_t i = save->d_size;
-      while(i >= seg->size()) {
-        i -= seg->size();
-        seg = seg->getNextSegment();
-      }
-      do {
-        while(i < seg->size()) {
-          this->d_allocator.destroy(&(*seg)[i++]);
-        }
-        i = 0;
-      } while((seg = seg->getNextSegment()) != NULL);
-    }
-
-    this->d_size = save->d_size;
-    this->d_tailSegment = save->d_tail;
-    this->d_tailSegment->size() = save->d_tailSize;
-    this->d_tailSegment->cutLink();
-    this->d_totalSizeAlloc = save->d_sizeAlloc;
-    Debug("cdlist:cmm") << "restore " << this
-                        << " level " << this->getContext()->getLevel()
-                        << " size back to " << this->d_size
-                        << " totalSizeAlloc at " << this->d_totalSizeAlloc
-                        << std::endl;
-  }
-
-public:
-
-  CDChunkList(Context* context, bool callDestructor, const Allocator& alloc) :
-    ContextObj(context),
-    d_headSegment(),
-    d_tailSegment(&d_headSegment),
-    d_callDestructor(callDestructor),
-    d_size(0),
-    d_totalSizeAlloc(0),
-    d_allocator(alloc) {
-    allocateHeadSegment();
-  }
-
-  CDChunkList(Context* context, bool callDestructor = true) :
-    ContextObj(context),
-    d_headSegment(),
-    d_tailSegment(&d_headSegment),
-    d_callDestructor(callDestructor),
-    d_size(0),
-    d_totalSizeAlloc(0),
-    d_allocator(Allocator(context->getCMM())) {
-    allocateHeadSegment();
-  }
-
-  CDChunkList(bool allocatedInCMM, Context* context, bool callDestructor,
-         const Allocator& alloc) :
-    ContextObj(allocatedInCMM, context),
-    d_headSegment(),
-    d_tailSegment(&d_headSegment),
-    d_callDestructor(callDestructor),
-    d_size(0),
-    d_totalSizeAlloc(0),
-    d_allocator(alloc) {
-    allocateHeadSegment();
-  }
-
-  CDChunkList(bool allocatedInCMM, Context* context, bool callDestructor = true) :
-    ContextObj(allocatedInCMM, context),
-    d_headSegment(),
-    d_tailSegment(&d_headSegment),
-    d_callDestructor(callDestructor),
-    d_size(0),
-    d_totalSizeAlloc(0),
-    d_allocator(Allocator(context->getCMM())) {
-    allocateHeadSegment();
-  }
-
-  /**
-   * Destructor: delete the list
-   */
-  ~CDChunkList() {
-    this->destroy();
-
-    if(this->d_callDestructor) {
-      for(ListSegment* segment = &d_headSegment;
-          segment != NULL;
-          segment = segment->getNextSegment()) {
-        for(size_t i = 0; i < segment->size(); ++i) {
-          this->d_allocator.destroy(&(*segment)[i]);
-        }
-      }
-    }
-  }
-
-  /**
-   * Return the current size of (i.e. valid number of objects in) the
-   * list.
-   */
-  size_t size() const {
-    return d_size;
-  }
-
-  /**
-   * Return true iff there are no valid objects in the list.
-   */
-  bool empty() const {
-    return d_size == 0;
-  }
-
-  /**
-   * Add an item to the end of the list.
-   */
-  void push_back(const T& data) {
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " level " << getContext()->getLevel()
-                        << ": make-current, "
-                        << "d_list == " << d_tailSegment->list() << std::endl;
-    makeCurrent();
-
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " level " << getContext()->getLevel()
-                        << ": grow? " << d_size
-                        << " size_alloc " << d_totalSizeAlloc
-                        << std::endl;
-
-    if(d_size == d_totalSizeAlloc) {
-      Debug("cdlist:cmm") << "push_back " << this
-                          << " " << getContext()->getLevel()
-                          << ": grow!\n";
-      grow();
-    }
-    Assert(d_size < d_totalSizeAlloc);
-
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " " << getContext()->getLevel()
-                        << ": construct! at [" << d_size << "] == "
-                        << &(*d_tailSegment)[d_tailSegment->size()]
-                        << std::endl;
-    d_allocator.construct(&(*d_tailSegment)[d_tailSegment->size()], data);
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " " << getContext()->getLevel()
-                        << ": done..." << std::endl;
-    ++d_tailSegment->size();
-    ++d_size;
-    Debug("cdlist:cmm") << "push_back " << this
-                        << " " << getContext()->getLevel()
-                        << ": size now " << d_size << std::endl;
-  }
-
-  /**
-   * Access to the ith item in the list in O(log n).
-   */
-  const T& operator[](size_t i) const {
-    Assert(i < d_size, "index out of bounds in CDChunkList::operator[]");
-    const ListSegment* seg = &d_headSegment;
-    while(i >= seg->size()) {
-      i -= seg->size();
-      seg = seg->getNextSegment();
-    }
-    return (*seg)[i];
-  }
-
-  /**
-   * Returns the most recent item added to the list.
-   */
-  const T& back() const {
-    Assert(d_size > 0, "CDChunkList::back() called on empty list");
-    return (*d_tailSegment)[d_tailSegment->size() - 1];
-  }
-
-  /**
-   * Iterator for CDChunkList class.  It has to be const because we don't
-   * allow items in the list to be changed.  It's a straightforward
-   * wrapper around a pointer.  Note that for efficiency, we implement
-   * only prefix increment and decrement.  Also note that it's OK to
-   * create an iterator from an empty, uninitialized list, as begin()
-   * and end() will have the same value (NULL).
-   */
-  class const_iterator {
-    const ListSegment* d_segment;
-    size_t d_index;
-
-    const_iterator(const ListSegment* segment, size_t i) :
-      d_segment(segment),
-      d_index(i) {
-    }
-
-    friend class CDChunkList<T>;
-
-  public:
-
-    typedef std::input_iterator_tag iterator_category;
-    typedef T value_type;
-    typedef std::ptrdiff_t difference_type;
-    typedef const T* pointer;
-    typedef const T& reference;
-
-    const_iterator() : d_segment(NULL), d_index(0) {}
-
-    inline bool operator==(const const_iterator& i) const {
-      return d_segment == i.d_segment && d_index == i.d_index;
-    }
-
-    inline bool operator!=(const const_iterator& i) const {
-      return !(*this == i);
-    }
-
-    inline const T& operator*() const {
-      return (*d_segment)[d_index];
-    }
-
-    /** Prefix increment */
-    const_iterator& operator++() {
-      if(++d_index >= d_segment->size()) {
-        d_segment = d_segment->getNextSegment();
-        d_index = 0;
-      }
-      return *this;
-    }
-
-    /** Postfix increment: returns new iterator with the old value. */
-    const_iterator operator++(int) {
-      const_iterator i = *this;
-      ++(*this);
-      return i;
-    }
-  };/* class CDChunkList<>::const_iterator */
-
-  /**
-   * Returns an iterator pointing to the first item in the list.
-   */
-  const_iterator begin() const {
-    // This looks curious, but we have to make sure that begin() == end()
-    // for an empty list, and begin() == (head,0) for a nonempty one.
-    // Since the segment spill-over is implemented in
-    // iterator::operator++(), let's reuse it. */
-    return ++const_iterator(&d_headSegment, -1);
-  }
-
-  /**
-   * Returns an iterator pointing one past the last item in the list.
-   */
-  const_iterator end() const {
-    return const_iterator(NULL, 0);
-  }
-};/* class CDChunkList<T, ContextMemoryAllocator<T> > */
-
-}/* CVC4::context namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__CONTEXT__CDCHUNK_LIST_H */
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 3dab675c3..aeb6567a3 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -419,7 +419,6 @@ public:
 template <class T, class CleanUp>
 class CDList<T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj {
   /* CDList is incompatible for use with a ContextMemoryAllocator.
-   * Consider using CDChunkList<T> instead.
    *
    * Explanation:
    * If ContextMemoryAllocator is used and d_list grows at a deeper context