* 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).

5 files changed, 12 insertions, 21 deletions

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();
     }