ltl: get rid of formula_ptr_hash

* src/ltlast/formula.hh: Specialize std::hash<>.
* src/ltlvisit/contain.hh, src/ltlvisit/relabel.cc,
src/tgba/taatgba.hh, src/tgbaalgos/ltl2tgba_fm.cc: Do
not pass formula_ptr_hash to unordered_map.

src/ltlast/formula.hh

@@ -501,31 +501,6 @@ namespace spot
       }
     };
 
-    /// \ingroup ltl_essentials
-    /// \ingroup hash_funcs
-    /// \brief Hash Function for <code>const formula*</code>.
-    ///
-    /// This is meant to be used as a hash functor for
-    /// \c unordered_map whose key are of type <code>const formula*</code>.
-    ///
-    /// For instance here is how one could declare
-    /// a map of \c const::formula*.
-    /// \code
-    ///   // Remember how many times each formula has been seen.
-    ///   std::unordered_map<const spot::ltl::formula*, int,
-    ///                      const spot::ltl::formula_ptr_hash> seen;
-    /// \endcode
-    struct formula_ptr_hash:
-      public std::unary_function<const formula*, size_t>
-    {
-      size_t
-      operator()(const formula* that) const
-      {
-	assert(that);
-	return that->hash();
-      }
-    };
-
     /// Print the properties of formula \a f on stream \a out.
     SPOT_API
     std::ostream& print_formula_props(std::ostream& out,
@@ -538,4 +513,19 @@ namespace spot
   }
 }
 
+#ifndef SWIG
+namespace std
+{
+  template <>
+  struct hash<const spot::ltl::formula*>
+  {
+    size_t operator()(const spot::ltl::formula* x) const noexcept
+    {
+      assert(x);
+      return x->hash();
+    }
+  };
+}
+#endif
+
 #endif // SPOT_LTLAST_FORMULA_HH

src/ltlvisit/contain.hh

@@ -41,8 +41,7 @@ namespace spot
 	typedef std::map<const record_*, bool> incomp_map;
 	incomp_map incompatible;
       };
-      typedef std::unordered_map<const formula*,
+      typedef std::unordered_map<const formula*, record_> trans_map;
-				 record_, formula_ptr_hash> trans_map;
     public:
       /// This class uses spot::ltl_to_tgba_fm to translate LTL
       /// formulae.  See that function for the meaning of these options.

src/ltlvisit/relabel.cc

@@ -92,8 +92,7 @@ namespace spot
       class relabeler: public clone_visitor
       {
       public:
-	typedef std::unordered_map<const formula*, const formula*,
+	typedef std::unordered_map<const formula*, const formula*> map;
-				   ptr_hash<formula> > map;
 	map newname;
 	ap_generator* gen;
 	relabeling_map* oldnames;
@@ -358,8 +357,7 @@ namespace spot
 	{
 	}
       };
-      typedef std::unordered_map<const formula*, data_entry,
+      typedef std::unordered_map<const formula*, data_entry> fmap_t;
-				 const formula_ptr_hash> fmap_t;
       struct stack_entry
       {
 	const formula* grand_parent;

src/tgba/taatgba.hh

@@ -23,6 +23,7 @@
 #include <set>
 #include <iosfwd>
 #include <vector>
+#include <string>
 #include "misc/hash.hh"
 #include "ltlast/formula.hh"
 #include "bdddict.hh"
@@ -144,7 +145,7 @@ namespace spot
 
   /// A taa_tgba instance with states labeled by a given type.
   /// Still an abstract class, see below.
-  template<typename label, typename label_hash>
+  template<typename label>
   class SPOT_API taa_tgba_labelled : public taa_tgba
   {
   public:
@@ -236,8 +237,7 @@ namespace spot
   protected:
     typedef label label_t;
 
-    typedef std::unordered_map<const label, taa_tgba::state*,
+    typedef std::unordered_map<label, taa_tgba::state*> ns_map;
-			       label_hash> ns_map;
     typedef std::unordered_map<const taa_tgba::state*, label,
 			       ptr_hash<taa_tgba::state> > sn_map;
 
@@ -308,14 +308,14 @@ namespace spot
 
   class SPOT_API taa_tgba_string :
 #ifndef SWIG
-    public taa_tgba_labelled<std::string, string_hash>
+    public taa_tgba_labelled<std::string>
 #else
     public taa_tgba
 #endif
   {
   public:
     taa_tgba_string(const bdd_dict_ptr& dict) :
-      taa_tgba_labelled<std::string, string_hash>(dict) {};
+      taa_tgba_labelled<std::string>(dict) {};
     ~taa_tgba_string();
   protected:
     virtual std::string label_to_string(const std::string& label) const;
@@ -332,14 +332,14 @@ namespace spot
 
   class SPOT_API taa_tgba_formula :
 #ifndef SWIG
-    public taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash>
+    public taa_tgba_labelled<const ltl::formula*>
 #else
     public taa_tgba
 #endif
   {
   public:
     taa_tgba_formula(const bdd_dict_ptr& dict) :
-      taa_tgba_labelled<const ltl::formula*, ltl::formula_ptr_hash>(dict) {};
+      taa_tgba_labelled<const ltl::formula*>(dict) {};
     ~taa_tgba_formula();
   protected:
     virtual std::string label_to_string(const label_t& label) const;

src/tgbaalgos/ltl2tgba_fm.cc

@@ -110,8 +110,7 @@ namespace spot
 
     class ratexp_to_dfa
     {
-      typedef typename tgba_digraph::namer<const formula*,
+      typedef typename tgba_digraph::namer<const formula*>::type namer;
-					   formula_ptr_hash>::type namer;
     public:
       ratexp_to_dfa(translate_dict& dict);
       std::tuple<const_tgba_digraph_ptr, const namer*, const state*>
@@ -124,8 +123,7 @@ namespace spot
 
     private:
       translate_dict& dict_;
-      typedef std::unordered_map<const formula*, labelled_aut,
+      typedef std::unordered_map<const formula*, labelled_aut> f2a_t;
-				 formula_ptr_hash> f2a_t;
       std::vector<labelled_aut> automata_;
       f2a_t f2a_;
     };
@@ -1068,7 +1066,7 @@ namespace spot
       assert(f->is_in_nenoform());
 
       auto a = make_tgba_digraph(dict_.dict);
-      auto namer = a->create_namer<const formula*, formula_ptr_hash>();
+      auto namer = a->create_namer<const formula*>();
 
       typedef std::set<const formula*, formula_ptr_less_than> set_type;
       set_type formulae_to_translate;
@@ -1931,8 +1929,7 @@ namespace spot
       }
 
     private:
-      typedef std::unordered_map<const formula*, bool,
+      typedef std::unordered_map<const formula*, bool> pfl_map;
-				 formula_ptr_hash> pfl_map;
       pfl_map pfl_;
     };
 
@@ -2084,8 +2081,8 @@ namespace spot
       // Map each formula to its associated bdd.  This speed things up when
       // the same formula is translated several times, which especially
       // occurs when canonize() is called repeatedly inside exprop.
-      typedef std::unordered_map<const formula*, translate_dict::translated,
+      typedef std::unordered_map<const formula*,
-				 ptr_hash<formula> > formula_to_bdd_map;
+				 translate_dict::translated> formula_to_bdd_map;
       formula_to_bdd_map f2b_;
 
       possible_fair_loop_checker pflc_;
@@ -2097,8 +2094,7 @@ namespace spot
   }
 
   typedef std::map<bdd, bdd, bdd_less_than> prom_map;
-  typedef std::unordered_map<const formula*, prom_map,
+  typedef std::unordered_map<const formula*, prom_map> dest_map;
-			     formula_ptr_hash> dest_map;
 
   static void
   fill_dests(translate_dict& d, dest_map& dests, bdd label, const formula* dest)
@@ -2151,7 +2147,7 @@ namespace spot
     assert(dict == s->get_dict());
 
     tgba_digraph_ptr a = make_tgba_digraph(dict);
-    auto namer = a->create_namer<const formula*, formula_ptr_hash>();
+    auto namer = a->create_namer<const formula*>();
 
     translate_dict d(dict, a->acc(), s, exprop, f->is_syntactic_persistence());