removing address dependencies

src/api/api_interp.cpp

@@ -42,6 +42,20 @@ Revision History:
 using namespace stl_ext;
 #endif
 
+#ifndef WIN32
+// WARNING: don't make a hash_map with this if the range type
+// has a destructor: you'll get an address dependency!!!
+namespace stl_ext {
+  template <>
+  class hash<Z3_ast> {
+  public:
+    size_t operator()(const Z3_ast p) const {
+      return (size_t) p;
+    }
+  };
+}
+#endif
+
 typedef interpolation_options_struct *Z3_interpolation_options;
 
 extern "C" {

src/duality/duality.h

@@ -1008,6 +1008,29 @@ private:
     };
 }
 
+
+// Allow to hash on nodes and edges in deterministic way
+
+namespace stl_ext {
+  template <>
+    class hash<Duality::RPFP::Node *> {
+  public:
+    size_t operator()(const Duality::RPFP::Node *p) const {
+      return p->number;
+    }
+  };
+}
+
+namespace stl_ext {
+  template <>
+    class hash<Duality::RPFP::Edge *> {
+  public:
+    size_t operator()(const Duality::RPFP::Edge *p) const {
+      return p->number;
+    }
+  };
+}
+
 // allow to walk sets of nodes without address dependency
 
 namespace std {

src/duality/duality_wrapper.h

@@ -1419,7 +1419,8 @@ namespace std {
     class less<Duality::func_decl> {
   public:
     bool operator()(const Duality::func_decl &s, const Duality::func_decl &t) const {
-      return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id();
+      // return s.raw() < t.raw();
+      return s.raw()->get_id() < t.raw()->get_id();
     }
   };
 }

src/interp/iz3base.h

@@ -146,7 +146,14 @@ class iz3base : public iz3mgr, public scopes {
     ranges(){scope_computed = false;}
   };
 
-  stl_ext::hash_map<symb,range> sym_range_hash;
+  // 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<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

src/interp/iz3foci.cpp

@@ -51,7 +51,14 @@ public:
   typedef hash_map<foci2::ast,ast> NodeToAst;
   NodeToAst node_to_ast;                    // maps Z3 ast's to foci expressions
 
-  typedef hash_map<symb,foci2::symb> FuncDeclToSymbol; 
+  // We only use this for FuncDeclToSymbol, which has no range destructor
+  struct symb_hash {
+    size_t operator()(const symb &s) const {
+      return (size_t) s;
+    }
+  };
+
+  typedef hash_map<symb,foci2::symb,symb_hash> FuncDeclToSymbol; 
   FuncDeclToSymbol func_decl_to_symbol;     // maps Z3 func decls to symbols
 
   typedef hash_map<foci2::symb,symb> SymbolToFuncDecl; 

src/interp/iz3hash.h

@@ -141,6 +141,7 @@ namespace std {
 
 #ifndef WIN32
 
+#if 0
 namespace stl_ext {
   template <class T>
     class hash<T *> {
@@ -150,6 +151,7 @@ namespace stl_ext {
     }
   };
 }
+#endif
 
 #endif
 

src/interp/iz3mgr.h

@@ -65,7 +65,7 @@ class ast_i {
     return _ast == other._ast;
   }
   bool lt(const ast_i &other) const {
-    return _ast < other._ast;
+    return _ast->get_id() < other._ast->get_id();
   }
   friend bool operator==(const ast_i &x, const ast_i&y){
     return x.eq(y);
@@ -76,7 +76,7 @@ class ast_i {
   friend bool operator<(const ast_i &x, const ast_i&y){
     return x.lt(y);
   }
-  size_t hash() const {return (size_t)_ast;}
+  size_t hash() const {return _ast->get_id();}
   bool null() const {return !_ast;}
 };
 

src/interp/iz3pp.cpp

@@ -40,6 +40,20 @@ Revision History:
 using namespace stl_ext;
 #endif
 
+#ifndef WIN32
+// We promise not to use this for hash_map with range destructor
+namespace stl_ext {
+  template <>
+    class hash<expr *> {
+  public:
+    size_t operator()(const expr *p) const {
+      return (size_t) p;
+    }
+  };
+}
+#endif
+
+
 // TBD: algebraic data-types declarations will not be printed.
 class free_func_visitor {
   ast_manager& m;

src/interp/iz3translate.cpp

@@ -619,7 +619,14 @@ public:
       return 1;
   }
 
-  void symbols_out_of_scope_rec(hash_set<ast> &memo, hash_set<symb> &symb_memo, int frame, const ast &t){
+  // 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){
     if(memo.find(t) != memo.end())
       return;
     memo.insert(t);
@@ -638,7 +645,7 @@ public:
 
   void symbols_out_of_scope(int frame, const ast &t){
     hash_set<ast> memo;
-    hash_set<symb> symb_memo;
+    hash_set<symb,symb_hash> symb_memo;
     symbols_out_of_scope_rec(memo,symb_memo,frame,t);
   }
 

src/interp/iz3translate_direct.cpp

@@ -37,6 +37,24 @@ Revision History:
 using namespace stl_ext;
 #endif
 
+#ifndef WIN32
+
+/* This can introduce an address dependency if the range type of hash_map has
+   a destructor. Since the code in this file is not used and only here for
+   historical comparisons, we allow this non-determinism.
+ */
+namespace stl_ext {
+  template <class T>
+    class hash<T *> {
+  public:
+    size_t operator()(const T *p) const {
+      return (size_t) p;
+    }
+  };
+}
+
+#endif
+
 
 static int lemma_count = 0;
 static int nll_lemma_count = 0;