diff --git a/ChangeLog b/ChangeLog
index 3f8e4b637..87142532f 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,21 @@
+2003-08-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
+
+	Rewrite all std::map<const formula*, ...> as
+	Sgi::hash_map<const formula*, ...>.
+
+	* src/misc/hash.hh: New file.
+	* src/misc/Makefile.am (misc_HEADERS): Add it.
+	* src/ltlvisit/dotty.cc (dotty_visitor::map): Use a hash_map instead
+	of a map.
+	* src/tgba/bdddict.hh (bdd_dict::fv_map, bdd_dict::vf_map,
+	bdd_dict::ref_set, bdd_dict::var_map): Define as hash_map or
+	hash_set.
+	* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::fv_map,
+	translate_dict::vf_map): Likewise.
+	* src/tgba/tgbabddconcretefactory.hh
+	(tgba_bdd_concrete_factory::acc_map_): Likewise.
+	* src/tgba/tgbatba.hh, src/tgbaalgos/reachiter.hh: Include <map>.
+
 2003-08-25  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
 	* src/tgba/state.hh (state_ptr_less_than): Make sure left is
diff --git a/src/ltlvisit/dotty.cc b/src/ltlvisit/dotty.cc
index a47e50b81..8c050fa00 100644
--- a/src/ltlvisit/dotty.cc
+++ b/src/ltlvisit/dotty.cc
@@ -1,3 +1,4 @@
+#include "misc/hash.hh"
 #include "dotty.hh"
 #include "ltlast/visitor.hh"
 #include "ltlast/allnodes.hh"
@@ -10,7 +11,7 @@ namespace spot
     class dotty_visitor : public const_visitor
     {
     public:
-      typedef std::map<const formula*, int> map;
+      typedef Sgi::hash_map<const formula*, int, ptr_hash<formula> > map;
       dotty_visitor(std::ostream& os, map& m)
 	: os_(os), father_(-1), node_(m)
       {
diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am
index 86d96a4a7..8f39b4a9b 100644
--- a/src/misc/Makefile.am
+++ b/src/misc/Makefile.am
@@ -6,6 +6,7 @@ miscdir = $(pkgincludedir)/misc
 misc_HEADERS = \
   bddalloc.hh \
   bddlt.hh \
+  hash.hh \
   version.hh
 
 noinst_LTLIBRARIES = libmisc.la
diff --git a/src/misc/hash.hh b/src/misc/hash.hh
new file mode 100644
index 000000000..62782834e
--- /dev/null
+++ b/src/misc/hash.hh
@@ -0,0 +1,40 @@
+#ifndef SPOT_MISC_HASH_HH
+#  define SPOT_MISC_HASH_HH
+
+// See the G++ FAQ for details about this.
+
+#  ifdef __GNUC__
+#  if __GNUC__ < 3
+#    include <hash_map.h>
+#    include <hash_set.h>
+    namespace Sgi { using ::hash_map; }; // inherit globals
+#  else
+#    include <ext/hash_map>
+#    include <ext/hash_set>
+#    if __GNUC_MINOR__ == 0
+      namespace Sgi = std;               // GCC 3.0
+#    else
+      namespace Sgi = ::__gnu_cxx;       // GCC 3.1 and later
+#    endif
+#  endif
+#  else      // ...  there are other compilers, right?
+#   include <hash_map>
+#   include <hash_set>
+    namespace Sgi = std;
+#  endif
+
+namespace spot
+{
+
+  /// A hash function for pointers.
+  template <class T>
+  struct ptr_hash
+  {
+    size_t operator()(const T* f) const
+    {
+      return reinterpret_cast<const char*>(f) - static_cast<const char*>(0);
+    }
+  };
+}
+
+#endif // SPOT_MISC_HASH_HH
diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh
index b54bbfbfb..30fae1270 100644
--- a/src/tgba/bdddict.hh
+++ b/src/tgba/bdddict.hh
@@ -1,7 +1,7 @@
 #ifndef SPOT_TGBA_BDDDICT_HH
 # define SPOT_TGBA_BDDDICT_HH
 
-#include <map>
+#include "misc/hash.hh"
 #include <list>
 #include <set>
 #include <iostream>
@@ -21,9 +21,10 @@ namespace spot
     ~bdd_dict();
 
     /// Formula-to-BDD-variable maps.
-    typedef std::map<const ltl::formula*, int> fv_map;
+    typedef Sgi::hash_map<const ltl::formula*, int,
+			  ptr_hash<ltl::formula> > fv_map;
     /// BDD-variable-to-formula maps.
-    typedef std::map<int, const ltl::formula*> vf_map;
+    typedef Sgi::hash_map<int, const ltl::formula*> vf_map;
 
     fv_map now_map;		///< Maps formulae to "Now" BDD variables
     vf_map now_formula_map;	///< Maps "Now" BDD variables to formulae
@@ -111,8 +112,8 @@ namespace spot
 
   protected:
     /// BDD-variable reference counts.
-    typedef std::set<const void*> ref_set;
-    typedef std::map<int, ref_set> vr_map;
+    typedef Sgi::hash_set<const void*, ptr_hash<void> > ref_set;
+    typedef Sgi::hash_map<int, ref_set> vr_map;
     vr_map var_refs;
 
   private:
diff --git a/src/tgba/tgbabddconcretefactory.hh b/src/tgba/tgbabddconcretefactory.hh
index 45bd89ed5..3e0ffc8f9 100644
--- a/src/tgba/tgbabddconcretefactory.hh
+++ b/src/tgba/tgbabddconcretefactory.hh
@@ -1,9 +1,9 @@
 #ifndef SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH
 # define SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH
 
+#include "misc/hash.hh"
 #include "ltlast/formula.hh"
 #include "tgbabddfactory.hh"
-#include <map>
 
 namespace spot
 {
@@ -64,7 +64,8 @@ namespace spot
   private:
     tgba_bdd_core_data data_;	///< Core data for the new automata.
 
-    typedef std::map<const ltl::formula*, bdd> acc_map_;
+    typedef Sgi::hash_map<const ltl::formula*, bdd,
+			  ptr_hash<ltl::formula> > acc_map_;
     acc_map_ acc_;		///< BDD associated to each accepting condition
   };
 
diff --git a/src/tgba/tgbatba.hh b/src/tgba/tgbatba.hh
index 1d4119718..4b3e97aeb 100644
--- a/src/tgba/tgbatba.hh
+++ b/src/tgba/tgbatba.hh
@@ -1,6 +1,7 @@
 #ifndef SPOT_TGBA_TGBATBA_HH
 # define SPOT_TGBA_TGBATBA_HH
 
+#include <map>
 #include "tgba.hh"
 #include "misc/bddlt.hh"
 
diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index e0af72eca..b5d86b864 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -1,3 +1,4 @@
+#include "misc/hash.hh"
 #include "misc/bddalloc.hh"
 #include "ltlast/visitor.hh"
 #include "ltlast/allnodes.hh"
@@ -48,9 +49,10 @@ namespace spot
       }
 
       /// Formula-to-BDD-variable maps.
-      typedef std::map<const ltl::formula*, int> fv_map;
+      typedef Sgi::hash_map<const ltl::formula*, int,
+			    ptr_hash<ltl::formula> > fv_map;
       /// BDD-variable-to-formula maps.
-      typedef std::map<int, const ltl::formula*> vf_map;
+      typedef Sgi::hash_map<int, const ltl::formula*> vf_map;
 
       fv_map a_map;	       ///< Maps formulae to "a" BDD variables
       vf_map a_formula_map;    ///< Maps "a" BDD variables to formulae
diff --git a/src/tgbaalgos/reachiter.hh b/src/tgbaalgos/reachiter.hh
index d6a0a9fb3..ea84df366 100644
--- a/src/tgbaalgos/reachiter.hh
+++ b/src/tgbaalgos/reachiter.hh
@@ -1,6 +1,7 @@
 #ifndef SPOT_TGBAALGOS_REACHITER_HH
 # define SPOT_TGBAALGOS_REACHITER_HH
 
+#include <map>
 #include "tgba/tgba.hh"
 #include <stack>
 #include <deque>