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.

2 files changed, 15 insertions, 14 deletions

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 097724d48..25c22f196 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -211,8 +211,8 @@ public:
   void testRegisterTerm() {
     TS_ASSERT(d_dummy->doneWrapper());
 
-    Type* typeX = d_nm->booleanType();
-    Type* typeF = d_nm->mkFunctionType(typeX, typeX);
+    Type typeX = d_nm->booleanType();
+    Type typeF = d_nm->mkFunctionType(typeX, typeX);
 
     Node x = d_nm->mkVar("x",typeX);
     Node f = d_nm->mkVar("f",typeF);
diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h
index f5da06a0b..44b13c87c 100644
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -107,10 +107,11 @@ public:
     d_outputChannel.clear();
     d_euf = new TheoryUF(d_ctxt, d_outputChannel);
 
-    d_booleanType = d_nm->booleanType();
+    d_booleanType = new Type(d_nm->booleanType());
   }
 
   void tearDown() {
+    delete d_booleanType;
     delete d_euf;
     d_outputChannel.clear();
     delete d_scope;
@@ -119,8 +120,8 @@ public:
   }
 
   void testPushPopChain() {
-    Node x = d_nm->mkVar(d_booleanType);
-    Node f = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node f = d_nm->mkVar(*d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -174,8 +175,8 @@ public:
 
   /* test that {f(f(x)) == x, f(f(f(x))) != f(x)} is inconsistent */
   void testSimpleChain() {
-    Node x = d_nm->mkVar(d_booleanType);
-    Node f = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node f = d_nm->mkVar(*d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -199,7 +200,7 @@ public:
 
   /* test that !(x == x) is inconsistent */
   void testSelfInconsistent() {
-    Node x = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
     Node x_neq_x = (x.eqNode(x)).notNode();
 
     d_euf->assertFact(x_neq_x);
@@ -212,7 +213,7 @@ public:
 
   /* test that (x == x) is consistent */
   void testSelfConsistent() {
-    Node x = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
     Node x_eq_x = x.eqNode(x);
 
     d_euf->assertFact(x_eq_x);
@@ -228,8 +229,8 @@ public:
       f(x) != x
      } is inconsistent */
   void testChain() {
-    Node x = d_nm->mkVar(d_booleanType);
-    Node f = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node f = d_nm->mkVar(*d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -259,7 +260,7 @@ public:
 
 
   void testPushPopA() {
-    Node x = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
     Node x_eq_x = x.eqNode(x);
 
     d_ctxt->push();
@@ -270,8 +271,8 @@ public:
   }
 
   void testPushPopB() {
-    Node x = d_nm->mkVar(d_booleanType);
-    Node f = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node f = d_nm->mkVar(*d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_x_eq_x = f_x.eqNode(x);