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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index abf800a8643b9d45696e7c526b53919e2c8263f7..c73525d9901da8e1fed8e8728048238a206983ec 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -44,10 +44,6 @@ namespace BEEV
                    ASTNode::ASTNodeHasher, 
                    ASTNode::ASTNodeEqual> ASTNodeCountMap;
 
-//   typedef hash_map<int32_t,
-//                ASTVec,
-//                hash(int32_t)> 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 848a406bbfb45d16fb763822a7dc901069981bb4..3238ee268db980c22bfc38bb5b4e6230e758c2ce 100644 (file)
--- 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 da00034d43f1b9654ea7561ac526745386bf0629..88cd6c7cebcd4ad55ce75f6596638cd2583dfb02 100644 (file)
--- 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 b0d1a911c9235d77060669ff633d35b23924b3ea..054738498c523770f3582b994c2206b0816f4ae8 100644 (file)
--- 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 685d0ad2b4e55b2bbb8bc40cf34f9857de79c633..55485c42f1042460f38ef253d5fb9a9b169704c6 100644 (file)
--- 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 4468ac0e06ab2a294f2f473dd3dc9c8dfc9fec35..fa40a441c4921985e518fdb8f7a80f7c4c34def4 100644 (file)
--- 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<string> h;
+#else
+    hash<char*> 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 27598ba0a3209501a218067d68e42990a567d6d7..06ec3dde2bd6cfade38f96bcbd801e19481d1b66 100644 (file)
--- 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<string> h;
-#else
-        hash<char*> 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,