Partial merge from datatypes-merge branch:

1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.

No performance impact is expected outside of datatypes.  I'm verifying that that is the case with a cluster job this morning.

1 files changed, 27 insertions, 25 deletions

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index ca69fb506..ade08164b 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -2,10 +2,10 @@
 /*! \file bitvector.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: cconway
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters, cconway
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -28,7 +28,7 @@
 
 namespace CVC4 {
 
-class BitVector {
+class CVC4_PUBLIC BitVector {
 
 private:
 
@@ -157,24 +157,24 @@ inline BitVector::BitVector(const std::string& num, unsigned base) {
   }
 
   d_value = Integer(num,base);
-}
+}/* BitVector::BitVector() */
 
 
 /**
  * Hash function for the BitVector constants.
  */
-struct BitVectorHashStrategy {
+struct CVC4_PUBLIC BitVectorHashStrategy {
   static inline size_t hash(const BitVector& bv) {
     return bv.hash();
   }
-};
+};/* struct BitVectorHashStrategy */
 
 /**
  * The structure representing the extraction operation for bit-vectors. The
  * operation map bit-vectors to bit-vector of size <code>high - low + 1</code>
  * by taking the bits at indices <code>high ... low</code>
  */
-struct BitVectorExtract  {
+struct CVC4_PUBLIC BitVectorExtract {
   /** The high bit of the range for this extract */
   unsigned high;
   /** The low bit of the range for this extract */
@@ -186,73 +186,75 @@ struct BitVectorExtract  {
   bool operator == (const BitVectorExtract& extract) const {
     return high == extract.high && low == extract.low;
   }
-};
+};/* struct BitVectorExtract */
 
 /**
  * Hash function for the BitVectorExtract objects.
  */
-class BitVectorExtractHashStrategy {
+class CVC4_PUBLIC BitVectorExtractHashStrategy {
 public:
   static size_t hash(const BitVectorExtract& extract) {
     size_t hash = extract.low;
     hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2);
     return hash;
   }
-};
+};/* class BitVectorExtractHashStrategy */
 
-struct BitVectorSize {
+struct CVC4_PUBLIC BitVectorSize {
   unsigned size;
   BitVectorSize(unsigned size)
   : size(size) {}
   operator unsigned () const { return size; }
-};
+};/* struct BitVectorSize */
 
-struct BitVectorRepeat {
+struct CVC4_PUBLIC BitVectorRepeat {
   unsigned repeatAmount;
   BitVectorRepeat(unsigned repeatAmount)
   : repeatAmount(repeatAmount) {}
   operator unsigned () const { return repeatAmount; }
-};
+};/* struct BitVectorRepeat */
 
-struct BitVectorZeroExtend {
+struct CVC4_PUBLIC BitVectorZeroExtend {
   unsigned zeroExtendAmount;
   BitVectorZeroExtend(unsigned zeroExtendAmount)
   : zeroExtendAmount(zeroExtendAmount) {}
   operator unsigned () const { return zeroExtendAmount; }
-};
+};/* struct BitVectorZeroExtend */
 
-struct BitVectorSignExtend {
+struct CVC4_PUBLIC BitVectorSignExtend {
   unsigned signExtendAmount;
   BitVectorSignExtend(unsigned signExtendAmount)
   : signExtendAmount(signExtendAmount) {}
   operator unsigned () const { return signExtendAmount; }
-};
+};/* struct BitVectorSignExtend */
 
-struct BitVectorRotateLeft {
+struct CVC4_PUBLIC BitVectorRotateLeft {
   unsigned rotateLeftAmount;
   BitVectorRotateLeft(unsigned rotateLeftAmount)
   : rotateLeftAmount(rotateLeftAmount) {}
   operator unsigned () const { return rotateLeftAmount; }
-};
+};/* struct BitVectorRotateLeft */
 
-struct BitVectorRotateRight {
+struct CVC4_PUBLIC BitVectorRotateRight {
   unsigned rotateRightAmount;
   BitVectorRotateRight(unsigned rotateRightAmount)
   : rotateRightAmount(rotateRightAmount) {}
   operator unsigned () const { return rotateRightAmount; }
-};
+};/* struct BitVectorRotateRight */
 
 template <typename T>
-struct UnsignedHashStrategy {
+struct CVC4_PUBLIC UnsignedHashStrategy {
   static inline size_t hash(const T& x) {
     return (size_t)x;
   }
-};
+};/* struct UnsignedHashStrategy */
 
+inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) CVC4_PUBLIC;
 inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
   return os << bv.toString();
 }
 
+inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) CVC4_PUBLIC;
 inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
   return os << "[" << bv.high << ":" << bv.low << "]";
 }