From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 6 Apr 2010 06:39:01 +0000 (+0000)
Subject: * Add some protected ContextObj accessors for ContextObj-derived classes:
X-Git-Tag: cvc5-1.0.0~9124
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4143f662e0c5ef311e98dbd554500b98cd02ecdb;p=cvc5.git

* Add some protected ContextObj accessors for ContextObj-derived classes:
  + Context* getContext() -- gets the context
  + ContextMemoryManager* getCMM() -- gets the CMM
  + int getLevel() -- the scope level of the ContextObj's most recent update
  + bool isCurrent() -- true iff the most recent update is the current top level

  In particular, the ContextObj::getCMM() call cleans up by TheoryUF's
  ECData::addPredecessor() function substantially (re: code review bug #64).

* Fix serious bugs in context operations that corrupted the ContextObj
  linked lists.  Closes bug #85.

* Identified a bug in the way objects of the "Link" class are
  allocated; see bug #96.

* Re-enable context white-box tests that ensure proper links in linked
  lists.  Closes bug #86.

* Re-enable CDMap<>::emptyTrash().  Closes bug #87.

* Add a tracing option (-t foo or --trace foo) to the driver to enable
  Trace("foo") output stream.  -d foo implies -t foo.

* Minor clean-up of some TheoryUF code; addition of some documentation
  (re: code review bug #64).

* Address some things that caused Doxygen discomfort.

* Address an issue raised in NodeManager's code review (bug #65).

* Remove an inaccurate comment in Attribute code (re: code review bug #61).
---

diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index d4de88daf..75f6eb2ae 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -71,6 +71,7 @@ class CDOmap : public ContextObj {
       }
       d_next->d_prev = d_prev;
       d_prev->d_next = d_next;
+      Debug("gc") << "CDMap<> trash push_back " << this << std::endl;
       d_map->d_trash.push_back(this);
     } else {
       d_data = p->d_data;
@@ -155,7 +156,7 @@ public:
 
   CDMapData(Context* context) : ContextObj(context) {}
   CDMapData(const ContextObj& co) : ContextObj(co) {}
-  ~CDMapData() { destroy(); }
+  ~CDMapData() throw(AssertionException) { destroy(); }
 };
 
 /**
@@ -192,7 +193,7 @@ class CDMap : public ContextObj {
         i != d_trash.end();
         ++i) {
       Debug("gc") << "emptyTrash(): " << *i << std::endl;
-      //(*i)->deleteSelf();
+      (*i)->deleteSelf();
     }
     d_trash.clear();
   }
@@ -201,21 +202,26 @@ public:
 
   CDMap(Context* context) :
     ContextObj(context),
+    d_map(),
     d_first(NULL),
     d_context(context),
     d_trash() {
   }
 
   ~CDMap() throw(AssertionException) {
+    Debug("gc") << "cdmap " << this
+                << " disappearing, destroying..." << std::endl;
     destroy();
+    Debug("gc") << "cdmap " << this
+                << " disappearing, done destroying" << std::endl;
     for(typename table_type::iterator i = d_map.begin();
         i != d_map.end();
         ++i) {
       (*i).second->deleteSelf();
     }
-    //d_map.clear();
-    Debug("gc") << "cdmap gone, emptying trash" << std::endl;
+    Debug("gc") << "cdmap " << this << " gone, emptying trash" << std::endl;
     emptyTrash();
+    Debug("gc") << "done emptying trash for " << this << std::endl;
   }
 
   // The usual operators of map
diff --git a/src/context/cdo.h b/src/context/cdo.h
index e03156e8a..ead43b2e8 100644
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -66,11 +66,26 @@ class CDO : public ContextObj {
   CDO<T>& operator=(const CDO<T>& cdo);
 
 public:
+
   /**
    * Main constructor - uses default constructor for T to create the initial
    * value of d_data.
    */
-  CDO(Context* context) : ContextObj(context) {}
+  CDO(Context* context) :
+    ContextObj(context) {
+  }
+
+  /**
+   * Main constructor - uses default constructor for T to create the
+   * initial value of d_data.
+   *
+   * This version takes an argument that specifies whether this CDO<>
+   * was itself allocated in context memory.  If it was, it is linked
+   * with the current scope rather than scope 0.
+   */
+  CDO(bool allocatedInCMM, Context* context) :
+    ContextObj(allocatedInCMM, context) {
+  }
 
   /**
    * Constructor from object of type T.  Creates a ContextObj and sets the data
@@ -78,7 +93,24 @@ public:
    * current Scope.  If the Scope is popped, the value will revert to whatever
    * is assigned by the default constructor for T
    */
-  CDO(Context* context, const T& data) : ContextObj(context) {
+  CDO(Context* context, const T& data) :
+    ContextObj(context) {
+    makeCurrent();
+    d_data = data;
+  }
+
+  /**
+   * Constructor from object of type T.  Creates a ContextObj and sets the data
+   * to the given data value.  Note that this value is only valid in the
+   * current Scope.  If the Scope is popped, the value will revert to whatever
+   * is assigned by the default constructor for T.
+   *
+   * This version takes an argument that specifies whether this CDO<>
+   * was itself allocated in context memory.  If it was, it is linked
+   * with the current scope rather than scope 0.
+   */
+  CDO(bool allocatedInCMM, Context* context, const T& data) :
+    ContextObj(allocatedInCMM, context) {
     makeCurrent();
     d_data = data;
   }
@@ -86,7 +118,7 @@ public:
   /**
    * Destructor - call destroy() method
    */
-  ~CDO() throw() { destroy(); }
+  ~CDO() throw(AssertionException) { destroy(); }
 
   /**
    * Set the data in the CDO.  First call makeCurrent.
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 05024430c..d371dc39a 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -10,9 +10,13 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Implementation of base context operations.
  **/
 
 
+#include <iostream>
+#include <vector>
+
 #include "context/context.h"
 #include "util/Assert.h"
 
@@ -54,7 +58,7 @@ Context::~Context() throw(AssertionException) {
 
 
 void Context::push() {
-  // FIXME: TRACE("pushpop", indentStr, "Push", " {");
+  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "Push {" << std::endl;
 
   // Create a new memory region
   d_pCMM->push();
@@ -93,7 +97,7 @@ void Context::pop() {
     pCNO = pCNO->d_pCNOnext;
   }
 
-  //FIXME:  TRACE("pushpop", indentStr, "}", " Pop");
+  Trace("pushpop") << std::string(2 * getLevel(), ' ') << "} Pop" << std::endl;
 }
 
 
@@ -124,16 +128,47 @@ void Context::addNotifyObjPost(ContextNotifyObj* pCNO) {
 }
 
 
-void ContextObj::update() {
+void ContextObj::update() throw(AssertionException) {
+  Debug("context") << "before update(" << this << "):" << std::endl
+                   << *getContext() << std::endl;
+
   // Call save() to save the information in the current object
   ContextObj* pContextObjSaved = save(d_pScope->getCMM());
 
+  Debug("context") << "in update(" << this << ") with restore "
+                   << pContextObjSaved << ": waypoint 1" << std::endl
+                   << *getContext() << std::endl;
+
   // Check that base class data was saved
-  Assert(pContextObjSaved->d_pContextObjNext == d_pContextObjNext &&
-         pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev &&
-         pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore &&
-         pContextObjSaved->d_pScope == d_pScope,
-         "save() did not properly copy information in base class");
+  Assert( ( pContextObjSaved->d_pContextObjNext == d_pContextObjNext &&
+            pContextObjSaved->d_ppContextObjPrev == d_ppContextObjPrev &&
+            pContextObjSaved->d_pContextObjRestore == d_pContextObjRestore &&
+            pContextObjSaved->d_pScope == d_pScope ),
+          "save() did not properly copy information in base class" );
+
+  // Link the "saved" object in place of this ContextObj in the scope
+  // we're moving it FROM.
+  Debug("context") << "in update(" << this
+                   << "): next() == " << next() << std::endl;
+  if(next() != NULL) {
+    Debug("context") << "in update(" << this
+                     << "): next()->prev() == " << next()->prev() << std::endl;
+    next()->prev() = &pContextObjSaved->next();
+    Debug("context") << "in update(" << this
+                     << "): next()->prev() is now "
+                     << next()->prev() << std::endl;
+  }
+  Debug("context") << "in update(" << this
+                   << "): prev() == " << prev() << std::endl;
+  Debug("context") << "in update(" << this
+                   << "): *prev() == " << *prev() << std::endl;
+  *prev() = pContextObjSaved;
+  Debug("context") << "in update(" << this
+                   << "): *prev() is now " << *prev() << std::endl;
+
+  Debug("context") << "in update(" << this << ") with restore "
+                   << pContextObjSaved << ": waypoint 3" << std::endl
+                   << *getContext() << std::endl;
 
   // Update Scope pointer to current top Scope
   d_pScope = d_pScope->getContext()->getTopScope();
@@ -144,18 +179,27 @@ void ContextObj::update() {
   // Insert object into the list of objects that need to be restored when this
   // Scope is popped.
   d_pScope->addToChain(this);
+
+  Debug("context") << "after update(" << this << ") with restore "
+                   << pContextObjSaved << ":" << std::endl
+                   << *getContext() << std::endl;
 }
 
 
-ContextObj* ContextObj::restoreAndContinue() {
+ContextObj* ContextObj::restoreAndContinue() throw(AssertionException) {
   // Variable to hold next object in list
   ContextObj* pContextObjNext;
 
   // Check the restore pointer.  If NULL, this must be the bottom Scope
   if(d_pContextObjRestore == NULL) {
-    Assert(d_pScope == d_pScope->getContext()->getBottomScope(),
-           "Expected bottom scope");
+    // might not be bottom scope, since objects allocated in context
+    // memory don't get linked to scope 0
+    //
+    // Assert(d_pScope == d_pScope->getContext()->getBottomScope(),
+    //        "Expected bottom scope");
+
     pContextObjNext = d_pContextObjNext;
+
     // Nothing else to do
   } else {
     // Call restore to update the subclass data
@@ -169,13 +213,23 @@ ContextObj* ContextObj::restoreAndContinue() {
     next() = d_pContextObjRestore->d_pContextObjNext;
     prev() = d_pContextObjRestore->d_ppContextObjPrev;
     d_pContextObjRestore = d_pContextObjRestore->d_pContextObjRestore;
+
+    // Re-link this ContextObj to the list in this scope
+    if(next() != NULL) {
+      next()->prev() = &next();
+    }
+    *prev() = this;
   }
+
   // Return the next object in the list
   return pContextObjNext;
 }
 
 
 void ContextObj::destroy() throw(AssertionException) {
+  Debug("context") << "before destroy " << this
+                   << " (level " << getLevel() << "):" << std::endl
+                   << *getContext() << std::endl;
   for(;;) {
     // If valgrind reports invalid writes on the next few lines,
     // here's a hint: make sure all classes derived from ContextObj in
@@ -184,12 +238,18 @@ void ContextObj::destroy() throw(AssertionException) {
     if(next() != NULL) {
       next()->prev() = prev();
     }
-    *(prev()) = next();
+    *prev() = next();
     if(d_pContextObjRestore == NULL) {
       break;
     }
+    Debug("context") << "in destroy " << this << ", restore object is "
+                     << d_pContextObjRestore << " at level "
+                     << d_pContextObjRestore->getLevel() << ":" << std::endl
+                     << *getContext() << std::endl;
     restoreAndContinue();
   }
+  Debug("context") << "after destroy " << this << ":" << std::endl
+                   << *getContext() << std::endl;
 }
 
 
@@ -198,11 +258,27 @@ ContextObj::ContextObj(Context* pContext) :
 
   Assert(pContext != NULL, "NULL context pointer");
 
+  Debug("context") << "create new ContextObj(" << this << ")" << std::endl;
   d_pScope = pContext->getBottomScope();
   d_pScope->addToChain(this);
 }
 
 
+ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) :
+  d_pContextObjRestore(NULL) {
+
+  Assert(pContext != NULL, "NULL context pointer");
+
+  Debug("context") << "create new ContextObj(" << this << ")" << std::endl;
+  if(allocatedInCMM) {
+    d_pScope = pContext->getTopScope();
+  } else {
+    d_pScope = pContext->getBottomScope();
+  }
+  d_pScope->addToChain(this);
+}
+
+
 ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
   if(preNotify) {
     pContext->addNotifyObjPre(this);
@@ -217,8 +293,44 @@ ContextNotifyObj::~ContextNotifyObj() throw(AssertionException) {
     d_pCNOnext->d_ppCNOprev = d_ppCNOprev;
   }
   if(d_ppCNOprev != NULL) {
-    *(d_ppCNOprev) = d_pCNOnext;
+    *d_ppCNOprev = d_pCNOnext;
+  }
+}
+
+
+std::ostream& operator<<(std::ostream& out,
+                         const Context& context) throw(AssertionException) {
+  const std::string separator(79, '-');
+
+  int level = context.d_scopeList.size() - 1;
+  typedef std::vector<Scope*>::const_reverse_iterator const_reverse_iterator;
+  for(const_reverse_iterator i = context.d_scopeList.rbegin();
+      i != context.d_scopeList.rend();
+      ++i, --level) {
+    Scope* pScope = *i;
+    Assert(pScope->getLevel() == level);
+    Assert(pScope->getContext() == &context);
+    out << separator << std::endl
+        << *pScope << std::endl;
+  }
+  return out << separator << std::endl;
+}
+
+
+std::ostream& operator<<(std::ostream& out,
+                         const Scope& scope) throw(AssertionException) {
+  out << "Scope " << scope.d_level << ":";
+  ContextObj* pContextObj = scope.d_pContextObjList;
+  Assert(pContextObj == NULL ||
+         pContextObj->prev() == &scope.d_pContextObjList);
+  while(pContextObj != NULL) {
+    out << " <--> " << pContextObj;
+    Assert(pContextObj->d_pScope == &scope);
+    Assert(pContextObj->next() == NULL ||
+           pContextObj->next()->prev() == &pContextObj->next());
+    pContextObj = pContextObj->next();
   }
+  return out << " --> NULL";
 }
 
 
diff --git a/src/context/context.h b/src/context/context.h
index 0e2a9107f..ff650ce5d 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -18,13 +18,15 @@
 #ifndef __CVC4__CONTEXT__CONTEXT_H
 #define __CVC4__CONTEXT__CONTEXT_H
 
-#include "context/context_mm.h"
-#include "util/Assert.h"
-
+#include <iostream>
 #include <cstdlib>
 #include <cstring>
+#include <vector>
 #include <new>
 
+#include "context/context_mm.h"
+#include "util/Assert.h"
+
 namespace CVC4 {
 namespace context {
 
@@ -33,6 +35,14 @@ class Scope;
 class ContextObj;
 class ContextNotifyObj;
 
+/** Pretty-printing of Contexts (for debugging) */
+std::ostream&
+operator<<(std::ostream&, const Context&) throw(AssertionException);
+
+/** Pretty-printing of Scopes (for debugging) */
+std::ostream&
+operator<<(std::ostream&, const Scope&) throw(AssertionException);
+
 /**
  * A Context encapsulates all of the dynamic state of the system.  Its main
  * methods are push() and pop().  A call to push() saves the current state,
@@ -78,6 +88,9 @@ class Context {
    */
   ContextNotifyObj* d_pCNOpost;
 
+  friend std::ostream&
+  operator<<(std::ostream&, const Context&) throw(AssertionException);
+
 public:
   /**
    * Constructor: create ContextMemoryManager and initial Scope
@@ -102,7 +115,7 @@ public:
   /**
    * Return the current Scope level.
    */
-  int getLevel() const { return ((int)d_scopeList.size()) - 1; }
+  int getLevel() const { return d_scopeList.size() - 1; }
 
   /**
    * Return the ContextMemoryManager associated with the context.
@@ -176,13 +189,16 @@ class Scope {
    */
   ContextObj* d_pContextObjList;
 
+  friend std::ostream&
+  operator<<(std::ostream&, const Scope&) throw(AssertionException);
+
 public:
 
   /**
    * Constructor: Create a new Scope; set the level and the previous Scope
    * if any.
    */
-  Scope(Context* pContext, ContextMemoryManager* pCMM, int level) :
+  Scope(Context* pContext, ContextMemoryManager* pCMM, int level) throw() :
     d_pContext(pContext),
     d_pCMM(pCMM),
     d_level(level),
@@ -193,38 +209,38 @@ public:
    * Destructor: Restore all of the objects in ContextObjList.  Defined inline
    * below.
    */
-  ~Scope() throw();
+  ~Scope() throw(AssertionException);
 
   /**
    * Get the Context for this Scope
    */
-  Context* getContext() const { return d_pContext; }
+  Context* getContext() const throw() { return d_pContext; }
 
   /**
    * Get the ContextMemoryManager for this Scope
    */
-  ContextMemoryManager* getCMM() const { return d_pCMM; }
+  ContextMemoryManager* getCMM() const throw() { return d_pCMM; }
 
   /**
    * Get the level of the current Scope
    */
-  int getLevel() const { return d_level; }
+  int getLevel() const throw() { return d_level; }
 
   /**
    * Return true iff this Scope is the current top Scope
    */
-  bool isCurrent() const { return this == d_pContext->getTopScope(); }
+  bool isCurrent() const throw() { return this == d_pContext->getTopScope(); }
 
   /**
-   * When a ContextObj object is modified for the first time in this Scope, it
-   * should call this method to add itself to the list of objects that will
-   * need to be restored.  Defined inline below.
+   * When a ContextObj object is modified for the first time in this
+   * Scope, it should call this method to add itself to the list of
+   * objects that will need to be restored.  Defined inline below.
    */
-  void addToChain(ContextObj* pContextObj);
+  void addToChain(ContextObj* pContextObj) throw(AssertionException);
 
   /**
-   * Overload operator new for use with ContextMemoryManager to allow creation
-   * of new Scope objects in the current memory region.
+   * Overload operator new for use with ContextMemoryManager to allow
+   * creation of new Scope objects in the current memory region.
    */
   static void* operator new(size_t size, ContextMemoryManager* pCMM) {
     return pCMM->newData(size);
@@ -232,9 +248,10 @@ public:
 
   /**
    * Overload operator delete for Scope objects allocated using
-   * ContextMemoryManager.  No need to do anything because memory is freed
-   * automatically when the ContextMemoryManager pop() method is called.
-   * Include both placement and standard delete for completeness.
+   * ContextMemoryManager.  No need to do anything because memory is
+   * freed automatically when the ContextMemoryManager pop() method is
+   * called.  Include both placement and standard delete for
+   * completeness.
    */
   static void operator delete(void* pMem, ContextMemoryManager* pCMM) {}
   static void operator delete(void* pMem) {}
@@ -245,9 +262,9 @@ public:
 };/* class Scope */
 
 /**
- * This is an abstract base class from which all objects that are context-dependent
- * should inherit.  For any data structure that you want to have be
- * automatically backtracked, do the following:
+ * This is an abstract base class from which all objects that are
+ * context-dependent should inherit.  For any data structure that you
+ * want to have be automatically backtracked, do the following:
  * 1. Create a class for the data structure that inherits from ContextObj
  * 2. Implement save()
  *    The role of save() is to create a new ContexObj object that contains
@@ -310,31 +327,34 @@ class ContextObj {
    * does the necessary bookkeeping to ensure that object can be restored to
    * its current state when restore is called.
    */
-  void update();
+  void update() throw(AssertionException);
 
   // The rest of the private methods are for the benefit of the Scope.  We make
   // Scope our friend so it is the only one that can use them.
 
   friend class Scope;
 
+  friend std::ostream&
+  operator<<(std::ostream&, const Scope&) throw(AssertionException);
+
   /**
    * Return reference to next link in ContextObjList.  Used by
    * Scope::addToChain method.
    */
-  ContextObj*& next() { return d_pContextObjNext; }
+  ContextObj*& next() throw() { return d_pContextObjNext; }
 
   /**
    * Return reference to prev link in ContextObjList.  Used by
    * Scope::addToChain method.
    */
-  ContextObj**& prev() { return d_ppContextObjPrev; }
+  ContextObj**& prev() throw() { return d_ppContextObjPrev; }
 
   /**
    * This method is called by Scope during a pop: it does the necessary work to
    * restore the object from its saved copy and then returns the next object in
    * the list that needs to be restored.
    */
-  ContextObj* restoreAndContinue();
+  ContextObj* restoreAndContinue() throw(AssertionException);
 
 protected:
 
@@ -351,14 +371,10 @@ protected:
   virtual void restore(ContextObj* pContextObjRestore) = 0;
 
   /**
-   * This method checks if the object has been modified in this Scope yet.  If
-   * not, it calls update().
+   * This method checks if the object has been modified in this Scope
+   * yet.  If not, it calls update().
    */
-  void makeCurrent() {
-    if(!(d_pScope->isCurrent())) {
-      update();
-    }
-  }
+  inline void makeCurrent() throw(AssertionException);
 
   /**
    * Should be called from sub-class destructor: calls restore until restored
@@ -369,9 +385,59 @@ protected:
    */
   void destroy() throw(AssertionException);
 
+  /////
+  //
+  //  These next four accessors return properties of the Scope to
+  //  derived classes without giving them the Scope object directly.
+  //
+  /////
+
+  /**
+   * Get the Context with which this ContextObj was created.  This is
+   * part of the protected interface, intended for derived classes to
+   * use if necessary.
+   */
+  Context* getContext() const throw() {
+    return d_pScope->getContext();
+  }
+
+  /**
+   * Get the ContextMemoryManager with which this ContextObj was
+   * created.  This is part of the protected interface, intended for
+   * derived classes to use if necessary.  If a ContextObj-derived
+   * class needs to allocate memory somewhere other than the save()
+   * member function (where it is explicitly given a
+   * ContextMemoryManager), it can use this accessor to get the memory
+   * manager.
+   */
+  ContextMemoryManager* getCMM() const throw() {
+    return d_pScope->getCMM();
+  }
+
+  /**
+   * Get the level associated to this ContextObj.  Useful if a
+   * ContextObj-derived class needs to compare the level of its last
+   * update with another ContextObj.
+   */
+  int getLevel() const throw() {
+    return d_pScope->getLevel();
+  }
+
+  /**
+   * Returns true if the object is "current"-- that is, updated in the
+   * topmost contextual scope.  Useful if a ContextObj-derived class
+   * needs to determine if it has been modified in the current scope.
+   * Note that it is always safe to call makeCurrent() without first
+   * checking if the object is current, so this function need not be
+   * used under normal circumstances.
+   */
+  bool isCurrent() const throw() {
+    return d_pScope->isCurrent();
+  }
+
   /**
    * operator new using ContextMemoryManager (common case used by
-   * subclasses during save() ).  No delete is required for memory
+   * subclasses during save()).  No delete is required for memory
    * allocated this way, since it is automatically released when the
    * context is popped.  Also note that allocations using this
    * operator never have their destructor called, so any clean-up has
@@ -401,10 +467,18 @@ public:
    */
   ContextObj(Context* context);
 
+  /**
+   * Create a new ContextObj.  This constructor takes an argument that
+   * specifies whether this ContextObj is itself allocated in context
+   * memory.  If it is, it's invalid below the current scope level, so
+   * we don't put it in scope 0.
+   */
+  ContextObj(bool allocatedInCMM, Context* context);
+
   /**
    * Destructor does nothing: subclass must explicitly call destroy() instead.
    */
-  virtual ~ContextObj() { Debug("contextgc") << "context obj dest" << std::endl; }
+  virtual ~ContextObj() {}
 
   /**
    * If you want to allocate a ContextObj object on the heap, use this
@@ -431,6 +505,7 @@ public:
    * ContextMemoryManager as an argument.
    */
   void deleteSelf() {
+    Debug("context") << "deleteSelf(" << this << ")" << std::endl;
     this->~ContextObj();
     ::operator delete(this);
   }
@@ -475,15 +550,16 @@ class ContextNotifyObj {
    * Return reference to next link in ContextNotifyObj list.  Used by
    * Context::addNotifyObj methods.
    */
-  ContextNotifyObj*& next() { return d_pCNOnext; }
+  ContextNotifyObj*& next() throw() { return d_pCNOnext; }
 
   /**
    * Return reference to prev link in ContextNotifyObj list.  Used by
    * Context::addNotifyObj methods.
    */
-  ContextNotifyObj**& prev() { return d_ppCNOprev; }
+  ContextNotifyObj**& prev() throw() { return d_ppCNOprev; }
 
 public:
+
   /**
    * Constructor for ContextNotifyObj.  Parameters are the context to
    * which this notify object will be added, and a flag which, if
@@ -504,11 +580,16 @@ public:
    * implemented by the subclass.
    */
   virtual void notify() = 0;
+
 };/* class ContextNotifyObj */
 
-// Inline functions whose definitions had to be delayed:
+inline void ContextObj::makeCurrent() throw(AssertionException) {
+  if(!(d_pScope->isCurrent())) {
+    update();
+  }
+}
 
-inline Scope::~Scope() throw() {
+inline Scope::~Scope() throw(AssertionException) {
   // Call restore() method on each ContextObj object in the list.
   // Note that it is the responsibility of restore() to return the
   // next item in the list.
@@ -517,9 +598,12 @@ inline Scope::~Scope() throw() {
   }
 }
 
-inline void Scope::addToChain(ContextObj* pContextObj) {
-  if(d_pContextObjList != NULL)
-    d_pContextObjList->prev() = &(pContextObj->next());
+inline void
+Scope::addToChain(ContextObj* pContextObj) throw(AssertionException) {
+  if(d_pContextObjList != NULL) {
+    d_pContextObjList->prev() = &pContextObj->next();
+  }
+
   pContextObj->next() = d_pContextObjList;
   pContextObj->prev() = &d_pContextObjList;
   d_pContextObjList = pContextObj;
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index ab81c7486..b0b015681 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -85,6 +85,9 @@ void* ContextMemoryManager::newData(size_t size) {
     AlwaysAssert(d_nextFree <= d_endChunk,
                  "Request is bigger than memory chunk size");
   }
+  Debug("context") << "ContextMemoryManager::newData(" << size
+                   << ") returning " << res << " at level "
+                   << d_chunkList.size() << std::endl;
   return res;
 }
 
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 5e8918133..1eeec68af 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -34,7 +34,6 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) {
 
   // FIXME CD-bools in optimized table
   for(unsigned id = 0; id < attr::LastAttributeId<bool, true>::s_id; ++id) {
-    Debug("gc") << "looking for " << id << " x " << nv << ":" << *nv << std::endl;
     d_cdbools.obliterate(std::make_pair(id, nv));
   }
   for(unsigned id = 0; id < attr::LastAttributeId<uint64_t, true>::s_id; ++id) {
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index c79f4da80..27cddf299 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -112,11 +112,6 @@ public:
   typename AttrKind::value_type getAttribute(NodeValue* nv,
                                              const AttrKind&) const;
 
-  // Note that there are two, distinct hasAttribute() declarations for
-  // a reason (rather than using a default argument): they permit more
-  // optimized code.  The first (without parameter "ret") need never
-  // check whether its parameter is NULL.
-
   /**
    * Determine if a particular attribute exists for a particular node.
    *
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 934c405ad..5fc9dee20 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -42,7 +42,7 @@ void CommandSequence::invoke(SmtEngine* smtEngine) {
   }
 }
 
-void CheckSatCommand::toStream(ostream& out) const {
+void CheckSatCommand::toStream(std::ostream& out) const {
   if(d_expr.isNull()) {
     out << "CheckSat()";
   } else {
@@ -50,7 +50,7 @@ void CheckSatCommand::toStream(ostream& out) const {
   }
 }
 
-void CommandSequence::toStream(ostream& out) const {
+void CommandSequence::toStream(std::ostream& out) const {
   out << "CommandSequence[" << endl;
   for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
     out << *d_commandSequence[i] << endl;
@@ -75,7 +75,7 @@ void PushCommand::invoke(SmtEngine* smtEngine) {
   smtEngine->push();
 }
 
-void PushCommand::toStream(ostream& out) const {
+void PushCommand::toStream(std::ostream& out) const {
   out << "Push()";
 }
 
@@ -83,7 +83,7 @@ void PopCommand::invoke(SmtEngine* smtEngine) {
   smtEngine->pop();
 }
 
-void PopCommand::toStream(ostream& out) const {
+void PopCommand::toStream(std::ostream& out) const {
   out << "Pop()";
 }
 
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index bb665ef81..a8d957c91 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -132,7 +132,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                                           child5.getNode())));
 }
 
-Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
+Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
   const unsigned n = children.size();
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 3f7196178..0f8938397 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -159,19 +159,16 @@ class NodeManager {
    */
   inline void markForDeletion(expr::NodeValue* nv) {
     Assert(nv->d_rc == 0);
+
     // if d_reclaiming is set, make sure we don't call
     // reclaimZombies(), because it's already running.
-    if(d_reclaiming) {// FIXME multithreading
-      // currently reclaiming zombies; just push onto the list
-      Debug("gc") << "zombifying node value " << nv
-                  << " [" << nv->d_id << "]: " << *nv
-                  << " [CURRENTLY-RECLAIMING]\n";
-      d_zombies.insert(nv);// FIXME multithreading
-    } else {
-      Debug("gc") << "zombifying node value " << nv
-                  << " [" << nv->d_id << "]: " << *nv << "\n";
-      d_zombies.insert(nv);// FIXME multithreading
+    Debug("gc") << "zombifying node value " << nv
+                << " [" << nv->d_id << "]: " << *nv
+                << (d_reclaiming ? " [CURRENTLY-RECLAIMING]" : "")
+                << std::endl;
+    d_zombies.insert(nv);// FIXME multithreading
 
+    if(!d_reclaiming) {// FIXME multithreading
       // for now, collect eagerly.  can add heuristic here later..
       reclaimZombies();
     }
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index cd952eef9..a272aaafd 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -81,6 +81,12 @@ enum OptionValue {
  *    getopt_long() returns the 4th entry
  * 4. the return value for getopt_long() when this long option (or the
  *    value to set the 3rd entry to; see #3)
+ *
+ * If you add something here, you should add it in src/main/usage.h
+ * also, to document it.
+ *
+ * If you add something that has a short option equivalent, you should
+ * add it to the getopt_long() call in parseOptions().
  */
 static struct option cmdlineOptions[] = {
   // name, has_arg, *flag, val
@@ -91,6 +97,7 @@ static struct option cmdlineOptions[] = {
   { "quiet"      , no_argument      , NULL, 'q'         },
   { "lang"       , required_argument, NULL, 'L'         },
   { "debug"      , required_argument, NULL, 'd'         },
+  { "trace"      , required_argument, NULL, 't'         },
   { "smtcomp"    , no_argument      , NULL, SMTCOMP     },
   { "stats"      , no_argument      , NULL, STATS       },
   { "segv-nospin", no_argument      , NULL, SEGV_NOSPIN },
@@ -131,7 +138,7 @@ throw(OptionException) {
   // cmdlineOptions specifies all the long-options and the return
   // value for getopt_long() should they be encountered.
   while((c = getopt_long(argc, argv,
-                         "+:hVvqL:d:",
+                         "+:hVvqL:d:t:",
                          cmdlineOptions, NULL)) != -1) {
     switch(c) {
 
@@ -171,8 +178,13 @@ throw(OptionException) {
       fputs(lang_help, stdout);
       exit(1);
 
+    case 't':
+      Trace.on(optarg);
+      break;
+
     case 'd':
       Debug.on(optarg);
+      Trace.on(optarg);
       /* fall-through */
 
     case STATS:
diff --git a/src/main/usage.h b/src/main/usage.h
index 3a609d2ec..c8ca6a179 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -32,7 +32,8 @@ CVC4 options:\n\
    --help | -h     this command line reference\n\
    --verbose | -v  increase verbosity (repeatable)\n\
    --quiet | -q    decrease verbosity (repeatable)\n\
-   --debug | -d    debugging for something (e.g. --debug arith)\n\
+   --trace | -t    tracing for something (e.g. --trace pushpop)\n\
+   --debug | -d    debugging for something (e.g. --debug arith), implies -t\n\
    --smtcomp       competition mode (very quiet)\n\
    --stats         give statistics on exit\n\
    --segv-nospin   (debug builds only) don't spin on segfault waiting for gdb\n\
diff --git a/src/theory/uf/ecdata.cpp b/src/theory/uf/ecdata.cpp
index a60aaf1cd..244605476 100644
--- a/src/theory/uf/ecdata.cpp
+++ b/src/theory/uf/ecdata.cpp
@@ -10,7 +10,8 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- **
+ ** Implementation of equivalence class data for UF theory.  This is a
+ ** context-dependent object.
  **/
 
 #include "theory/uf/ecdata.h"
@@ -20,29 +21,27 @@ using namespace context;
 using namespace theory;
 using namespace uf;
 
-
 ECData::ECData(Context * context, TNode n) :
   ContextObj(context),
   d_find(this),
   d_rep(n),
   d_watchListSize(0),
   d_first(NULL),
-  d_last(NULL)
-{}
-
+  d_last(NULL) {
+}
 
-bool ECData::isClassRep(){
+bool ECData::isClassRep() {
   return this == this->d_find;
 }
 
-void ECData::addPredecessor(TNode n, Context* context){
+void ECData::addPredecessor(TNode n) {
   Assert(isClassRep());
 
   makeCurrent();
 
-  Link * newPred = new (context->getCMM())  Link(context, n, d_first);
+  Link * newPred = new(getCMM()) Link(getContext(), n, d_first);
   d_first = newPred;
-  if(d_last == NULL){
+  if(d_last == NULL) {
     d_last = newPred;
   }
 
@@ -62,43 +61,40 @@ void ECData::restore(ContextObj* pContextObj) {
   d_watchListSize = data->d_watchListSize;
 }
 
-Node ECData::getRep(){
+Node ECData::getRep() {
   return d_rep;
 }
 
-unsigned ECData::getWatchListSize(){
+unsigned ECData::getWatchListSize() {
   return d_watchListSize;
 }
 
-
-void ECData::setFind(ECData * ec){
+void ECData::setFind(ECData * ec) {
   makeCurrent();
   d_find = ec;
 }
 
-ECData * ECData::getFind(){
+ECData* ECData::getFind() {
   return d_find;
 }
 
-
-Link* ECData::getFirst(){
+Link* ECData::getFirst() {
   return d_first;
 }
 
-
-void ECData::takeOverDescendantWatchList(ECData * nslave, ECData * nmaster){
+void ECData::takeOverDescendantWatchList(ECData* nslave, ECData* nmaster) {
   Assert(nslave != nmaster);
-  Assert(nslave->getFind() == nmaster );
+  Assert(nslave->getFind() == nmaster);
 
   nmaster->makeCurrent();
 
-  nmaster->d_watchListSize +=  nslave->d_watchListSize;
+  nmaster->d_watchListSize += nslave->d_watchListSize;
 
-  if(nmaster->d_first == NULL){
+  if(nmaster->d_first == NULL) {
     nmaster->d_first = nslave->d_first;
     nmaster->d_last = nslave->d_last;
-  }else if(nslave->d_first != NULL){
-    Link * currLast = nmaster->d_last;
+  } else if(nslave->d_first != NULL) {
+    Link* currLast = nmaster->d_last;
     currLast->d_next = nslave->d_first;
     nmaster->d_last = nslave->d_last;
   }
diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h
index 462e713de..bfc7eab8e 100644
--- a/src/theory/uf/ecdata.h
+++ b/src/theory/uf/ecdata.h
@@ -42,12 +42,14 @@ struct Link {
    * Pointer to the next element in linked list.
    * This is context dependent. 
    */
-  context::CDO< Link* > d_next;
+  context::CDO<Link*> d_next;
 
-  /* Link is supposed to be allocated in a region of a ContextMemoryManager.
-   * In order to avoid having to decrement the ref count at deletion time,
-   * it is preferrable for the user of Link to maintain the invariant that
-   * data will survival for the entire scope of the TNode.
+  /**
+   * Link is supposed to be allocated in a region of a
+   * ContextMemoryManager.  In order to avoid having to decrement the
+   * ref count at deletion time, it is preferrable for the user of
+   * Link to maintain the invariant that data will survival for the
+   * entire scope of the TNode.
    */
   TNode d_data;
 
@@ -55,9 +57,12 @@ struct Link {
    * Creates a new Link w.r.t. a context for the node n.
    * An optional parameter is to specify the next element in the link.
    */
-  Link(context::Context* context, TNode n, Link * l = NULL):
-    d_next(context, l), d_data(n)
-  {}
+  Link(context::Context* context, TNode n, Link* l = NULL) :
+    d_next(true, context, l),
+    d_data(n) {
+    Debug("context") << "Link: " << this
+                     << " so cdo is " << &d_next << std::endl;
+  }
 
   /**
    * Allocates a new Link in the region for the provided ContextMemoryManager.
@@ -67,7 +72,25 @@ struct Link {
     return pCMM->newData(size);
   }
 
-};
+private:
+
+  /**
+   * The destructor isn't actually defined.  This declaration keeps
+   * the compiler from creating (wastefully) a default definition, and
+   * ensures that we get a link error if someone uses Link in a way
+   * that requires destruction.  Objects of class Link should always
+   * be allocated in a ContextMemoryManager, which doesn't call
+   * destructors.
+   */
+  ~Link() throw();
+
+  /**
+   * Just like the destructor, this is not defined.  This ensures no
+   * one tries to create a Link on the heap.
+   */
+  static void* operator new(size_t size);
+
+};/* struct Link */
 
 
 /**
@@ -124,13 +147,16 @@ private:
    */
   TNode d_rep;
 
-  /* Watch list datastructures. */
-  /** Maintains watch list size for more efficient merging */
+  // Watch list data structures follow
+
+  /**
+   * Maintains watch list size for more efficient merging.
+   */
   unsigned d_watchListSize;
 
   /**
-   *Pointer to the beginning of the watchlist.
-   *This value is NULL iff the watch list is empty.
+   * Pointer to the beginning of the watchlist.
+   * This value is NULL iff the watch list is empty.
    */
   Link* d_first;
 
@@ -143,11 +169,11 @@ private:
    */
   Link* d_last;
 
-
-  /** Context dependent operations */
+  /** Context-dependent operation: save this ECData */
   context::ContextObj* save(context::ContextMemoryManager* pCMM);
-  void restore(context::ContextObj* pContextObj);
 
+  /** Context-dependent operation: restore this ECData */
+  void restore(context::ContextObj* pContextObj);
 
 public:
   /**
@@ -157,15 +183,14 @@ public:
   bool isClassRep();
 
   /**
-   * Adds a node to the watch list of the equivalence class.
-   * Requires a Context in-order to do context dependent memory allocation.
+   * Adds a node to the watch list of the equivalence class.  Does
+   * context-dependent memory allocation in the Context with which
+   * this ECData was created.
    *
    * @param n the node to be added.
    * @pre isClassRep() == true
    */
-  void addPredecessor(TNode n, context::Context* context);
-
-
+  void addPredecessor(TNode n);
 
   /**
    * Creates a EQ with the representative n
@@ -175,6 +200,7 @@ public:
    */
   ECData(context::Context* context, TNode n);
 
+  /** Destructor for ECDatas */
   ~ECData() {
     Debug("ufgc") << "Calling ECData destructor" << std::endl;
     destroy();
@@ -189,7 +215,6 @@ public:
    */
   static void takeOverDescendantWatchList(ECData * nslave, ECData * nmaster);
 
-
   /**
    * Returns the representative of this ECData.
    */
@@ -212,7 +237,6 @@ public:
    */
   ECData* getFind();
 
-
   /**
    * Sets the find pointer of the equivalence class to be another ECData object.
    *
@@ -223,13 +247,10 @@ public:
    */
   void setFind(ECData * ec);
 
-
-}; /* class ECData */
-
+};/* class ECData */
 
 }/* CVC4::theory::uf namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-
 #endif /* __CVC4__THEORY__UF__ECDATA_H */
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index f0d8b47e0..2d7d4e91f 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -125,7 +125,7 @@ void TheoryUF::registerTerm(TNode n) {
         }
       }
 
-      ecChild->addPredecessor(n, getContext());
+      ecChild->addPredecessor(n);
     }
   }
   Debug("uf") << "uf: end registerTerm(" << n << ")" << std::endl;
diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h
index 3e0928baf..0963e4100 100644
--- a/test/unit/context/context_white.h
+++ b/test/unit/context/context_white.h
@@ -164,14 +164,14 @@ public:
     TS_ASSERT(b.d_pScope == t);
     TS_ASSERT(b.d_pContextObjRestore != NULL);
     TS_ASSERT(b.d_pContextObjNext == &a);
-    //TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList);// THIS ONE FAILS
+    TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList);
 
     d_context->pop();
 
     TS_ASSERT(s->d_pContext == d_context);
     TS_ASSERT(s->d_pCMM == d_context->d_pCMM);
     TS_ASSERT(s->d_level == 0);
-    //TS_ASSERT(s->d_pContextObjList == &b);// THIS ONE FAILS
+    TS_ASSERT(s->d_pContextObjList == &c);
 
     TS_ASSERT(a.d_pScope == s);
     TS_ASSERT(a.d_pContextObjRestore == NULL);
@@ -181,6 +181,11 @@ public:
     TS_ASSERT(b.d_pScope == s);
     TS_ASSERT(b.d_pContextObjRestore == NULL);
     TS_ASSERT(b.d_pContextObjNext == &a);
-    TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList);
+    TS_ASSERT(b.d_ppContextObjPrev == &c.d_pContextObjNext);
+
+    TS_ASSERT(c.d_pScope == s);
+    TS_ASSERT(c.d_pContextObjRestore == NULL);
+    TS_ASSERT(c.d_pContextObjNext == &b);
+    TS_ASSERT(c.d_ppContextObjPrev == &s->d_pContextObjList);
   }
 };