From 6dbb71dfedb18465c861a5bb67aa7e4af5c5751c Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Mon, 12 Oct 2009 20:48:11 +0000 Subject: [PATCH] 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 --- src/AST/AST.h | 10 +++--- src/AST/ASTUtil.h | 32 ++++++++++++------- src/AST/UsefulDefs.h | 5 +-- src/STPManager/STPManager.h | 8 ++--- .../AbsRefine_CounterExample.h | 6 ++-- .../CounterExample.cpp | 10 +++--- src/printer/dotPrinter.cpp | 4 +-- src/to-sat/ToCNF.h | 4 +-- src/to-sat/ToSAT.h | 2 +- 9 files changed, 46 insertions(+), 35 deletions(-) diff --git a/src/AST/AST.h b/src/AST/AST.h index f68f314..19d48eb 100644 --- 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 6a8c94a..e69aa59 100644 --- a/src/AST/ASTUtil.h +++ b/src/AST/ASTUtil.h @@ -12,18 +12,22 @@ #include #include +#include + #ifdef EXT_HASH_MAP -#include -#include + #include + #include #elif defined(TR1_UNORDERED_MAP) -#include -#include + #include + #include #else -#include -#include + #include + #include #endif -#include +#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,eqstr> function_counters; + typedef tr1::unordered_map< + const char*, + int, + tr1::hash, + eqstr> function_counters; #else - typedef hash_map,eqstr> function_counters; + typedef HASHMAP< + const char*, + int, + hash, + eqstr> function_counters; #endif void CountersAndStats(const char * functionname); diff --git a/src/AST/UsefulDefs.h b/src/AST/UsefulDefs.h index 66e6597..473cad8 100644 --- 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 56cf1ed..6ed7130 100644 --- 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 d85b5ac..6a2ec50 100644 --- 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 *, + HASHMAP *, 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 * w, unsigned int l); + ASTNode BoolVectoBVConst(HASHMAP * w, unsigned int l); public: diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index 53f613c..39e892f 100644 --- 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 * v; + HASHMAP * v; if (_ASTNode_to_Bitvector.find(symbol) == _ASTNode_to_Bitvector.end()) _ASTNode_to_Bitvector[symbol] = - new hash_map (symbolWidth); + new HASHMAP (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 * w = it->second; + HASHMAP * 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 * w, unsigned int l) + ASTNode AbsRefine_CounterExample::BoolVectoBVConst(HASHMAP * 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 1fdb0b7..3881d84 100644 --- 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 *alreadyOutput) + void Dot_Print1(ostream &os, const ASTNode n, HASHSET *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 alreadyOutput; + HASHSET alreadyOutput; Dot_Print1(os, n, &alreadyOutput); diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h index f2e6fd2..15cf28c 100644 --- 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 f267e6a..0b7b753 100644 --- 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, -- 2.47.3