Add -DTR1_UNORDERED_MAP, analogous to -DEXT_HASH_MAP, to allow use of

another, newer, quasi-standard STL hash table class.

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

diff --git a/AST/AST.h b/AST/AST.h
index 58b6d7a04dc8f38e6fa0b09562d0d87f3f588085..fb6f6491510c71653a9e171a6afea849810c49f9 100644 (file)
--- a/AST/AST.h
+++ b/AST/AST.h
@@ -15,6 +15,12 @@
 #ifdef EXT_HASH_MAP
 #include <ext/hash_set>
 #include <ext/hash_map>
+#elif defined(TR1_UNORDERED_MAP)
+#include <tr1/unordered_map>
+#include <tr1/unordered_set>
+#define hash_map tr1::unordered_map
+#define hash_set tr1::unordered_set
+#define hash_multiset tr1::unordered_multiset
 #else
 #include <hash_set>
 #include <hash_map>
@@ -24,6 +30,7 @@
 #include <string>
 #include <map>
 #include <set>
+#include <algorithm>
 #include "ASTUtil.h"
 #include "ASTKind.h"
 #include "../sat/core/Solver.h"
@@ -543,7 +550,11 @@ 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); 
       };
     };

diff --git a/AST/ASTUtil.h b/AST/ASTUtil.h
index bd49c84573c890b2a7d1ded06b1f0cb25fc99626..9ae42553fe8cafb796ca16f764a7b4e3f958551b 100644 (file)
--- a/AST/ASTUtil.h
+++ b/AST/ASTUtil.h
@@ -15,6 +15,9 @@
 #ifdef EXT_HASH_MAP
 #include <ext/hash_set>
 #include <ext/hash_map>
+#elif defined(TR1_UNORDERED_MAP)
+#include <tr1/unordered_map>
+#include <tr1/unordered_set>
 #else
 #include <hash_set>
 #include <hash_map>
@@ -97,8 +100,13 @@ 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;
+#else
   typedef hash_map<const char*,int, 
                   hash<char *>,eqstr> function_counters;
+#endif
 
   void CountersAndStats(const char * functionname);