replaced hash_map/hash_set with defines HASHMAP and HASHSET resp.

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index f68f31408c81ed6bfbf53d201834d0958908f712..19d48ebc86842c48073481dda86f714d74da7446 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -46,29 +46,29 @@ namespace BEEV
   //Takes a BVCONST and returns its constant value
   unsigned int GetUnsignedConst(const ASTNode n);
 
-  typedef hash_map<
+  typedef HASHMAP<
     ASTNode, 
     ASTNode, 
     ASTNode::ASTNodeHasher, 
     ASTNode::ASTNodeEqual> ASTNodeMap;
 
-  typedef hash_map<
+  typedef HASHMAP<
     ASTNode, 
     int32_t, 
     ASTNode::ASTNodeHasher, 
     ASTNode::ASTNodeEqual> ASTNodeCountMap;
 
-  typedef hash_set<
+  typedef HASHSET<
     ASTNode, 
     ASTNode::ASTNodeHasher, 
     ASTNode::ASTNodeEqual> ASTNodeSet;
 
-  typedef hash_multiset<
+  typedef HASHMULTISET<
     ASTNode, 
     ASTNode::ASTNodeHasher, 
     ASTNode::ASTNodeEqual> ASTNodeMultiSet;
 
-  typedef hash_map<
+  typedef HASHMAP<
     ASTNode, 
     ASTVec, 
     ASTNode::ASTNodeHasher, 

diff --git a/src/AST/ASTUtil.h b/src/AST/ASTUtil.h
index 6a8c94a5b0f96ff50099d2d4f3d8a695910aed2d..e69aa599ec34559ab76ac2c0dbc94b284a61d11e 100644 (file)
--- a/src/AST/ASTUtil.h
+++ b/src/AST/ASTUtil.h
@@ -12,18 +12,22 @@
 
 #include <iostream>
 #include <vector>
+#include <cstring>
+
 #ifdef EXT_HASH_MAP
-#include <ext/hash_set>
-#include <ext/hash_map>
+ #include <ext/hash_set>
+ #include <ext/hash_map>
 #elif defined(TR1_UNORDERED_MAP)
-#include <tr1/unordered_map>
-#include <tr1/unordered_set>
+ #include <tr1/unordered_map>
+ #include <tr1/unordered_set>
 #else
-#include <hash_set>
-#include <hash_map>
+ #include <hash_set>
+ #include <hash_map>
 #endif
 
-#include <cstring>
+#define HASHMAP      hash_map
+#define HASHSET      hash_set
+#define HASHMULTISET hash_multiset
 
 using namespace std;
 namespace BEEV {
@@ -55,11 +59,17 @@ namespace BEEV {
 
   // Table for storing function count stats.
 #ifdef TR1_UNORDERED_MAP
-  typedef tr1::unordered_map<const char*,int,
-    tr1::hash<const char *>,eqstr> function_counters;
+  typedef tr1::unordered_map<
+    const char*,
+    int,
+    tr1::hash<const char *>,
+    eqstr> function_counters;
 #else
-  typedef hash_map<const char*,int,
-    hash<char *>,eqstr> function_counters;
+  typedef HASHMAP<
+    const char*,
+    int,
+    hash<char *>,
+    eqstr> function_counters;
 #endif
 
   void CountersAndStats(const char * functionname);

diff --git a/src/AST/UsefulDefs.h b/src/AST/UsefulDefs.h
index 66e6597b6b45c059b943fc6529f49532d75a5fc3..473cad82a5bf43b4f75f3998a8421955da3b5cd1 100644 (file)
--- a/src/AST/UsefulDefs.h
+++ b/src/AST/UsefulDefs.h
@@ -43,8 +43,9 @@
 #include "../extlib-constbv/constantbv.h"
 #include "RunTimes.h"
 
-#define HASHMAP hash_map;
-#define HASHSET hash_set;
+#define HASHMAP      hash_map
+#define HASHSET      hash_set
+#define HASHMULTISET hash_multiset
 
 namespace BEEV {
 

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 56cf1ed5eef2800b902d6f633572166722bfd171..6ed713076241fac364377f07844085b2a166d16f 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -32,19 +32,19 @@ namespace BEEV
      ****************************************************************/
 
     // Typedef for unique Interior node table.
-    typedef hash_set<
+    typedef HASHSET<
       ASTInterior *, 
       ASTInterior::ASTInteriorHasher, 
       ASTInterior::ASTInteriorEqual> ASTInteriorSet;    
 
     // Typedef for unique Symbol node (leaf) table.
-    typedef hash_set<
+    typedef HASHSET<
       ASTSymbol *, 
       ASTSymbol::ASTSymbolHasher, 
       ASTSymbol::ASTSymbolEqual> ASTSymbolSet;
 
     //Typedef for unique BVConst node (leaf) table.
-    typedef hash_set<
+    typedef HASHSET<
       ASTBVConst *, 
       ASTBVConst::ASTBVConstHasher, 
       ASTBVConst::ASTBVConstEqual> ASTBVConstSet;
@@ -58,7 +58,7 @@ namespace BEEV
     // Table to uniquefy bvconst
     ASTBVConstSet _bvconst_unique_table;
 
-    typedef hash_map<
+    typedef HASHMAP<
       ASTNode, 
       ASTNodeSet,
       ASTNode::ASTNodeHasher, 

diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h
index d85b5ac183ccd4f69c5047af38dcc3d4e46b7f06..6a2ec50851edf0d127fcda1bbb58f2edaf3df025 100644 (file)
--- a/src/absrefine_counterexample/AbsRefine_CounterExample.h
+++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h
@@ -31,9 +31,9 @@ namespace BEEV
       // This map for building/printing counterexamples. MINISAT
       // returns values for each bit (a BVGETBIT Node), and this maps
       // allows us to assemble the bits into bitvectors.
-      typedef hash_map<
+      typedef HASHMAP<
        ASTNode, 
-       hash_map<unsigned int, bool> *, 
+       HASHMAP<unsigned int, bool> *, 
        ASTNode::ASTNodeHasher, 
        ASTNode::ASTNodeEqual> ASTtoBitvectorMap;
 
@@ -71,7 +71,7 @@ namespace BEEV
       void CopySolverMap_To_CounterExample(void);
 
       //Converts a vector of bools to a BVConst
-      ASTNode BoolVectoBVConst(hash_map<unsigned, bool> * w, unsigned int l);
+      ASTNode BoolVectoBVConst(HASHMAP<unsigned, bool> * w, unsigned int l);
 
     public:
 

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index 53f613c0271debd40c0cc391396f748a693f46a2..39e892f1e5d3af8c3a6a293e86082ffe43814bd4 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -52,10 +52,10 @@ namespace BEEV
                 unsigned int symbolWidth = symbol.GetValueWidth();
 
                 //'v' is the map from bit-index to bit-value
-                hash_map<unsigned, bool> * v;
+                HASHMAP<unsigned, bool> * v;
                 if (_ASTNode_to_Bitvector.find(symbol) == _ASTNode_to_Bitvector.end())
                   _ASTNode_to_Bitvector[symbol] = 
-                   new hash_map<unsigned, bool> (symbolWidth);
+                   new HASHMAP<unsigned, bool> (symbolWidth);
 
                 //v holds the map from bit-index to bit-value
                 v = _ASTNode_to_Bitvector[symbol];
@@ -106,7 +106,7 @@ namespace BEEV
           FatalError("ConstructCounterExample: error while constructing counterexample: not a variable: ", var);
 
         //construct the bitvector value
-        hash_map<unsigned, bool> * w = it->second;
+        HASHMAP<unsigned, bool> * w = it->second;
         ASTNode value = BoolVectoBVConst(w, var.GetValueWidth());
         //debugging
         //cerr << value;
@@ -873,12 +873,12 @@ namespace BEEV
   } //end of PrintSATModel()
 
   //FUNCTION: this function accepts a boolvector and returns a BVConst
-  ASTNode AbsRefine_CounterExample::BoolVectoBVConst(hash_map<unsigned, bool> * w, unsigned int l)
+  ASTNode AbsRefine_CounterExample::BoolVectoBVConst(HASHMAP<unsigned, bool> * w, unsigned int l)
   {
     unsigned len = w->size();
     if (l < len)
       FatalError("BoolVectorBVConst : "
-                 "length of bitvector does not match hash_map size:", ASTUndefined, l);
+                 "length of bitvector does not match HASHMAP size:", ASTUndefined, l);
     std::string cc;
     for (unsigned int jj = 0; jj < l; jj++)
       {

diff --git a/src/printer/dotPrinter.cpp b/src/printer/dotPrinter.cpp
index 1fdb0b701023bd5a65c916926870880fb1777e90..3881d84e05b3ee43d5ccf3ac3133169b3e429c1e 100644 (file)
--- a/src/printer/dotPrinter.cpp
+++ b/src/printer/dotPrinter.cpp
@@ -21,7 +21,7 @@ namespace printer
 
   void outputBitVec(const ASTNode n, ostream& os);
 
-  void Dot_Print1(ostream &os, const ASTNode n, hash_set<int> *alreadyOutput)
+  void Dot_Print1(ostream &os, const ASTNode n, HASHSET<int> *alreadyOutput)
   {
 
     // check if this node has already been printed. If so return.
@@ -70,7 +70,7 @@ namespace printer
     os << "digraph G{" << endl;
 
     // create hashmap to hold integers (node numbers).
-    hash_set<int> alreadyOutput;
+    HASHSET<int> alreadyOutput;
 
     Dot_Print1(os, n, &alreadyOutput);
 

diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h
index f2e6fd2e1615ddd589c0433486fc39235cbb4946..15cf28c882063d9106f9c9c97449d43b78e2b7b3 100644 (file)
--- a/src/to-sat/ToCNF.h
+++ b/src/to-sat/ToCNF.h
@@ -36,13 +36,13 @@ namespace BEEV
       };
     } CNFInfo;
 
-    typedef hash_map<
+    typedef HASHMAP<
       ASTNode, 
       CNFInfo*, 
       ASTNode::ASTNodeHasher, 
       ASTNode::ASTNodeEqual> ASTNodeToCNFInfoMap;
 
-    typedef hash_map<
+    typedef HASHMAP<
       ASTNode, 
       ASTNode*, 
       ASTNode::ASTNodeHasher, 

diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index f267e6a93446af195c89c742e0798a916c33abae..0b7b753be277ff8f92406bcd515d7ea53fb35641 100644 (file)
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -35,7 +35,7 @@ namespace BEEV
     // ClauseList returned by CNF converter. For every new boolean
     // variable in ASTClause a new MINISAT::Var is created (these vars
     // typedefs for ints)
-    typedef hash_map<
+    typedef HASHMAP<
       ASTNode, 
       MINISAT::Var, 
       ASTNode::ASTNodeHasher,