From 483e071d035595367fd3a481a0ad61fbaee3c648 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 24 Mar 2011 01:28:52 +0000 Subject: [PATCH] Improvement. No longer have vectors in the ASTSymbol and ASTBVConst nodes (which are always leaves). This saves 24 bytes per node. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1233 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ASTBVConst.cpp | 4 +++- src/AST/ASTBVConst.h | 8 +++++++ src/AST/ASTInterior.h | 9 +++---- src/AST/ASTInternal.h | 30 ++++-------------------- src/AST/ASTInternalWithChildren.h | 39 +++++++++++++++++++++++++++++++ src/AST/ASTSymbol.cpp | 3 +++ src/AST/ASTSymbol.h | 11 +++++++-- 7 files changed, 71 insertions(+), 33 deletions(-) create mode 100644 src/AST/ASTInternalWithChildren.h diff --git a/src/AST/ASTBVConst.cpp b/src/AST/ASTBVConst.cpp index dae19e2..82ba82f 100644 --- 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 32cba9a..8b45905 100644 --- 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 854dec4..9c5a49a 100644 --- 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 1843c1e..31910b4 100644 --- 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; - // 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 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 b047d9d..bc29bd8 100644 --- 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 c30b558..2658686 100644 --- 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); } -- 2.47.3