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.

7 files changed, 154 insertions, 19 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 6597c8b48..7820acb0a 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -25,4 +25,7 @@ libutil_la_SOURCES = \
 	rational.h \
 	rational.cpp \
 	integer.h \
-	integer.cpp
+	integer.cpp \
+	bitvector.h \
+	bitvector.cpp \
+	gmp_util.h
diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
new file mode 100644
index 000000000..bea06f71a
--- /dev/null
+++ b/src/util/bitvector.cpp
@@ -0,0 +1,16 @@
+/*
+ * bitvector.cpp
+ *
+ *  Created on: Apr 5, 2010
+ *      Author: dejan
+ */
+
+#include "bitvector.h"
+
+namespace CVC4 {
+
+std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
+  return os << bv.toString();
+}
+
+}
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
new file mode 100644
index 000000000..3859fa407
--- /dev/null
+++ b/src/util/bitvector.h
@@ -0,0 +1,99 @@
+/*
+ * bitvector.h
+ *
+ *  Created on: Mar 31, 2010
+ *      Author: dejan
+ */
+
+#ifndef __CVC4__BITVECTOR_H_
+#define __CVC4__BITVECTOR_H_
+
+#include <string>
+#include <iostream>
+#include "util/gmp_util.h"
+
+namespace CVC4 {
+
+class BitVector {
+
+private:
+
+  unsigned d_size;
+  mpz_class d_value;
+
+  BitVector(unsigned size, const mpz_class& val) : d_size(size), d_value(val) {}
+
+public:
+
+  BitVector(unsigned size = 0)
+  : d_size(size), d_value(0) {}
+
+  BitVector(unsigned size, unsigned int z)
+  : d_size(size), d_value(z) {}
+
+  BitVector(unsigned size, unsigned long int z)
+  : d_size(size), d_value(z) {}
+
+  BitVector(unsigned size, const BitVector& q)
+  : d_size(size), d_value(q.d_value) {}
+
+  ~BitVector() {}
+
+  BitVector& operator =(const BitVector& x) {
+    if(this == &x)
+      return *this;
+    d_value = x.d_value;
+    return *this;
+  }
+
+  bool operator ==(const BitVector& y) const {
+    if (d_size != y.d_size) return false;
+    return d_value == y.d_value;
+  }
+
+  bool operator !=(const BitVector& y) const {
+    if (d_size == y.d_size) return false;
+    return d_value != y.d_value;
+  }
+
+  BitVector operator +(const BitVector& y) const {
+    return BitVector(std::max(d_size, y.d_size), d_value + y.d_value);
+  }
+
+  BitVector operator -(const BitVector& y) const {
+    return *this + ~y + 1;
+  }
+
+  BitVector operator -() const {
+    return ~(*this) + 1;
+  }
+
+  BitVector operator *(const BitVector& y) const {
+    return BitVector(d_size, d_value * y.d_value);
+  }
+
+  BitVector operator ~() const {
+    return BitVector(d_size, d_value);
+  }
+
+  size_t hash() const {
+    return gmpz_hash(d_value.get_mpz_t());
+  }
+
+  std::string toString(unsigned int base = 2) const {
+    return d_value.get_str(base);
+  }
+};
+
+struct BitVectorHashStrategy {
+  static inline size_t hash(const BitVector& bv) {
+    return bv.hash();
+  }
+};
+
+std::ostream& operator <<(std::ostream& os, const BitVector& bv);
+
+}
+
+
+#endif /* __CVC4__BITVECTOR_H_ */
diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
new file mode 100644
index 000000000..1849974cd
--- /dev/null
+++ b/src/util/gmp_util.h
@@ -0,0 +1,28 @@
+/*
+ * gmp.h
+ *
+ *  Created on: Apr 5, 2010
+ *      Author: dejan
+ */
+
+#ifndef __CVC4__GMP_H_
+#define __CVC4__GMP_H_
+
+#include <gmpxx.h>
+
+namespace CVC4 {
+
+  /** Hashes the gmp integer primitive in a word by word fashion. */
+  inline size_t gmpz_hash(const mpz_t toHash) {
+    size_t hash = 0;
+    for (int i=0, n=mpz_size(toHash); i<n; ++i){
+      mp_limb_t limb = mpz_getlimbn(toHash, i);
+      hash = hash * 2;
+      hash = hash xor limb;
+    }
+    return hash;
+  }
+
+}
+
+#endif /* __CVC4__GMP_H_ */
diff --git a/src/util/integer.cpp b/src/util/integer.cpp
index 3a7851eec..a26f2108f 100644
--- a/src/util/integer.cpp
+++ b/src/util/integer.cpp
@@ -23,6 +23,6 @@
 
 using namespace CVC4;
 
-std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n){
+std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
   return os << n.toString();
 }
diff --git a/src/util/integer.h b/src/util/integer.h
index c1e5d90ea..2aa8b711a 100644
--- a/src/util/integer.h
+++ b/src/util/integer.h
@@ -18,22 +18,12 @@
 #ifndef __CVC4__INTEGER_H
 #define __CVC4__INTEGER_H
 
-#include <gmpxx.h>
 #include <string>
+#include <iostream>
+#include "util/gmp_util.h"
 
 namespace CVC4 {
 
-/** Hashes the gmp integer primitive in a word by word fashion. */
-inline size_t gmpz_hash(const mpz_t toHash){
-  size_t hash = 0;
-  for (int i=0, n=mpz_size(toHash); i<n; ++i){
-    mp_limb_t limb = mpz_getlimbn(toHash, i);
-    hash = hash * 2;
-    hash = hash xor limb;
-  }
-  return hash;
-}
-
 class Rational;
 
 class Integer {
diff --git a/src/util/rational.h b/src/util/rational.h
index 48b00899a..e4f0e2bb7 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -24,9 +24,8 @@
 #ifndef __CVC4__RATIONAL_H
 #define __CVC4__RATIONAL_H
 
-#include <gmpxx.h>
 #include <string>
-#include "integer.h"
+#include "util/integer.h"
 
 namespace CVC4 {
 
@@ -76,20 +75,20 @@ public:
   /**
    * Constructs a canonical Rational from a numerator and denominator.
    */
-  Rational(  signed int n,   signed int d) : d_value(n,d) {
+  Rational(signed int n, signed int d) : d_value(n,d) {
     d_value.canonicalize();
   }
   Rational(unsigned int n, unsigned int d) : d_value(n,d) {
     d_value.canonicalize();
   }
-  Rational(  signed long int n,   signed long int d) : d_value(n,d) {
+  Rational(signed long int n, signed long int d) : d_value(n,d) {
     d_value.canonicalize();
   }
   Rational(unsigned long int n, unsigned long int d) : d_value(n,d) {
     d_value.canonicalize();
   }
 
-  Rational(const Integer& n, const Integer& d):
+  Rational(const Integer& n, const Integer& d) :
     d_value(n.get_mpz(), d.get_mpz())
   {
     d_value.canonicalize();