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

Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.

3 files changed, 11 insertions, 16 deletions

diff --git a/src/decision/assertion_list.cpp b/src/decision/assertion_list.cpp
index 098378d22..28c285a8f 100644
--- a/src/decision/assertion_list.cpp
+++ b/src/decision/assertion_list.cpp
@@ -101,8 +101,7 @@ void AssertionList::notifyStatus(TNode n, DecisionStatus s)
     // no decision does not impact the decision order
     return;
   }
-  std::unordered_set<TNode, TNodeHashFunction>::iterator it =
-      d_dlistSet.find(n);
+  std::unordered_set<TNode>::iterator it = d_dlistSet.find(n);
   if (s == DecisionStatus::DECISION)
   {
     if (it == d_dlistSet.end())
diff --git a/src/decision/assertion_list.h b/src/decision/assertion_list.h
index fdb4bb2d5..3e7a1fee8 100644
--- a/src/decision/assertion_list.h
+++ b/src/decision/assertion_list.h
@@ -97,7 +97,7 @@ class AssertionList
   /** The list of assertions */
   std::vector<TNode> d_dlist;
   /** The set of assertions for fast membership testing in the above vector */
-  std::unordered_set<TNode, TNodeHashFunction> d_dlistSet;
+  std::unordered_set<TNode> d_dlistSet;
   /** The index of the next assertion to satify */
   context::CDO<size_t> d_dindex;
 };
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 870d0674c..8c713ab06 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -45,21 +45,17 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW};
 
   typedef std::vector<std::pair<Node, Node> > SkolemList;
-  typedef context::CDHashMap<Node, SkolemList, NodeHashFunction> SkolemCache;
+  typedef context::CDHashMap<Node, SkolemList> SkolemCache;
   typedef std::vector<Node> ChildList;
-  typedef context::
-      CDHashMap<Node, std::pair<ChildList, ChildList>, NodeHashFunction>
-          ChildCache;
-  typedef context::CDHashMap<Node,Node,NodeHashFunction> SkolemMap;
-  typedef context::CDHashMap<Node,
-                             std::pair<DecisionWeight, DecisionWeight>,
-                             NodeHashFunction>
+  typedef context::CDHashMap<Node, std::pair<ChildList, ChildList>> ChildCache;
+  typedef context::CDHashMap<Node, Node> SkolemMap;
+  typedef context::CDHashMap<Node, std::pair<DecisionWeight, DecisionWeight>>
       WeightCache;
 
   // being 'justified' is monotonic with respect to decisions
-  typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet;
+  typedef context::CDHashSet<Node> JustifiedSet;
   JustifiedSet d_justified;
-  typedef context::CDHashMap<Node,DecisionWeight,NodeHashFunction> ExploredThreshold;
+  typedef context::CDHashMap<Node, DecisionWeight> ExploredThreshold;
   ExploredThreshold d_exploredThreshold;
   context::CDO<unsigned>  d_prvsIndex;
   context::CDO<unsigned>  d_threshPrvsIndex;
@@ -86,13 +82,13 @@ class JustificationHeuristic : public ITEDecisionStrategy {
    * splitter. Can happen when exploring assertion corresponding to a
    * term-ITE.
    */
-  std::unordered_set<Node,NodeHashFunction> d_visited;
+  std::unordered_set<Node> d_visited;
 
   /**
    * Set to track visited nodes in a dfs search done in computeSkolems
    * function
    */
-  std::unordered_set<Node, NodeHashFunction> d_visitedComputeSkolems;
+  std::unordered_set<Node> d_visitedComputeSkolems;
 
   /** current decision for the recursive call */
   prop::SatLiteral d_curDecision;
@@ -172,7 +168,7 @@ private:
   * For big and/or nodes, a cache to save starting index into children
   * for efficiently.
   */
- typedef context::CDHashMap<Node, int, NodeHashFunction> StartIndexCache;
+ typedef context::CDHashMap<Node, int> StartIndexCache;
  StartIndexCache d_startIndexCache;
  int getStartIndex(TNode node);
  void saveStartIndex(TNode node, int val);