Marging from types 404:415, changes: Massive

* Types are now represented as nodes in the attribute table and are managed, i.e. you can say
    Type booleanType = d_nodeManager->booleanType();
    Type t = d_nodeManager->mkFunctionType(booleanType, booleanType);
    FunctionType ft = (FunctionType)t;
    Assert(ft.getArgTypes()[0], booleanType);
* The attributes now have a table for Nodes and a table for TNodes (both should be used with caution)
* Changes the way nodes are extracted from NodeBuilder, added several methods to
  extract a Node, NodeValue, or Node*, with corresponding methods for extraction
* Used the above in the construction of Expr and Type objects
* The NodeManager now destroys the attributes in the destructor by pausing the
  garbage collection
* To achive destruction a flag d_inDesctruction has been added to loosen the assertion
  in NodeValue::dec() (there might be -refcount TNodes leftover)
* Beginnings of the Bitvector constants using GMP

Not yet in tiptop phase, needs more documentation, and Types should be pulled out to TypeNodes eventually. Also, the types are currently defined in the builting_kinds, and I need to add these to the theory specific definitions with special 'type' constructs.

I hate branching and merging.

1 files changed, 49 insertions, 41 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 708bd16b2..4f0e0ff76 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -27,55 +27,23 @@ 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();
-  }
-
-  poolRemove( &expr::NodeValue::s_null );
-}
-
 /**
  * This class ensures that NodeManager::d_reclaiming gets set to false
  * even on exceptional exit from NodeManager::reclaimZombies().
  */
-struct Reclaim {
-  bool& d_reclaimField;
+struct ScopedBool {
+  bool& d_value;
 
-  Reclaim(bool& reclaim) :
-    d_reclaimField(reclaim) {
+  ScopedBool(bool& reclaim) :
+    d_value(reclaim) {
 
     Debug("gc") << ">> setting RECLAIM field\n";
-    d_reclaimField = true;
+    d_value = true;
   }
 
-  ~Reclaim() {
+  ~ScopedBool() {
     Debug("gc") << "<< clearing RECLAIM field\n";
-    d_reclaimField = false;
+    d_value = false;
   }
 };
 
@@ -98,17 +66,57 @@ struct NVReclaim {
   }
 };
 
+
+NodeManager::NodeManager(context::Context* ctxt) :
+  d_attrManager(ctxt),
+  d_nodeUnderDeletion(NULL),
+  d_dontGC(false),
+  d_inDestruction(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);
+  ScopedBool inDestruction(d_inDestruction);
+
+  {
+    ScopedBool dontGC(d_dontGC);
+    d_attrManager.deleteAllAttributes();
+  }
+
+  for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
+    d_operators[i] = Node::null();
+  }
+
+  while(!d_zombies.empty()) {
+    reclaimZombies();
+  }
+
+  poolRemove( &expr::NodeValue::s_null );
+}
+
 void NodeManager::reclaimZombies() {
   // FIXME multithreading
 
   Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n";
 
   // during reclamation, reclaimZombies() is never supposed to be called
-  Assert(! d_reclaiming, "NodeManager::reclaimZombies() not re-entrant!");
+  Assert(! d_dontGC, "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);
+  ScopedBool r(d_dontGC);
 
   // We copy the set away and clear the NodeManager's set of zombies.
   // This is because reclaimZombie() decrements the RC of the