From 1e8c04be8e9384d6163bd2154b8e22f657181c1f Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Sun, 15 Dec 2013 17:31:46 -0800
Subject: [PATCH] fixing templates for broken windows hash functions

---
 src/duality/duality.h           |  4 ++--
 src/duality/duality_wrapper.cpp |  2 +-
 src/interp/iz3base.h            | 18 ++++++++++--------
 src/interp/iz3foci.cpp          |  2 +-
 src/interp/iz3translate.cpp     | 11 ++---------
 5 files changed, 16 insertions(+), 21 deletions(-)

diff --git a/src/duality/duality.h b/src/duality/duality.h
index 7729d2175..979071639 100644
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -1011,7 +1011,7 @@ private:
 
 // Allow to hash on nodes and edges in deterministic way
 
-namespace stl_ext {
+namespace hash_space {
   template <>
     class hash<Duality::RPFP::Node *> {
   public:
@@ -1021,7 +1021,7 @@ namespace stl_ext {
   };
 }
 
-namespace stl_ext {
+namespace hash_space {
   template <>
     class hash<Duality::RPFP::Edge *> {
   public:
diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp
index 705d71abe..55883202f 100644
--- a/src/duality/duality_wrapper.cpp
+++ b/src/duality/duality_wrapper.cpp
@@ -606,7 +606,7 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
   void model::show_hash() const {
     std::ostringstream ss;
     model_smt2_pp(ss, m(), *m_model, 0);
-    stl_ext::hash<std::string> hasher;
+    hash_space::hash<std::string> hasher;
     unsigned h = hasher(ss.str());
     std::cout << "model hash: " << h << "\n";
   }
diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h
index e19ae894d..7c56b06a6 100755
--- a/src/interp/iz3base.h
+++ b/src/interp/iz3base.h
@@ -146,14 +146,7 @@ class iz3base : public iz3mgr, public scopes {
     ranges(){scope_computed = false;}
   };
 
-  // We only use this for sym_range_hash, which has no range destructor
-  struct symb_hash {
-    size_t operator()(const symb &s) const {
-      return (size_t) s;
-    }
-  };
-
-  stl_ext::hash_map<symb,range,symb_hash> sym_range_hash;
+  stl_ext::hash_map<symb,range> sym_range_hash;
   stl_ext::hash_map<ast,ranges> ast_ranges_hash;
   stl_ext::hash_map<ast,ast> simplify_memo;
   stl_ext::hash_map<ast,int> frame_map;                      // map assertions to frames
@@ -187,6 +180,15 @@ class iz3base : public iz3mgr, public scopes {
 
 };
 
+namespace hash_space {
+  template <>
+    class hash<iz3mgr::symb> {
+  public:
+    size_t operator()(const iz3mgr::symb &s) const {
+      return (size_t) s;
+    }
+  };
+}
 
 
 
diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp
index fe20f1372..1d81a1b15 100755
--- a/src/interp/iz3foci.cpp
+++ b/src/interp/iz3foci.cpp
@@ -58,7 +58,7 @@ public:
     }
   };
 
-  typedef hash_map<symb,foci2::symb,symb_hash> FuncDeclToSymbol; 
+  typedef hash_map<symb,foci2::symb> FuncDeclToSymbol; 
   FuncDeclToSymbol func_decl_to_symbol;     // maps Z3 func decls to symbols
 
   typedef hash_map<foci2::symb,symb> SymbolToFuncDecl; 
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index 88e4f1174..fae914292 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -619,14 +619,7 @@ public:
       return 1;
   }
 
-  // We only use this for debugging purposes
-  struct symb_hash {
-    size_t operator()(const symb &s) const {
-      return (size_t) s;
-    }
-  };
-
-  void symbols_out_of_scope_rec(hash_set<ast> &memo, hash_set<symb,symb_hash> &symb_memo, int frame, const ast &t){
+  void symbols_out_of_scope_rec(hash_set<ast> &memo, hash_set<symb> &symb_memo, int frame, const ast &t){
     if(memo.find(t) != memo.end())
       return;
     memo.insert(t);
@@ -645,7 +638,7 @@ public:
 
   void symbols_out_of_scope(int frame, const ast &t){
     hash_set<ast> memo;
-    hash_set<symb,symb_hash> symb_memo;
+    hash_set<symb> symb_memo;
     symbols_out_of_scope_rec(memo,symb_memo,frame,t);
   }