From 0906dbc4068c839bd9c2bfe20475edc2f6196048 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Fri, 2 Oct 2009 21:36:33 +0000 Subject: [PATCH] more AST reorganization git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@273 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/AST.h | 108 ----------------------------------------- src/AST/ASTBVConst.cpp | 22 +++++++++ src/AST/ASTBVConst.h | 18 +------ src/AST/ASTInternal.h | 18 ++++--- src/AST/ASTNode.cpp | 92 +++++++++++++++++++++++++++++++++++ src/AST/ASTSymbol.cpp | 22 +++++++++ src/AST/ASTSymbol.h | 16 +----- 7 files changed, 152 insertions(+), 144 deletions(-) diff --git a/src/AST/AST.h b/src/AST/AST.h index abf800a..c73525d 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -44,10 +44,6 @@ namespace BEEV ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTNodeCountMap; -// typedef hash_map IntToASTVecMap; - // Function to dump contents of ASTNodeMap ostream &operator<<(ostream &os, const ASTNodeMap &nmap); @@ -902,110 +898,6 @@ namespace BEEV * INLINE METHODS from various classed, declared here because of * dependencies on classes that are declared later. *****************************************************************/ - // ASTNode accessor function. - inline Kind ASTNode::GetKind() const - { - //cout << "GetKind: " << _int_node_ptr; - return _int_node_ptr->GetKind(); - } - - // FIXME: should be const ASTVec const? - // Declared here because of same ordering problem as GetKind. - inline const ASTVec &ASTNode::GetChildren() const - { - return _int_node_ptr->GetChildren(); - } - - // Access node number - inline int ASTNode::GetNodeNum() const - { - return _int_node_ptr->_node_num; - } - - inline unsigned int ASTNode::GetIndexWidth() const - { - return _int_node_ptr->_index_width; - } - - inline void ASTNode::SetIndexWidth(unsigned int iw) const - { - _int_node_ptr->_index_width = iw; - } - - inline unsigned int ASTNode::GetValueWidth() const - { - return _int_node_ptr->_value_width; - } - - inline void ASTNode::SetValueWidth(unsigned int vw) const - { - _int_node_ptr->_value_width = vw; - } - - //return the type of the ASTNode: 0 iff BOOLEAN; 1 iff BITVECTOR; 2 - //iff ARRAY; 3 iff UNKNOWN; - inline types ASTNode::GetType() const - { - if ((GetIndexWidth() == 0) && (GetValueWidth() == 0)) //BOOLEAN - return BOOLEAN_TYPE; - if ((GetIndexWidth() == 0) && (GetValueWidth() > 0)) //BITVECTOR - return BITVECTOR_TYPE; - if ((GetIndexWidth() > 0) && (GetValueWidth() > 0)) //ARRAY - return ARRAY_TYPE; - return UNKNOWN_TYPE; - } - - // Constructor; creates a new pointer, increments refcount of - // pointed-to object. - inline ASTNode::ASTNode(ASTInternal *in) : - _int_node_ptr(in) - { - if (in) - in->IncRef(); - } - - // Assignment. Increment refcount of new value, decrement refcount of - // old value and destroy if this was the last pointer. FIXME: - // accelerate this by creating an intnode with a ref counter instead - // of pointing to NULL. Need a special check in CleanUp to make sure - // the null node never gets freed. - - inline ASTNode& ASTNode::operator=(const ASTNode& n) - { - if (n._int_node_ptr) - { - n._int_node_ptr->IncRef(); - } - if (_int_node_ptr) - { - _int_node_ptr->DecRef(); - } - _int_node_ptr = n._int_node_ptr; - return *this; - } - - inline void ASTInternal::DecRef() - { - if (--_ref_count == 0) - { - // Delete node from unique table and kill it. - CleanUp(); - } - } - - // Destructor - inline ASTNode::~ASTNode() - { - if (_int_node_ptr) - { - _int_node_ptr->DecRef(); - } - } - - inline BeevMgr* ASTNode::GetBeevMgr() const - { - return GlobalBeevMgr; - } //Return the unsigned constant value of the input 'n' inline unsigned int GetUnsignedConst(const ASTNode n) diff --git a/src/AST/ASTBVConst.cpp b/src/AST/ASTBVConst.cpp index 848a406..3238ee2 100644 --- a/src/AST/ASTBVConst.cpp +++ b/src/AST/ASTBVConst.cpp @@ -95,5 +95,27 @@ namespace BEEV { return _bvconst; } //End of GetBVConst() + + /**************************************************************** + * Class ASTBVConstHasher and ASTBVConstEqual Functions * + ****************************************************************/ + + size_t ASTBVConst::ASTBVConstHasher::operator()(const ASTBVConst * bvc) const + { + return CONSTANTBV::BitVector_Hash(bvc->_bvconst); + } //End of ASTBVConstHasher operator + + + bool ASTBVConst::ASTBVConstEqual::operator()(const ASTBVConst * bvc1, + const ASTBVConst * bvc2) const + { + if (bvc1->_value_width != bvc2->_value_width) + { + return false; + } + return (0 == + CONSTANTBV::BitVector_Compare(bvc1->_bvconst, + bvc2->_bvconst)); + } //End of ASTBVConstEqual operator };//End of namespace diff --git a/src/AST/ASTBVConst.h b/src/AST/ASTBVConst.h index da00034..88cd6c7 100644 --- a/src/AST/ASTBVConst.h +++ b/src/AST/ASTBVConst.h @@ -43,11 +43,7 @@ namespace BEEV class ASTBVConstHasher { public: - size_t operator()(const ASTBVConst * bvc) const - { - return CONSTANTBV::BitVector_Hash(bvc->_bvconst); - } - ; + size_t operator()(const ASTBVConst * bvc) const; }; //End of class ASTBVConstHahser /**************************************************************** @@ -59,19 +55,9 @@ namespace BEEV { public: bool operator()(const ASTBVConst * bvc1, - const ASTBVConst * bvc2) const - { - if (bvc1->_value_width != bvc2->_value_width) - { - return false; - } - return (0 == - CONSTANTBV::BitVector_Compare(bvc1->_bvconst, - bvc2->_bvconst)); - } + const ASTBVConst * bvc2) const; }; //End of class ASTBVConstEqual - /**************************************************************** * Private Functions (virtual defs and friends) * ****************************************************************/ diff --git a/src/AST/ASTInternal.h b/src/AST/ASTInternal.h index b0d1a91..0547384 100644 --- a/src/AST/ASTInternal.h +++ b/src/AST/ASTInternal.h @@ -155,22 +155,28 @@ namespace BEEV void IncRef() { ++_ref_count; - } + } //End of IncRef() // Decrement Reference Count - void DecRef(); + void DecRef() + { + if (--_ref_count == 0) + { + // Delete node from unique table and kill it. + CleanUp(); + } + }//End of DecRef() int GetNodeNum() const { return _node_num; - } + } //End of GetNodeNum() void SetNodeNum(int nn) { _node_num = nn; - } - ; - }; //End of Class ASTInternal + } //End of SetNodeNum() + }; //End of Class ASTInternal }; //end of namespace #endif diff --git a/src/AST/ASTNode.cpp b/src/AST/ASTNode.cpp index 685d0ad..55485c4 100644 --- a/src/AST/ASTNode.cpp +++ b/src/AST/ASTNode.cpp @@ -13,6 +13,16 @@ ********************************************************************/ namespace BEEV { + // Constructor; + // + // creates a new pointer, increments refcount of pointed-to object. + inline ASTNode::ASTNode(ASTInternal *in) : + _int_node_ptr(in) + { + if (in) + in->IncRef(); + } //End of Constructor + // Copy constructor. Maintain _ref_count ASTNode::ASTNode(const ASTNode &n) : _int_node_ptr(n._int_node_ptr) @@ -23,6 +33,88 @@ namespace BEEV } } //End of Copy Constructor for ASTNode + // ASTNode accessor function. + inline Kind ASTNode::GetKind() const + { + //cout << "GetKind: " << _int_node_ptr; + return _int_node_ptr->GetKind(); + } //End of GetKind() + + // Declared here because of same ordering problem as GetKind. + inline const ASTVec &ASTNode::GetChildren() const + { + return _int_node_ptr->GetChildren(); + } //End of GetChildren() + + // Access node number + inline int ASTNode::GetNodeNum() const + { + return _int_node_ptr->_node_num; + } //End of GetNodeNum() + + inline unsigned int ASTNode::GetIndexWidth() const + { + return _int_node_ptr->_index_width; + } //End of GetIndexWidth() + + inline void ASTNode::SetIndexWidth(unsigned int iw) const + { + _int_node_ptr->_index_width = iw; + } //End of SetIndexWidth() + + inline unsigned int ASTNode::GetValueWidth() const + { + return _int_node_ptr->_value_width; + } //End of GetValueWidth() + + inline void ASTNode::SetValueWidth(unsigned int vw) const + { + _int_node_ptr->_value_width = vw; + } //End of SetValueWidth() + + //return the type of the ASTNode: + // + // 0 iff BOOLEAN; 1 iff BITVECTOR; 2 iff ARRAY; 3 iff UNKNOWN; + inline types ASTNode::GetType() const + { + if ((GetIndexWidth() == 0) && (GetValueWidth() == 0)) //BOOLEAN + return BOOLEAN_TYPE; + if ((GetIndexWidth() == 0) && (GetValueWidth() > 0)) //BITVECTOR + return BITVECTOR_TYPE; + if ((GetIndexWidth() > 0) && (GetValueWidth() > 0)) //ARRAY + return ARRAY_TYPE; + return UNKNOWN_TYPE; + } //End of GetType() + + // Assignment + inline ASTNode& ASTNode::operator=(const ASTNode& n) + { + if (n._int_node_ptr) + { + n._int_node_ptr->IncRef(); + } + if (_int_node_ptr) + { + _int_node_ptr->DecRef(); + } + _int_node_ptr = n._int_node_ptr; + return *this; + } //End of operator= + + // Destructor + inline ASTNode::~ASTNode() + { + if (_int_node_ptr) + { + _int_node_ptr->DecRef(); + } + } //End of Destructor() + + inline BeevMgr* ASTNode::GetBeevMgr() const + { + return GlobalBeevMgr; + } //End of GetBeevMgr() + // Checks if the node has alreadybeen printed or not bool ASTNode::IsAlreadyPrinted() const { diff --git a/src/AST/ASTSymbol.cpp b/src/AST/ASTSymbol.cpp index 4468ac0..fa40a44 100644 --- a/src/AST/ASTSymbol.cpp +++ b/src/AST/ASTSymbol.cpp @@ -35,4 +35,26 @@ namespace BEEV free((char*) this->_name); delete this; }//End of cleanup() + + + /**************************************************************** + * ASTSymbolHasher and ASTSymbolEqual functions * + * * + ****************************************************************/ + size_t + ASTSymbol::ASTSymbolHasher::operator()(const ASTSymbol *sym_ptr) const + { +#ifdef TR1_UNORDERED_MAP + tr1::hash h; +#else + hash h; +#endif + return h(sym_ptr->_name); + } //End of ASTSymbolHasher operator + + bool ASTSymbol::ASTSymbolEqual::operator()(const ASTSymbol *sym_ptr1, + const ASTSymbol *sym_ptr2) const + { + return (*sym_ptr1 == *sym_ptr2); + } //End of ASTSymbolEqual operator };//end of namespace diff --git a/src/AST/ASTSymbol.h b/src/AST/ASTSymbol.h index 27598ba..06ec3dd 100644 --- a/src/AST/ASTSymbol.h +++ b/src/AST/ASTSymbol.h @@ -39,16 +39,7 @@ namespace BEEV class ASTSymbolHasher { public: - size_t operator()(const ASTSymbol *sym_ptr) const - { -#ifdef TR1_UNORDERED_MAP - tr1::hash h; -#else - hash h; -#endif - return h(sym_ptr->_name); - } - ; + size_t operator()(const ASTSymbol *sym_ptr) const; }; // End of class ASTSymbolHasher /**************************************************************** @@ -60,10 +51,7 @@ namespace BEEV { public: bool operator()(const ASTSymbol *sym_ptr1, - const ASTSymbol *sym_ptr2) const - { - return (*sym_ptr1 == *sym_ptr2); - } + const ASTSymbol *sym_ptr2) const; }; //End of class ASTSymbolEqual friend bool operator==(const ASTSymbol &sym1, -- 2.47.3