Add std::hash overloads for Node, TNode and TypeNode. (#6534)

Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.

9 files changed, 85 insertions, 59 deletions

diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h
index cd4ba5de0..ce2f29bd5 100644
--- a/src/theory/sets/cardinality_extension.h
+++ b/src/theory/sets/cardinality_extension.h
@@ -62,7 +62,7 @@ namespace sets {
  */
 class CardinalityExtension
 {
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashSet<Node> NodeSet;
 
  public:
   /**
diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h
index bcb38ff5c..7a64b10c7 100644
--- a/src/theory/sets/inference_manager.h
+++ b/src/theory/sets/inference_manager.h
@@ -36,7 +36,7 @@ class TheorySetsPrivate;
  */
 class InferenceManager : public InferenceManagerBuffered
 {
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashSet<Node> NodeSet;
 
  public:
   InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm);
diff --git a/src/theory/sets/singleton_op.cpp b/src/theory/sets/singleton_op.cpp
index 993457fe8..06d144f72 100644
--- a/src/theory/sets/singleton_op.cpp
+++ b/src/theory/sets/singleton_op.cpp
@@ -28,7 +28,7 @@ std::ostream& operator<<(std::ostream& out, const SingletonOp& op)
 
 size_t SingletonOpHashFunction::operator()(const SingletonOp& op) const
 {
-  return TypeNodeHashFunction()(op.getType());
+  return std::hash<TypeNode>()(op.getType());
 }
 
 SingletonOp::SingletonOp(const TypeNode& elementType)
diff --git a/src/theory/sets/skolem_cache.h b/src/theory/sets/skolem_cache.h
index a41886f9d..62547a66e 100644
--- a/src/theory/sets/skolem_cache.h
+++ b/src/theory/sets/skolem_cache.h
@@ -74,7 +74,7 @@ class SkolemCache
   /** map from node pairs and identifiers to skolems */
   std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache;
   /** the set of all skolems we have generated */
-  std::unordered_set<Node, NodeHashFunction> d_allSkolems;
+  std::unordered_set<Node> d_allSkolems;
 };
 
 }  // namespace sets
diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h
index 94e06971c..63039eddd 100644
--- a/src/theory/sets/solver_state.h
+++ b/src/theory/sets/solver_state.h
@@ -43,7 +43,7 @@ class TheorySetsPrivate;
  */
 class SolverState : public TheoryState
 {
-  typedef context::CDHashMap<Node, size_t, NodeHashFunction> NodeIntMap;
+  typedef context::CDHashMap<Node, size_t> NodeIntMap;
 
  public:
   SolverState(context::Context* c,
diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h
index f98f204e0..87f25341e 100644
--- a/src/theory/sets/term_registry.h
+++ b/src/theory/sets/term_registry.h
@@ -37,7 +37,7 @@ namespace sets {
  */
 class TermRegistry
 {
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
+  typedef context::CDHashMap<Node, Node> NodeMap;
 
  public:
   TermRegistry(SolverState& state,
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 952bfd83b..3b5ee2390 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -38,8 +38,8 @@ namespace sets {
 class TheorySets;
 
 class TheorySetsPrivate {
-  typedef context::CDHashMap< Node, bool, NodeHashFunction> NodeBoolMap;
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashMap<Node, bool> NodeBoolMap;
+  typedef context::CDHashSet<Node> NodeSet;
 
  public:
   void eqNotifyNewClass(TNode t);
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 0e14a6c34..74dfc01ba 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -28,9 +28,10 @@ namespace sets {
 
 typedef std::map< Node, std::vector< Node > >::iterator                                         MEM_IT;
 typedef std::map< kind::Kind_t, std::vector< Node > >::iterator                                 KIND_TERM_IT;
-typedef std::map< Node, std::unordered_set< Node, NodeHashFunction > >::iterator                     TC_GRAPH_IT;
+typedef std::map<Node, std::unordered_set<Node> >::iterator TC_GRAPH_IT;
 typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator               TERM_IT;
-typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator   TC_IT;
+typedef std::map<Node, std::map<Node, std::unordered_set<Node> > >::iterator
+    TC_IT;
 
 TheorySetsRels::TheorySetsRels(SolverState& s,
                                InferenceManager& im,
@@ -281,7 +282,7 @@ void TheorySetsRels::check(Theory::Effort level)
     NodeManager* nm = NodeManager::currentNM();
 
     Node join_image_rel = join_image_term[0];
-    std::unordered_set< Node, NodeHashFunction > hasChecked;
+    std::unordered_set<Node> hasChecked;
     Node join_image_rel_rep = getRepresentative( join_image_rel );
     std::vector< Node >::iterator mem_rep_it = (*rel_mem_it).second.begin();
     MEM_IT rel_mem_exp_it = d_rReps_memberReps_exp_cache.find( join_image_rel_rep );
@@ -544,14 +545,14 @@ void TheorySetsRels::check(Theory::Effort level)
       if( tc_graph_it != (tc_it->second).end() ) {
         (tc_graph_it->second).insert( mem_rep_snd );
       } else {
-        std::unordered_set< Node, NodeHashFunction > sets;
+        std::unordered_set<Node> sets;
         sets.insert( mem_rep_snd );
         (tc_it->second)[mem_rep_fst] = sets;
       }
     } else {
       std::map< Node, Node > exp_map;
-      std::unordered_set< Node, NodeHashFunction > sets;
-      std::map< Node, std::unordered_set<Node, NodeHashFunction> > element_map;
+      std::unordered_set<Node> sets;
+      std::map<Node, std::unordered_set<Node> > element_map;
       sets.insert( mem_rep_snd );
       element_map[mem_rep_fst] = sets;
       d_tcr_tcGraph[tc_rel] = element_map;
@@ -609,7 +610,7 @@ void TheorySetsRels::check(Theory::Effort level)
     TC_IT tc_it = d_rRep_tcGraph.find( getRepresentative(tc_rel[0]) );
     if( tc_it != d_rRep_tcGraph.end() ) {
       bool isReachable = false;
-      std::unordered_set<Node, NodeHashFunction> seen;
+      std::unordered_set<Node> seen;
       isTCReachable( getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 0) ),
                      getRepresentative( RelsUtils::nthElementOfTuple(mem_rep, 1) ), seen, tc_it->second, isReachable );
       return isReachable;
@@ -617,8 +618,13 @@ void TheorySetsRels::check(Theory::Effort level)
     return false;
   }
 
-  void TheorySetsRels::isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen,
-                                    std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ) {
+  void TheorySetsRels::isTCReachable(
+      Node start,
+      Node dest,
+      std::unordered_set<Node>& hasSeen,
+      std::map<Node, std::unordered_set<Node> >& tc_graph,
+      bool& isReachable)
+  {
     if(hasSeen.find(start) == hasSeen.end()) {
       hasSeen.insert(start);
     }
@@ -630,7 +636,7 @@ void TheorySetsRels::check(Theory::Effort level)
         isReachable = true;
         return;
       } else {
-        std::unordered_set< Node, NodeHashFunction >::iterator set_it = pair_set_it->second.begin();
+        std::unordered_set<Node>::iterator set_it = pair_set_it->second.begin();
 
         while( set_it != pair_set_it->second.end() ) {
           // need to check if *set_it has been looked already
@@ -645,7 +651,7 @@ void TheorySetsRels::check(Theory::Effort level)
 
   void TheorySetsRels::buildTCGraphForRel( Node tc_rel ) {
     std::map< Node, Node > rel_tc_graph_exps;
-    std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph;
+    std::map<Node, std::unordered_set<Node> > rel_tc_graph;
 
     Node rel_rep = getRepresentative( tc_rel[0] );
     Node tc_rel_rep = getRepresentative( tc_rel );
@@ -656,10 +662,11 @@ void TheorySetsRels::check(Theory::Effort level)
       Node fst_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 0 ));
       Node snd_element_rep = getRepresentative( RelsUtils::nthElementOfTuple( members[i], 1 ));
       Node tuple_rep = RelsUtils::constructPair( rel_rep, fst_element_rep, snd_element_rep );
-      std::map< Node, std::unordered_set<Node, NodeHashFunction> >::iterator rel_tc_graph_it = rel_tc_graph.find( fst_element_rep );
+      std::map<Node, std::unordered_set<Node> >::iterator rel_tc_graph_it =
+          rel_tc_graph.find(fst_element_rep);
 
       if( rel_tc_graph_it == rel_tc_graph.end() ) {
-        std::unordered_set< Node, NodeHashFunction > snd_elements;
+        std::unordered_set<Node> snd_elements;
         snd_elements.insert( snd_element_rep );
         rel_tc_graph[fst_element_rep] = snd_elements;
         rel_tc_graph_exps[tuple_rep] = exps[i];
@@ -676,19 +683,23 @@ void TheorySetsRels::check(Theory::Effort level)
     }
   }
 
-  void TheorySetsRels::doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ) {
+  void TheorySetsRels::doTCInference(
+      std::map<Node, std::unordered_set<Node> > rel_tc_graph,
+      std::map<Node, Node> rel_tc_graph_exps,
+      Node tc_rel)
+  {
     Trace("rels-debug") << "[Theory::Rels] ****** doTCInference !" << std::endl;
     for (TC_GRAPH_IT tc_graph_it = rel_tc_graph.begin();
          tc_graph_it != rel_tc_graph.end();
          ++tc_graph_it)
     {
-      for (std::unordered_set<Node, NodeHashFunction>::iterator
-               snd_elements_it = tc_graph_it->second.begin();
+      for (std::unordered_set<Node>::iterator snd_elements_it =
+               tc_graph_it->second.begin();
            snd_elements_it != tc_graph_it->second.end();
            ++snd_elements_it)
       {
         std::vector< Node > reasons;
-        std::unordered_set<Node, NodeHashFunction> seen;
+        std::unordered_set<Node> seen;
         Node tuple = RelsUtils::constructPair( tc_rel, getRepresentative( tc_graph_it->first ), getRepresentative( *snd_elements_it) );
         Assert(rel_tc_graph_exps.find(tuple) != rel_tc_graph_exps.end());
         Node exp   = rel_tc_graph_exps.find( tuple )->second;
@@ -701,8 +712,15 @@ void TheorySetsRels::check(Theory::Effort level)
     Trace("rels-debug") << "[Theory::Rels] ****** Done with doTCInference !" << std::endl;
   }
 
-  void TheorySetsRels::doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph,
-                                       std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ) {
+  void TheorySetsRels::doTCInference(
+      Node tc_rel,
+      std::vector<Node> reasons,
+      std::map<Node, std::unordered_set<Node> >& tc_graph,
+      std::map<Node, Node>& rel_tc_graph_exps,
+      Node start_node_rep,
+      Node cur_node_rep,
+      std::unordered_set<Node>& seen)
+  {
     NodeManager* nm = NodeManager::currentNM();
     Node tc_mem = RelsUtils::constructPair( tc_rel, RelsUtils::nthElementOfTuple((reasons.front())[0], 0), RelsUtils::nthElementOfTuple((reasons.back())[0], 1) );
     std::vector< Node > all_reasons( reasons );
@@ -737,8 +755,7 @@ void TheorySetsRels::check(Theory::Effort level)
     seen.insert( cur_node_rep );
     TC_GRAPH_IT  cur_set = tc_graph.find( cur_node_rep );
     if( cur_set != tc_graph.end() ) {
-      for (std::unordered_set<Node, NodeHashFunction>::iterator set_it =
-               cur_set->second.begin();
+      for (std::unordered_set<Node>::iterator set_it = cur_set->second.begin();
            set_it != cur_set->second.end();
            ++set_it)
       {
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 2ca8696b0..c30322d07 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -61,27 +61,27 @@ public:
  */
 class TheorySetsRels {
   typedef context::CDList<Node> NodeList;
-  typedef context::CDHashSet< Node, NodeHashFunction >            NodeSet;
-  typedef context::CDHashMap< Node, Node, NodeHashFunction >      NodeMap;
+  typedef context::CDHashSet<Node> NodeSet;
+  typedef context::CDHashMap<Node, Node> NodeMap;
 
-public:
- TheorySetsRels(SolverState& s,
-                InferenceManager& im,
-                SkolemCache& skc,
-                TermRegistry& treg);
-
- ~TheorySetsRels();
- /**
-  * Invoke the check method with effort level e. At a high level, this class
-  * will make calls to TheorySetsPrivate::processInference to assert facts,
-  * lemmas, and conflicts. If this class makes no such call, then the current
-  * set of assertions is satisfiable with respect to relations.
-  */
- void check(Theory::Effort e);
- /** Is kind k a kind that belongs to the relation theory? */
- static bool isRelationKind(Kind k);
-
-private:
+ public:
+  TheorySetsRels(SolverState& s,
+                 InferenceManager& im,
+                 SkolemCache& skc,
+                 TermRegistry& treg);
+
+  ~TheorySetsRels();
+  /**
+   * Invoke the check method with effort level e. At a high level, this class
+   * will make calls to TheorySetsPrivate::processInference to assert facts,
+   * lemmas, and conflicts. If this class makes no such call, then the current
+   * set of assertions is satisfiable with respect to relations.
+   */
+  void check(Theory::Effort e);
+  /** Is kind k a kind that belongs to the relation theory? */
+  static bool isRelationKind(Kind k);
+
+ private:
   /** True and false constant nodes */
   Node                          d_trueNode;
   Node                          d_falseNode;
@@ -98,13 +98,12 @@ private:
   std::vector<Node> d_pending;
   NodeSet                       d_shared_terms;
 
-
-  std::unordered_set< Node, NodeHashFunction >       d_rel_nodes;
+  std::unordered_set<Node> d_rel_nodes;
   std::map< Node, std::vector<Node> >           d_tuple_reps;
   std::map< Node, TupleTrie >                   d_membership_trie;
 
   /** Symbolic tuple variables that has been reduced to concrete ones */
-  std::unordered_set< Node, NodeHashFunction >       d_symbolic_tuples;
+  std::unordered_set<Node> d_symbolic_tuples;
 
   /** Mapping between relation and its member representatives */
   std::map< Node, std::vector< Node > >           d_rReps_memberReps_cache;
@@ -116,8 +115,8 @@ private:
   std::map< Node, std::map<kind::Kind_t, std::vector<Node> > >                  d_terms_cache;
 
   /** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/
-  std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > >     d_rRep_tcGraph;
-  std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > >     d_tcr_tcGraph;
+  std::map<Node, std::map<Node, std::unordered_set<Node> > > d_rRep_tcGraph;
+  std::map<Node, std::map<Node, std::unordered_set<Node> > > d_tcr_tcGraph;
   std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps;
 
  private:
@@ -154,9 +153,16 @@ private:
   void applyTCRule( Node mem, Node rel, Node rel_rep, Node exp);
   void buildTCGraphForRel( Node tc_rel );
   void doTCInference();
-  void doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel );
-  void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph,
-                       std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen );
+  void doTCInference(std::map<Node, std::unordered_set<Node> > rel_tc_graph,
+                     std::map<Node, Node> rel_tc_graph_exps,
+                     Node tc_rel);
+  void doTCInference(Node tc_rel,
+                     std::vector<Node> reasons,
+                     std::map<Node, std::unordered_set<Node> >& tc_graph,
+                     std::map<Node, Node>& rel_tc_graph_exps,
+                     Node start_node_rep,
+                     Node cur_node_rep,
+                     std::unordered_set<Node>& seen);
 
   void composeMembersForRels( Node );
   void computeMembersForBinOpRel( Node );
@@ -165,8 +171,11 @@ private:
   void computeMembersForJoinImageTerm( Node );
 
   bool isTCReachable( Node mem_rep, Node tc_rel );
-  void isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen,
-                    std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable );
+  void isTCReachable(Node start,
+                     Node dest,
+                     std::unordered_set<Node>& hasSeen,
+                     std::map<Node, std::unordered_set<Node> >& tc_graph,
+                     bool& isReachable);
 
   /** Helper functions */
   bool hasTerm( Node a );