Remove CDChunkList (#1414)

26 files changed, 97 insertions, 708 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 6a21251bd..69e9cd014 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -36,7 +36,6 @@ libcvc4_la_SOURCES = \
 	git_versioninfo.cpp \
 	svn_versioninfo.cpp \
 	context/backtrackable.h \
-	context/cdchunk_list.h \
 	context/cddense_set.h \
 	context/cdhashmap.h \
 	context/cdhashmap_forward.h \
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
diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 9cfa7355d..099b45fec 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -22,9 +22,9 @@
 #include <iostream>
 #include <map>
 
-#include "context/cdchunk_list.h"
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
+#include "context/cdlist.h"
 #include "context/cdo.h"
 #include "context/context.h"
 #include "expr/datatype.h"
@@ -59,7 +59,6 @@ private:
   typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap;
   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-  typedef context::CDChunkList<Node> NodeList;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
   IntMap d_testers;
   IntMap d_is_const;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 5166e118e..3c0a7c7cf 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -22,13 +22,13 @@
 #include <iostream>
 #include <map>
 
-#include "context/cdchunk_list.h"
+#include "context/cdlist.h"
+#include "expr/attribute.h"
 #include "expr/datatype.h"
 #include "theory/datatypes/datatypes_sygus.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 #include "util/hash.h"
-#include "expr/attribute.h"
 
 namespace CVC4 {
 namespace theory {
@@ -40,24 +40,25 @@ namespace quantifiers{
 namespace datatypes {
 
 class TheoryDatatypes : public Theory {
-private:
-  typedef context::CDChunkList<Node> NodeList;
-  typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
-  typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-  typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
+ private:
+  typedef context::CDList<Node> NodeList;
+  typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+  typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
 
   /** transitive closure to record equivalence/subterm relation.  */
-  //TransitiveClosureNode d_cycle_check;
+  // TransitiveClosureNode d_cycle_check;
   /** has seen cycle */
-  context::CDO< bool > d_hasSeenCycle;
+  context::CDO<bool> d_hasSeenCycle;
   /** inferences */
   NodeList d_infer;
   NodeList d_infer_exp;
   Node d_true;
   Node d_zero;
   /** mkAnd */
-  Node mkAnd( std::vector< TNode >& assumptions );
-private:
+  Node mkAnd(std::vector<TNode>& assumptions);
+
+ private:
   //notification class for equality engine
   class NotifyClass : public eq::EqualityEngineNotify {
     TheoryDatatypes& d_dt;
diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index a91b04ab3..99d77a8e7 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -23,7 +23,6 @@
 
 #include "context/context.h"
 #include "context/context_mm.h"
-#include "context/cdchunk_list.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/ce_guided_pbe.h b/src/theory/quantifiers/ce_guided_pbe.h
index 8cfed253c..e8bccaac5 100644
--- a/src/theory/quantifiers/ce_guided_pbe.h
+++ b/src/theory/quantifiers/ce_guided_pbe.h
@@ -18,7 +18,6 @@
 #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_PBE_H
 
 #include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 33fc7303f..888e078af 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -17,8 +17,7 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
 #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
 
-#include "context/cdchunk_list.h"
-#include "context/cdhashmap.h"
+#include "context/cdlist.h"
 #include "theory/quantifiers/ce_guided_single_inv_sol.h"
 #include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/inst_strategy_cbqi.h"
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h
index 61ade265f..c5f976f02 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h
@@ -18,7 +18,6 @@
 #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H
 
 #include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index a67530556..fa74795c3 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -18,7 +18,6 @@
 #define CONJECTURE_GENERATOR_H
 
 #include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/type_enumerator.h"
 
@@ -229,7 +228,6 @@ class ConjectureGenerator : public QuantifiersModule
   friend class SubsEqcIndex;
   friend class TermGenerator;
   friend class TermGenEnv;
-  typedef context::CDChunkList<Node> NodeList;
   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
 //this class maintains a congruence closure for *universal* facts
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h
index 5b714c2d3..5a3f2e4d5 100644
--- a/src/theory/quantifiers/equality_infer.h
+++ b/src/theory/quantifiers/equality_infer.h
@@ -21,11 +21,10 @@
 #include <map>
 #include <vector>
 
-#include "context/context.h"
-#include "context/context_mm.h"
 #include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
 #include "context/cdhashset.h"
+#include "context/context.h"
+#include "context/context_mm.h"
 #include "theory/theory.h"
 
 
@@ -37,7 +36,7 @@ class EqualityInference
 {
   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-  typedef context::CDChunkList<Node> NodeList;
+  typedef context::CDList<Node> NodeList;
   typedef context::CDHashMap< Node, int, NodeHashFunction > NodeIntMap;
 private:
   context::Context * d_c;
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 8a1043ded..f4d0e8e43 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -21,9 +21,9 @@
 #include <vector>
 
 #include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
-#include "theory/quantifiers_engine.h"
+#include "context/cdlist.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
@@ -191,7 +191,6 @@ class QuantConflictFind : public QuantifiersModule
 {
   friend class MatchGen;
   friend class QuantInfo;
-  typedef context::CDChunkList<Node> NodeList;
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 private:
   context::CDO< bool > d_conflict;
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 5d1918205..d56e7c730 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -18,7 +18,6 @@
 #ifndef __CVC4__REWRITE_ENGINE_H
 #define __CVC4__REWRITE_ENGINE_H
 
-#include "context/cdchunk_list.h"
 #include "context/context.h"
 #include "context/context_mm.h"
 #include "theory/quantifiers/trigger.h"
diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h
index 466e6d9a9..091490cec 100644
--- a/src/theory/quantifiers/symmetry_breaking.h
+++ b/src/theory/quantifiers/symmetry_breaking.h
@@ -22,7 +22,6 @@
 #include <string>
 #include <vector>
 
-#include "context/cdchunk_list.h"
 #include "context/cdhashmap.h"
 #include "context/context.h"
 #include "context/context_mm.h"
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 6c7820cef..3cd4e8ef9 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -22,8 +22,8 @@
 #include <memory>
 #include <unordered_map>
 
-#include "context/cdchunk_list.h"
 #include "context/cdhashset.h"
+#include "context/cdlist.h"
 #include "expr/attribute.h"
 #include "options/quantifiers_modes.h"
 #include "theory/quantifiers/inst_match.h"
@@ -95,8 +95,8 @@ class QuantifiersEngine {
   friend class quantifiers::QuantConflictFind;
   friend class inst::InstMatch;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-  typedef context::CDChunkList<Node> NodeList;
-  typedef context::CDChunkList<bool> BoolList;
+  typedef context::CDList<Node> NodeList;
+  typedef context::CDList<bool> BoolList;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 private:
   /** reference to theory engine object */
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 1786584d4..591a495d0 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -19,13 +19,13 @@
 #ifndef __CVC4__THEORY__SEP__THEORY_SEP_H
 #define __CVC4__THEORY__SEP__THEORY_SEP_H
 
-#include "theory/theory.h"
-#include "util/statistics_registry.h"
-#include "theory/uf/equality_engine.h"
-#include "context/cdchunk_list.h"
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
+#include "context/cdlist.h"
 #include "context/cdqueue.h"
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -35,7 +35,7 @@ class TheoryModel;
 namespace sep {
 
 class TheorySep : public Theory {
-  typedef context::CDChunkList<Node> NodeList;
+  typedef context::CDList<Node> NodeList;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index eb97405dc..d6e52a308 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -19,8 +19,8 @@
 
 #include <unordered_set>
 
-#include "context/cdchunk_list.h"
 #include "context/cdhashset.h"
+#include "context/cdlist.h"
 #include "theory/sets/rels_utils.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -46,8 +46,7 @@ public:
 };/* class TupleTrie */
 
 class TheorySetsRels {
-
-  typedef context::CDChunkList< Node >                            NodeList;
+  typedef context::CDList<Node> NodeList;
   typedef context::CDHashSet< Node, NodeHashFunction >            NodeSet;
   typedef context::CDHashMap< Node, Node, NodeHashFunction >      NodeMap;
 
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 0bdaf7ab5..39ab70e2f 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -19,14 +19,13 @@
 #ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
 #define __CVC4__THEORY__STRINGS__THEORY_STRINGS_H
 
-#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/strings/theory_strings_preprocess.h"
-#include "theory/strings/regexp_operation.h"
-
-#include "context/cdchunk_list.h"
 #include "context/cdhashset.h"
+#include "context/cdlist.h"
 #include "expr/attribute.h"
+#include "theory/strings/regexp_operation.h"
+#include "theory/strings/theory_strings_preprocess.h"
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
 
 #include <climits>
 #include <deque>
@@ -49,7 +48,7 @@ struct StringsProxyVarAttributeId {};
 typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttribute;
 
 class TheoryStrings : public Theory {
-  typedef context::CDChunkList<Node> NodeList;
+  typedef context::CDList<Node> NodeList;
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 60bfd6fab..41987265e 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -23,7 +23,6 @@
 #include "util/hash.h"
 #include "theory/theory.h"
 #include "theory/rewriter.h"
-#include "context/cdchunk_list.h"
 #include "context/cdhashmap.h"
 
 namespace CVC4 {
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index a7239dba5..0166bd947 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -17,7 +17,6 @@
 #ifndef __CVC4__THEORY_UF_STRONG_SOLVER_H
 #define __CVC4__THEORY_UF_STRONG_SOLVER_H
 
-#include "context/cdchunk_list.h"
 #include "context/cdhashmap.h"
 #include "context/context.h"
 #include "context/context_mm.h"
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 9d049e9d2..80ca1a5ef 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -78,7 +78,6 @@ SMT2_TESTS = \
 	sqrt2-sort-inf-unk.smt2 \
 	rec-fun-const-parse-bug.smt2
 
-
 # Regression tests for PL inputs
 CVC_TESTS = \
 	boolean.cvc \
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 55a6c2b09..1be242e3d 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -3,6 +3,7 @@ TEST_EXTENSIONS = .class
 CPLUSPLUS_TESTS = \
 	boilerplate \
 	ouroborous \
+	reset_assertions \
 	two_smt_engines \
 	smt2_compliance \
 	statistics
diff --git a/test/system/reset_assertions.cpp b/test/system/reset_assertions.cpp
new file mode 100644
index 000000000..4fed06698
--- /dev/null
+++ b/test/system/reset_assertions.cpp
@@ -0,0 +1,53 @@
+/*********************                                                        */
+/*! \file reset_assertions.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** 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 A simple test for SmtEngine::resetAssertions()
+ **
+ ** This program indirectly also tests some corner cases w.r.t.
+ ** context-dependent datastructures: resetAssertions() pops the contexts to
+ ** zero but some context-dependent datastructures are created at leevel 1,
+ ** which the datastructure needs to handle properly problematic.
+ **/
+
+#include <iostream>
+#include <sstream>
+
+#include "expr/expr.h"
+#include "smt/smt_engine.h"
+
+using namespace CVC4;
+
+int main()
+{
+  ExprManager em;
+  SmtEngine smt(&em);
+
+  smt.setOption("incremental", SExpr(true));
+
+  Type real = em.realType();
+  Expr x = em.mkVar("x", real);
+  Expr four = em.mkConst(Rational(4));
+  Expr xEqFour = em.mkExpr(Kind::EQUAL, x, four);
+  smt.assertFormula(xEqFour);
+  std::cout << smt.checkSat() << std::endl;
+
+  smt.resetAssertions();
+
+  Type elementType = em.integerType();
+  Type indexType = em.integerType();
+  Type arrayType = em.mkArrayType(indexType, elementType);
+  Expr array = em.mkVar("array", arrayType);
+  Expr arrayAtFour = em.mkExpr(Kind::SELECT, array, four);
+  Expr ten = em.mkConst(Rational(10));
+  Expr arrayAtFour_eq_ten = em.mkExpr(Kind::EQUAL, arrayAtFour, ten);
+  smt.assertFormula(arrayAtFour_eq_ten);
+  std::cout << smt.checkSat() << std::endl;
+}
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 8c45eeb23..9de940a0d 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -34,7 +34,6 @@ UNIT_TESTS += \
 	context/context_mm_black \
 	context/cdo_black \
 	context/cdlist_black \
-	context/cdlist_context_memory_black \
 	context/cdmap_black \
 	context/cdmap_white \
 	context/cdvector_black \
diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h
index 8525ef6f3..5015ae002 100644
--- a/test/unit/context/cdlist_black.h
+++ b/test/unit/context/cdlist_black.h
@@ -150,4 +150,12 @@ class CDListBlack : public CxxTest::TestSuite {
 
 #endif /* CVC4_MEMORY_LIMITING_DISABLED */
   }
+
+  void testPopBelowLevelCreated()
+  {
+    d_context->push();
+    CDList<int> list(d_context);
+    d_context->popto(0);
+    list.push_back(42);
+  }
 };
diff --git a/test/unit/context/cdlist_context_memory_black.h b/test/unit/context/cdlist_context_memory_black.h
deleted file mode 100644
index 654251a0c..000000000
--- a/test/unit/context/cdlist_context_memory_black.h
+++ /dev/null
@@ -1,160 +0,0 @@
-/*********************                                                        */
-/*! \file cdlist_context_memory_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Paul Meng
- ** 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 Black box testing of CVC4::context::CDList<>.
- **
- ** Black box testing of CVC4::context::CDList<>.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <iostream>
-#include <vector>
-
-#include <limits.h>
-
-#include "memory.h"
-
-#include "context/cdchunk_list.h"
-#include "context/context.h"
-
-using namespace std;
-using namespace CVC4::context;
-
-struct DtorSensitiveObject {
-  bool& d_dtorCalled;
-  DtorSensitiveObject(bool& dtorCalled) : d_dtorCalled(dtorCalled) {}
-  ~DtorSensitiveObject() { d_dtorCalled = true; }
-};
-
-class CDListContextMemoryBlack : public CxxTest::TestSuite {
- private:
-  Context* d_context;
-
- public:
-  void setUp() { d_context = new Context(); }
-
-  void tearDown() { delete d_context; }
-
-  // test at different sizes.  this triggers grow() behavior differently.
-  // grow() was completely broken in revision 256
-  void testCDChunkList10() { listTest(10); }
-  void testCDChunkList15() { listTest(15); }
-  void testCDChunkList20() { listTest(20); }
-  void testCDChunkList35() { listTest(35); }
-  void testCDChunkList50() { listTest(50); }
-  void testCDChunkList99() { listTest(99); }
-
-  void listTest(int N) {
-    listTest(N, true);
-    listTest(N, false);
-  }
-
-  void listTest(int N, bool callDestructor) {
-    CDChunkList<int> list(d_context, callDestructor,
-                          ContextMemoryAllocator<int>(d_context->getCMM()));
-
-    TS_ASSERT(list.empty());
-    for (int i = 0; i < N; ++i) {
-      TS_ASSERT_EQUALS(list.size(), unsigned(i));
-      list.push_back(i);
-      TS_ASSERT(!list.empty());
-      TS_ASSERT_EQUALS(list.back(), i);
-      int i2 = 0;
-      for (CDChunkList<int>::const_iterator j = list.begin(); j != list.end();
-           ++j) {
-        TS_ASSERT_EQUALS(*j, i2++);
-      }
-    }
-    TS_ASSERT_EQUALS(list.size(), unsigned(N));
-
-    for (int i = 0; i < N; ++i) {
-      TS_ASSERT_EQUALS(list[i], i);
-    }
-  }
-
-  void testEmptyIterator() {
-    CDChunkList<int>* list = new (d_context->getCMM())
-        CDChunkList<int>(true, d_context, false,
-                         ContextMemoryAllocator<int>(d_context->getCMM()));
-    TS_ASSERT_EQUALS(list->begin(), list->end());
-  }
-
-  void testDtorCalled() {
-    bool shouldRemainFalse = false;
-    bool shouldFlipToTrue = false;
-    bool alsoFlipToTrue = false;
-    bool shouldAlsoRemainFalse = false;
-    bool aThirdFalse = false;
-
-    CDChunkList<DtorSensitiveObject> listT(
-        d_context, true,
-        ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
-    CDChunkList<DtorSensitiveObject> listF(
-        d_context, false,
-        ContextMemoryAllocator<DtorSensitiveObject>(d_context->getCMM()));
-
-    DtorSensitiveObject shouldRemainFalseDSO(shouldRemainFalse);
-    DtorSensitiveObject shouldFlipToTrueDSO(shouldFlipToTrue);
-    DtorSensitiveObject alsoFlipToTrueDSO(alsoFlipToTrue);
-    DtorSensitiveObject shouldAlsoRemainFalseDSO(shouldAlsoRemainFalse);
-    DtorSensitiveObject aThirdFalseDSO(aThirdFalse);
-
-    listT.push_back(shouldAlsoRemainFalseDSO);
-    listF.push_back(shouldAlsoRemainFalseDSO);
-
-    d_context->push();
-
-    listT.push_back(shouldFlipToTrueDSO);
-    listT.push_back(alsoFlipToTrueDSO);
-
-    listF.push_back(shouldRemainFalseDSO);
-    listF.push_back(shouldAlsoRemainFalseDSO);
-    listF.push_back(aThirdFalseDSO);
-
-    TS_ASSERT_EQUALS(shouldRemainFalse, false);
-    TS_ASSERT_EQUALS(shouldFlipToTrue, false);
-    TS_ASSERT_EQUALS(alsoFlipToTrue, false);
-    TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false);
-    TS_ASSERT_EQUALS(aThirdFalse, false);
-
-    d_context->pop();
-
-    TS_ASSERT_EQUALS(shouldRemainFalse, false);
-    TS_ASSERT_EQUALS(shouldFlipToTrue, true);
-    TS_ASSERT_EQUALS(alsoFlipToTrue, true);
-    TS_ASSERT_EQUALS(shouldAlsoRemainFalse, false);
-    TS_ASSERT_EQUALS(aThirdFalse, false);
-  }
-
-  void testOutOfMemory() {
-#ifdef CVC4_MEMORY_LIMITING_DISABLED
-
-    CVC4::test::WarnWithLimitedMemoryDisabledReason();
-
-#else /* CVC4_MEMORY_LIMITING_DISABLED */
-
-    CDChunkList<unsigned> list(d_context);
-    CVC4::test::WithLimitedMemory wlm(1);
-
-    TS_ASSERT_THROWS(
-        {
-          // We cap it at UINT_MAX, preferring to terminate with a
-          // failure than run indefinitely.
-          for (unsigned i = 0; i < UINT_MAX; ++i) {
-            list.push_back(i);
-          }
-        },
-        bad_alloc);
-
-#endif /* CVC4_MEMORY_LIMITING_DISABLED */
-  }
-};