From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 30 Sep 2009 23:14:43 +0000 (+0000)
Subject: shaved off 4 bytes from each ASTInternal node
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=eb8bc35940c195791a7a8dd8725baa25823e6804;p=francis%2Fstp.git

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 094a850..17ca581 100644
--- 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 35caa2a..69b13ab 100644
--- 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 fff6f76..e0eb3c7 100644
--- 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()