Highlights of this commit are:

* add NodeManagerWhite unit test

* change kind::APPLY to kind::APPLY_UF

* better APPLY handling: operators are no longer considered children

* more efficient pool lookup; the NodeValue doesn't have to be as fully constructed for the lookup to proceed

* extend DSL for kind declarations
  + new "theory" command declares a theory and its header.  theory_def.h no longer required.
  + arity enforced on operators
  + constant mapping, hashing, equality

* CONSTANT metakinds supported (via Node::getConst<T>(), for example, Node::getConst<CVC4::Rational>() gets a Rational out of a Node (assuming it is of CONST_RATIONAL kind)

* added CONST_RATIONAL and CONST_INTEGER kinds

* builtin operators (AND, OR, PLUS, etc..) returned by Node::getOperator() are now CONSTANT metakind and are created by NodeManager

* Pretty-printing of Nodes now has a depth limit settable by a stream manipulator (e.g. "cout << Node::setdepth(5) << m << endl;" prints DAG rooted at m to a depth of 5)

* getters added to Node, TNode, NodeValue, etc., for operators and metakinds

* build-time generators for kind.h, metakind.h, and theoryof_table.h headers now have a simpler design and flag errors better, and the templates (kind_template.h etc.) are easier to understand.

* DISTINCT is now a kind, and the SMT parser now passes through DISTINCT nodes instead of blowing them up into ANDs.  Until theory rewriting is online, though, DISTINCTs are directly blown up into conjunctions in TheoryEngine::rewrite().

* add gmpxx detection and inclusion

* better Asserts throughout, some documentation, cleanup

1 files changed, 33 insertions, 12 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index ee370f682..29749ee5d 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -25,8 +25,31 @@ namespace CVC4 {
 
 __thread NodeManager* NodeManager::s_current = 0;
 
+NodeManager::NodeManager(context::Context* ctxt) :
+  d_attrManager(ctxt),
+  d_nodeUnderDeletion(NULL),
+  d_reclaiming(false) {
+  poolInsert( &expr::NodeValue::s_null );
+
+  for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
+    Kind k = Kind(i);
+
+    if(hasOperator(k)) {
+      d_operators[i] = mkConst(Kind(k));
+    }
+  }
+}
+
 NodeManager::~NodeManager() {
+  // have to ensure "this" is the current NodeManager during
+  // destruction of operators, because they get GCed.
+
   NodeManagerScope nms(this);
+
+  for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
+    d_operators[i] = Node::null();
+  }
+
   while(!d_zombies.empty()) {
     reclaimZombies();
   }
@@ -34,15 +57,6 @@ NodeManager::~NodeManager() {
   poolRemove( &expr::NodeValue::s_null );
 }
 
-NodeValue* NodeManager::poolLookup(NodeValue* nv) const {
-  NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
-  if(find == d_nodeValuePool.end()) {
-    return NULL;
-  } else {
-    return *find;
-  }
-}
-
 /**
  * This class ensure that NodeManager::d_reclaiming gets set to false
  * even on exceptional exit from NodeManager::reclaimZombies().
@@ -81,6 +95,9 @@ void NodeManager::reclaimZombies() {
 
   // during reclamation, reclaimZombies() is never supposed to be called
   Assert(! d_reclaiming, "NodeManager::reclaimZombies() not re-entrant!");
+
+  // whether exit is normal or exceptional, the Reclaim dtor is called
+  // and ensures that d_reclaiming is set back to false.
   Reclaim r(d_reclaiming);
 
   // We copy the set away and clear the NodeManager's set of zombies.
@@ -111,14 +128,18 @@ void NodeManager::reclaimZombies() {
     // collect ONLY IF still zero
     if(nv->d_rc == 0) {
       Debug("gc") << "deleting node value " << nv
-                  << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+                  << " [" << nv->d_id << "]: " << *nv << "\n";
 
       // remove from the pool
       if(nv->getKind() != kind::VARIABLE) {
         poolRemove(nv);
       }
-      NVReclaim rc(d_underTheShotgun);
-      d_underTheShotgun = nv;
+
+      // whether exit is normal or exceptional, the NVReclaim dtor is
+      // called and ensures that d_nodeUnderDeletion is set back to
+      // NULL.
+      NVReclaim rc(d_nodeUnderDeletion);
+      d_nodeUnderDeletion = nv;
 
       // remove attributes
       d_attrManager.deleteAllAttributes(nv);