* public/private code untangled (smt/smt_engine.h no longer #includes

  expr/node.h).  This removes the warnings we had during compilation,
  and heads off a number of potential linking errors due to improper
  inlining of private (library-only) stuff in client (out-of-library)
  code.

* "configure" now takes some options as part of a "bare-option" build
  type (e.g., "./configure debug-coverage" or "./configure production-muzzle").

* split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h

* split cdlist_black unit test from context_black

* implement CDMap<>.

* give ExprManagers ownership of the context (and have SmtEngine share
  that one)

* fix main driver to properly report file-not-found

* fix MemoryMappedInputBuffer class to report reasons for
  "errno"-returned system errors

* src/expr/attribute.h: context-dependent attribute kinds now
  supported

* test/unit/expr/node_white.h: context-dependent attribute tests

* src/prop/cnf_conversion.h and associated parts of src/util/options.h
  and src/main/getopt.cpp: obsolete command-line option, removed.

* src/util/Assert.h: assertions are now somewhat more useful (in debug
  builds, anyway) during stack unwinding.

* test/unit/theory/theory_black.h: test context-dependent behavior of
  registerTerm() attribute for theories

* src/expr/node_builder.h: formatting, fixes for arithmetic
  convenience node builders, check memory allocations

* test/unit/expr/node_builder_black.h: add tessts for addition,
  subtraction, unary minus, and multiplication convenience node
  builders

* src/expr/attribute.h: more comments

* (various) code formatting, comment cleanup, added throws specifier
  to some destructors

* contrib/code-checker: prototype perl script to test (some) code policy

* contrib/indent-settings: command line for GNU indent to indent using
  CVC4 style (sort of; this is a work in progress)

* COPYING: legal stuff

* DESIGN_QUESTIONS: obsolete, removed

1 files changed, 47 insertions, 7 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 62bcc7516..c4f54727a 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -28,6 +28,7 @@
 
 #include "expr/kind.h"
 #include "expr/expr.h"
+#include "context/context.h"
 
 namespace CVC4 {
 
@@ -51,7 +52,8 @@ class NodeManager {
 
   template <unsigned> friend class CVC4::NodeBuilder;
 
-  typedef __gnu_cxx::hash_set<expr::NodeValue*, expr::NodeValueHashFcn,
+  typedef __gnu_cxx::hash_set<expr::NodeValue*,
+                              expr::NodeValueInternalHashFcn,
                               expr::NodeValue::NodeValueEq> NodeValueSet;
   NodeValueSet d_nodeValueSet;
 
@@ -61,10 +63,18 @@ class NodeManager {
   void poolInsert(expr::NodeValue* nv);
 
   friend class NodeManagerScope;
+  friend class expr::NodeValue;
+
+  std::vector<expr::NodeValue*> d_zombieList;
+
+  inline void gc(expr::NodeValue* nv) {
+    Assert(nv->d_rc == 0);
+    d_zombieList.push_back(nv);
+  }
 
 public:
 
-  NodeManager() {
+  NodeManager(context::Context* ctxt) : d_attrManager(ctxt) {
     poolInsert( &expr::NodeValue::s_null );
   }
 
@@ -133,6 +143,26 @@ public:
   inline const Type* getType(TNode n);
 };
 
+/**
+ * Resource-acquisition-is-instantiation C++ idiom: create one of
+ * these "scope" objects to temporarily change the thread-specific
+ * notion of the "current" NodeManager for Node creation/deletion,
+ * etc.  On destruction, the previous NodeManager pointer is restored.
+ * Therefore such objects should only be created and destroyed in a
+ * well-scoped manner (such as on the stack).
+ *
+ * This is especially useful on public-interface calls into the CVC4
+ * library, where CVC4's notion of the "current" NodeManager should be
+ * set to match the calling context.  See, for example, the
+ * implementations of public calls in the ExprManager and SmtEngine
+ * classes.
+ *
+ * You may create a NodeManagerScope with "new" and destroy it with
+ * "delete", or place it as a data member of an object that is, but if
+ * the scope of these new/delete pairs isn't properly maintained, the
+ * incorrect "current" NodeManager pointer may be restored after a
+ * delete.
+ */
 class NodeManagerScope {
   NodeManager *d_oldNodeManager;
 
@@ -143,22 +173,32 @@ public:
     Debug("current") << "node manager scope: " << NodeManager::s_current << "\n";
   }
 
-  ~NodeManagerScope() throw() {
+  ~NodeManagerScope() {
     NodeManager::s_current = d_oldNodeManager;
     Debug("current") << "node manager scope: returning to " << NodeManager::s_current << "\n";
   }
 };
 
 /**
- * A wrapper (essentially) for NodeManagerScope.  Without this, we'd
- * need Expr to be a friend of ExprManager.
+ * A wrapper (essentially) for NodeManagerScope.  The current
+ * "NodeManager" pointer is set to this Expr's underlying
+ * ExpressionManager's NodeManager.  When the ExprManagerScope is
+ * destroyed, the previous NodeManager is restored.
+ *
+ * This is especially useful on public-interface calls into the CVC4
+ * library, where CVC4's notion of the "current" NodeManager should be
+ * set to match the calling context.  See, for example, the
+ * implementations of public calls in the Expr class.
+ *
+ * Without this, we'd need Expr to be a friend of ExprManager.
  */
 class ExprManagerScope {
   NodeManagerScope d_nms;
 public:
   inline ExprManagerScope(const Expr& e) :
-    d_nms(e.getExprManager() == NULL ?
-          NodeManager::currentNM() : e.getExprManager()->getNodeManager()) {
+    d_nms(e.getExprManager() == NULL
+          ? NodeManager::currentNM()
+          : e.getExprManager()->getNodeManager()) {
   }
 };