shaved off 4 bytes from each ASTInternal node

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@268 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/INSTALL b/INSTALL
index 094a8502a6d308c67b142a08f6f1465114e68517..17ca581e37804471aa2e9fa91fa19e69bceafde1 100644 (file)
--- a/INSTALL
+++ b/INSTALL
@@ -22,5 +22,5 @@
 
 3. Run tests:
 
-   make regressall
+   make regresscapi && make regresscvc && make regresssmt
 

diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp
index 35caa2ac8510d5e30fa63204f2c724df4a99d752..69b13aba2f14e617f703e316dca28b5a350360d7 100644 (file)
--- a/src/AST/AST.cpp
+++ b/src/AST/AST.cpp
@@ -1001,7 +1001,7 @@ namespace BEEV
         cout << a << endl;
       }
     cout << "Node size is: ";
-    cout << NodeSize(a) << endl << endl;
+    cout << NodeSize(a) << endl;
   }
 
   unsigned int BeevMgr::NodeSize(const ASTNode& a, bool clearStatInfo)
@@ -1016,6 +1016,8 @@ namespace BEEV
 
     //record that you have seen this node already
     StatInfoSet.insert(a);
+    // cout << "Number of bytes per Node is: ";
+    // cout << sizeof(*(a._int_node_ptr)) << endl;
 
     //leaf node has a size of 1
     if (a.Degree() == 0)

diff --git a/src/AST/AST.h b/src/AST/AST.h
index fff6f7662dcecceeefdb2121984128f3bafc851d..e0eb3c744150db103624cf2c9f2664268c175f1e 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -64,6 +64,28 @@ namespace BEEV
   class ASTBVConst;
   class BVSolver;
 
+
+  template <class E, class T>
+  struct enumeration
+  {
+    typedef T type;
+    typedef E enum_type;
+
+    enumeration()
+      : e_(E())
+    {}
+    
+    enumeration(E e)
+      : e_(static_cast<T>(e))
+    {}
+    
+    operator E() const
+    { return static_cast<E>(e_); }
+    
+  private:
+    T e_;
+  };
+
   //Useful typedefs: Vector of ASTNodes, used for child nodes among
   //other things.
   typedef vector<ASTNode> ASTVec;
@@ -87,7 +109,6 @@ namespace BEEV
                                         int indentation = 0);
 
   private:
-    // FIXME: make this into a reference?
     ASTInternal * _int_node_ptr; // The real data.
 
     // Usual constructor.
@@ -398,7 +419,8 @@ namespace BEEV
     int _ref_count;
 
     // Kind.  It's a type tag and the operator.
-    Kind _kind;
+    //Kind _kind;
+    enumeration<Kind,unsigned char> _kind;
 
     // The vector of children (*** should this be in ASTInterior? ***)
     ASTVec _children;
@@ -416,12 +438,12 @@ namespace BEEV
     // Length of bitvector type for array index.  The term is an
     // array iff this is positive.  Otherwise, the term is a bitvector
     // or a bit.
-    unsigned int _index_width;
+    unsigned short _index_width;
 
     // Length of bitvector type for scalar value or array element.
     // If this is one, the term represents a single bit (same as a bitvector
     // of length 1).  It must be 1 or greater.
-    unsigned int _value_width;
+    unsigned short _value_width;
 
     // Increment refcount.
     void IncRef()