Improvement. No longer have vectors in the ASTSymbol and ASTBVConst nodes (which...

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

diff --git a/src/AST/ASTBVConst.cpp b/src/AST/ASTBVConst.cpp
index dae19e20952028c8481ccffdb2d8cddb1c09673c..82ba82f1cc4afffb9a953c95fb0027a4a8175e96 100644 (file)
--- a/src/AST/ASTBVConst.cpp
+++ b/src/AST/ASTBVConst.cpp
@@ -11,6 +11,8 @@
 #include "../STPManager/STP.h"
 namespace BEEV
 {
+  const ASTVec ASTBVConst::astbv_empty_children;
+
   /****************************************************************
    * ASTBVConst Member Function definitions                       *
    ****************************************************************/
@@ -26,7 +28,7 @@ namespace BEEV
 
   // Copy constructor.
   ASTBVConst::ASTBVConst(const ASTBVConst &sym) :
-    ASTInternal(sym._kind, sym._children)
+    ASTInternal(sym._kind)
   {
     _bvconst = CONSTANTBV::BitVector_Clone(sym._bvconst);
     _value_width = sym._value_width;

diff --git a/src/AST/ASTBVConst.h b/src/AST/ASTBVConst.h
index 32cba9a1275f8a6d89a0bdfe8ae60779921f2eb7..8b45905560cfcc8f57d25175ee49154b2a70a742 100644 (file)
--- a/src/AST/ASTBVConst.h
+++ b/src/AST/ASTBVConst.h
@@ -101,8 +101,16 @@ namespace BEEV
     // compilers will accept)
     virtual void nodeprint(ostream& os, bool c_friendly = false);
     
+    const static ASTVec astbv_empty_children;
+
   public:
 
+    virtual ASTVec const &
+    GetChildren() const
+    {
+      return astbv_empty_children;
+    }
+
     /****************************************************************
      * Public Member Functions                                      *
      ****************************************************************/

diff --git a/src/AST/ASTInterior.h b/src/AST/ASTInterior.h
index 854dec440693cd9f592322c959a4553304470d38..9c5a49a0ef59c19f7bb14222d587ebe75dfd27a5 100644 (file)
--- a/src/AST/ASTInterior.h
+++ b/src/AST/ASTInterior.h
@@ -11,6 +11,7 @@
 #define ASTINTERIOR_H
 
 #include "UsefulDefs.h"
+#include "ASTInternalWithChildren.h"
 namespace BEEV
 {
   class ASTNode;
@@ -23,7 +24,7 @@ namespace BEEV
    * Internal representation of an interior ASTNode.Generally, these*
    * nodes should have at least one child                           * 
    ******************************************************************/
-  class ASTInterior: public ASTInternal
+  class ASTInterior: public ASTInternalWithChildren
   {
 
     friend class STPMgr;
@@ -82,18 +83,18 @@ namespace BEEV
      ******************************************************************/
     
     // Basic constructors
-    ASTInterior(Kind kind) : ASTInternal(kind)
+    ASTInterior(Kind kind) : ASTInternalWithChildren(kind)
     {
     }
 
-    ASTInterior(Kind kind, ASTVec &children) : ASTInternal(kind, children)
+    ASTInterior(Kind kind, ASTVec &children) : ASTInternalWithChildren(kind, children)
     {
     }
 
     //Copy constructor.  This copies the contents of the child nodes
     //array, along with everything else. Assigning the smart pointer,
     //ASTNode, does NOT invoke this.
-    ASTInterior(const ASTInterior &int_node) : ASTInternal(int_node)
+    ASTInterior(const ASTInterior &int_node) : ASTInternalWithChildren(int_node)
     {
     }
 

diff --git a/src/AST/ASTInternal.h b/src/AST/ASTInternal.h
index 1843c1e33c711b3d28c24d72bf3c32b4900bc120..31910b488dc9b790aaf5206e3f89865f6d2a7253 100644 (file)
--- a/src/AST/ASTInternal.h
+++ b/src/AST/ASTInternal.h
@@ -61,14 +61,10 @@ namespace BEEV
     // Kind. It's a type tag and the operator.
     enumeration<Kind,unsigned char> _kind;
 
-    // The vector of children
-    ASTVec _children;
-
     //Nodenum is a unique positive integer for the node.  The nodenum
     //of a node should always be greater than its descendents (which
     //is easily achieved by incrementing the number each time a new
     //node is created).
-    //FIXME: Get rid of this
     unsigned int _node_num;
 
     /*******************************************************************
@@ -78,11 +74,8 @@ namespace BEEV
      *                                                                 *
      * Width of the index of an array. Positive for array, 0 otherwise *
      *******************************************************************/
-#ifdef LESSBYTES_PERNODE
-    unsigned char _index_width;
-#else
     unsigned int  _index_width;
-#endif
+
 
     /*******************************************************************
      * ASTNode is of type BV      <==> ((indexwidth=0)&&(valuewidth>0))*
@@ -91,11 +84,7 @@ namespace BEEV
      *                                                                 *
      * Number of bits of bitvector. +ve for array/bitvector,0 otherwise*
      *******************************************************************/
-#ifdef LESSBYTES_PERNODE
-    unsigned char _value_width;
-#else
     unsigned int  _value_width;
-#endif
 
     /****************************************************************
      * Protected Member Functions                                   *
@@ -127,10 +116,7 @@ namespace BEEV
     }
 
     // Get the child nodes of this node
-    virtual ASTVec const &GetChildren() const
-    {
-      return _children;
-    }
+    virtual ASTVec const &GetChildren() const = 0;
 
   public:
 
@@ -154,14 +140,6 @@ namespace BEEV
     {
     }
 
-    // Constructor (kind and children).
-    ASTInternal(Kind kind, const ASTVec &children, int nodenum = 0) :
-      _ref_count(0), _kind(kind), _children(children), 
-      _node_num(nodenum),
-      _index_width(0), _value_width(0)
-    {
-    }
-
     // Copy constructor.  This copies the contents of the child nodes
     // array, along with everything else.  Assigning the smart pointer,
     // ASTNode, does NOT invoke this; This should only be used for
@@ -169,9 +147,9 @@ namespace BEEV
     // FIXME:  I don't think children need to be copied.
     ASTInternal(const ASTInternal &int_node, int nodenum = 0) :
       _ref_count(0), _kind(int_node._kind), 
-      _children(int_node._children),
+      //_children(int_node._children),
       _node_num(int_node._node_num), 
-      _index_width(int_node._index_width), 
+      _index_width(int_node._index_width),
       _value_width(int_node._value_width)
     {
     }

diff --git a/src/AST/ASTInternalWithChildren.h b/src/AST/ASTInternalWithChildren.h
new file mode 100644 (file)
index 0000000..c744dcb
--- /dev/null
+++ b/src/AST/ASTInternalWithChildren.h
@@ -0,0 +1,39 @@
+#ifndef ASTINTERNALWithChildren_H
+#define ASTINTERNALWithChildren_H
+
+/*
+ * Leaf objects like Symbols and BVConsts don't need a vector of
+ * children. On a 64-bit machine, a vector object is 24 bytes. So
+ * splitting the two objects apart saves 24 bytes for those objects.
+ */
+
+namespace BEEV
+{
+  class ASTInternalWithChildren : public ASTInternal
+  {
+
+  protected:
+    // The vector of children
+    ASTVec _children;
+
+  public:
+
+    virtual ASTVec const &GetChildren() const
+    {
+      return _children;
+    }
+
+    // Constructor (kind and children).
+    ASTInternalWithChildren(Kind kind, const ASTVec &children, int nodenum = 0) :
+      ASTInternal(kind,nodenum), _children(children)
+    {
+    }
+
+    // Constructor (kind only, empty children, int nodenum)
+    ASTInternalWithChildren(Kind kind, int nodenum = 0) :
+      ASTInternal(kind,nodenum)
+    {
+    }
+  }; //End of Class ASTInternalBase
+}; //end of namespace
+#endif

diff --git a/src/AST/ASTSymbol.cpp b/src/AST/ASTSymbol.cpp
index b047d9d213d89c19e4ecd59388dfba65ba157340..bc29bd88c6a822e9fd58aaf3626833cce41a4bdf 100644 (file)
--- a/src/AST/ASTSymbol.cpp
+++ b/src/AST/ASTSymbol.cpp
@@ -11,6 +11,9 @@
 #include "../STPManager/STP.h"
 namespace BEEV
 {
+  const ASTVec ASTSymbol::empty_children;
+
+
   /****************************************************************
    * ASTSymbol Member Function definitions                        *
    ****************************************************************/

diff --git a/src/AST/ASTSymbol.h b/src/AST/ASTSymbol.h
index c30b5581ed7626f00005ab565999b64bd67487c3..2658686d256ed936f391c82cdec9ac95738851ed 100644 (file)
--- a/src/AST/ASTSymbol.h
+++ b/src/AST/ASTSymbol.h
@@ -26,6 +26,8 @@ namespace BEEV
     friend class ASTNodeHasher;
     friend class ASTNodeEqual;
 
+    const static ASTVec empty_children;
+
   private:
     /****************************************************************
      * Private Data                                                 *
@@ -95,6 +97,12 @@ namespace BEEV
 
   public:
 
+    virtual ASTVec const &GetChildren() const
+        {
+          return empty_children;
+        }
+
+
     /****************************************************************
      * Public Member Functions                                      *
      ****************************************************************/
@@ -109,7 +117,6 @@ namespace BEEV
     ASTSymbol(const char * const name) :
       ASTInternal(SYMBOL), _name(name)
     {
-      //printf("inside ASTSymbol constructor %s\n", _name);
     }
 
     // Destructor (does nothing, but is declared virtual here.
@@ -119,7 +126,7 @@ namespace BEEV
 
     // Copy constructor
     ASTSymbol(const ASTSymbol &sym) :
-      ASTInternal(sym._kind, sym._children), _name(sym._name)
+      ASTInternal(sym._kind), _name(sym._name)
     {
       //printf("inside ASTSymbol constructor %s\n", _name);
     }