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

Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.

19 files changed, 45 insertions, 50 deletions

diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp
index 9c9adf99e..4c3b2f17e 100644
--- a/src/theory/strings/arith_entail.cpp
+++ b/src/theory/strings/arith_entail.cpp
@@ -131,7 +131,7 @@ bool ArithEntail::checkApprox(Node ar)
       // c.isNull() means c = 1
       bool isOverApprox = !c.isNull() && c.getConst<Rational>().sgn() == -1;
       std::vector<Node>& approx = mApprox[v];
-      std::unordered_set<Node, NodeHashFunction> visited;
+      std::unordered_set<Node> visited;
       std::vector<Node> toProcess;
       toProcess.push_back(v);
       do
@@ -561,7 +561,7 @@ bool ArithEntail::checkWithEqAssumption(Node assumption, Node a, bool strict)
                           << ", strict=" << strict << std::endl;
 
   // Find candidates variables to compute substitutions for
-  std::unordered_set<Node, NodeHashFunction> candVars;
+  std::unordered_set<Node> candVars;
   std::vector<Node> toVisit = {assumption};
   while (!toVisit.empty())
   {
diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h
index 41cb3e608..6c423e3b8 100644
--- a/src/theory/strings/base_solver.h
+++ b/src/theory/strings/base_solver.h
@@ -39,7 +39,7 @@ namespace strings {
  */
 class BaseSolver
 {
-  using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+  using NodeSet = context::CDHashSet<Node>;
 
  public:
   BaseSolver(SolverState& s, InferenceManager& im);
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index ed220c1eb..a6e4ce698 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1078,7 +1078,7 @@ void CoreSolver::processNEqc(Node eqc,
   // the possible inferences
   std::vector<CoreInferInfo> pinfer;
   // compute normal forms that are effectively unique
-  std::unordered_map<Node, size_t, NodeHashFunction> nfCache;
+  std::unordered_map<Node, size_t> nfCache;
   std::vector<size_t> nfIndices;
   bool hasConstIndex = false;
   for (size_t i = 0, nnforms = normal_forms.size(); i < nnforms; i++)
diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h
index 143155f55..4e8a0a96b 100644
--- a/src/theory/strings/core_solver.h
+++ b/src/theory/strings/core_solver.h
@@ -79,7 +79,7 @@ class CoreInferInfo
 class CoreSolver
 {
   friend class InferenceManager;
-  using NodeIntMap = context::CDHashMap<Node, int, NodeHashFunction>;
+  using NodeIntMap = context::CDHashMap<Node, int>;
 
  public:
   CoreSolver(SolverState& s,
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index e00668997..a1de5e295 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -251,7 +251,7 @@ void ExtfSolver::checkExtfEval(int effort)
   bool has_nreduce = false;
   std::vector<Node> terms = d_extt.getActive();
   // the set of terms we have done extf inferences for
-  std::unordered_set<Node, NodeHashFunction> inferProcessed;
+  std::unordered_set<Node> inferProcessed;
   for (const Node& n : terms)
   {
     // Setup information about n, including if it is equal to a constant.
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h
index bfcf244d7..82b4f61ee 100644
--- a/src/theory/strings/extf_solver.h
+++ b/src/theory/strings/extf_solver.h
@@ -81,7 +81,7 @@ class ExtfInfoTmp
  */
 class ExtfSolver
 {
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashSet<Node> NodeSet;
 
  public:
   ExtfSolver(SolverState& s,
diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h
index 6b2c4dfc4..af905cbad 100644
--- a/src/theory/strings/infer_proof_cons.h
+++ b/src/theory/strings/infer_proof_cons.h
@@ -45,8 +45,7 @@ namespace strings {
  */
 class InferProofCons : public ProofGenerator
 {
-  typedef context::CDHashMap<Node, std::shared_ptr<InferInfo>, NodeHashFunction>
-      NodeInferInfoMap;
+  typedef context::CDHashMap<Node, std::shared_ptr<InferInfo>> NodeInferInfoMap;
 
  public:
   InferProofCons(context::Context* c,
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index b18c64319..cf9c64bb1 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -72,8 +72,8 @@ namespace strings {
  */
 class InferenceManager : public InferenceManagerBuffered
 {
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+  typedef context::CDHashSet<Node> NodeSet;
+  typedef context::CDHashMap<Node, Node> NodeNodeMap;
   friend class InferInfo;
 
  public:
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index ace2756c1..bf4c20f85 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -63,7 +63,7 @@ bool RegExpOpr::checkConstRegExp( Node r ) {
 RegExpConstType RegExpOpr::getRegExpConstType(Node r)
 {
   Assert(r.getType().isRegExp());
-  std::unordered_map<Node, RegExpConstType, NodeHashFunction>::iterator it;
+  std::unordered_map<Node, RegExpConstType>::iterator it;
   std::vector<TNode> visit;
   TNode cur;
   visit.push_back(r);
@@ -1345,8 +1345,8 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
 Node RegExpOpr::removeIntersection(Node r) {
   Assert(checkConstRegExp(r));
   NodeManager* nm = NodeManager::currentNM();
-  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
-  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::unordered_map<TNode, Node> visited;
+  std::unordered_map<TNode, Node>::iterator it;
   std::vector<TNode> visit;
   TNode cur;
   visit.push_back(r);
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index d0ed07308..a20e9a0a9 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -78,7 +78,7 @@ class RegExpOpr {
   std::map<PairNodeStr, Node> d_dv_cache;
   std::map<PairNodeStr, std::pair<Node, int> > d_deriv_cache;
   /** cache mapping regular expressions to whether they contain constants */
-  std::unordered_map<Node, RegExpConstType, NodeHashFunction> d_constCache;
+  std::unordered_map<Node, RegExpConstType> d_constCache;
   std::map<Node, std::pair<std::set<unsigned>, std::set<Node> > > d_fset_cache;
   std::map<PairNodes, Node> d_inter_cache;
   std::map<Node, std::vector<PairNodes> > d_split_cache;
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 38fc6fc8f..167ce9570 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -137,7 +137,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
     NodeManager* nm = NodeManager::currentNM();
     // representatives of strings that are the LHS of positive memberships that
     // we unfolded
-    std::unordered_set<Node, NodeHashFunction> repUnfold;
+    std::unordered_set<Node> repUnfold;
     // check positive (e=0), then negative (e=1) memberships
     for (unsigned e = 0; e < 2; e++)
     {
@@ -329,7 +329,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
 
 bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems)
 {
-  std::unordered_set<Node, NodeHashFunction> remove;
+  std::unordered_set<Node> remove;
 
   for (const Node& m1 : mems)
   {
diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h
index bf148a071..98e2449c5 100644
--- a/src/theory/strings/regexp_solver.h
+++ b/src/theory/strings/regexp_solver.h
@@ -38,11 +38,11 @@ namespace strings {
 class RegExpSolver
 {
   typedef context::CDList<Node> NodeList;
-  typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
-  typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
-  typedef context::CDHashMap<Node, unsigned, NodeHashFunction> NodeUIntMap;
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashMap<Node, bool> NodeBoolMap;
+  typedef context::CDHashMap<Node, int> NodeIntMap;
+  typedef context::CDHashMap<Node, unsigned> NodeUIntMap;
+  typedef context::CDHashMap<Node, Node> NodeNodeMap;
+  typedef context::CDHashSet<Node> NodeSet;
 
  public:
   RegExpSolver(SolverState& s,
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index b3ffa784f..126ee313d 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -207,7 +207,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 strings
diff --git a/src/theory/strings/strings_fmf.h b/src/theory/strings/strings_fmf.h
index ba9f0f4e1..39ba6168a 100644
--- a/src/theory/strings/strings_fmf.h
+++ b/src/theory/strings/strings_fmf.h
@@ -37,7 +37,7 @@ namespace strings {
  */
 class StringsFmf
 {
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashSet<Node> NodeSet;
 
  public:
   StringsFmf(context::Context* c,
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 4460e1ff3..d7a0a0554 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -437,8 +437,7 @@ const context::CDList<TNode>& TermRegistry::getFunctionTerms() const
   return d_functionsTerms;
 }
 
-const context::CDHashSet<Node, NodeHashFunction>& TermRegistry::getInputVars()
-    const
+const context::CDHashSet<Node>& TermRegistry::getInputVars() const
 {
   return d_inputVars;
 }
diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h
index f0543c282..7c399759b 100644
--- a/src/theory/strings/term_registry.h
+++ b/src/theory/strings/term_registry.h
@@ -46,9 +46,9 @@ class InferenceManager;
  */
 class TermRegistry
 {
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-  typedef context::CDHashSet<TypeNode, TypeNodeHashFunction> TypeNodeSet;
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+  typedef context::CDHashSet<Node> NodeSet;
+  typedef context::CDHashSet<TypeNode, std::hash<TypeNode>> TypeNodeSet;
+  typedef context::CDHashMap<Node, Node> NodeNodeMap;
 
  public:
   TermRegistry(SolverState& s,
@@ -147,7 +147,7 @@ class TermRegistry
    * Get the "input variables", corresponding to the set of leaf nodes of
    * string-like type that have been preregistered as terms to this object.
    */
-  const context::CDHashSet<Node, NodeHashFunction>& getInputVars() const;
+  const context::CDHashSet<Node>& getInputVars() const;
   /** Returns true if any str.code terms have been preregistered */
   bool hasStringCode() const;
   //---------------------------- end queries
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 02c0c3130..06a39ec64 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -210,7 +210,7 @@ bool TheoryStrings::collectModelValues(TheoryModel* m,
     Trace("strings-debug-model") << d_esolver.debugPrintModel() << std::endl;
   }
   Trace("strings-model") << "TheoryStrings::collectModelValues" << std::endl;
-  std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > repSet;
+  std::map<TypeNode, std::unordered_set<Node> > repSet;
   // Generate model
   // get the relevant string equivalence classes
   for (const Node& s : termSet)
@@ -222,9 +222,7 @@ bool TheoryStrings::collectModelValues(TheoryModel* m,
       repSet[tn].insert(r);
     }
   }
-  for (const std::pair<const TypeNode,
-                       std::unordered_set<Node, NodeHashFunction> >& rst :
-       repSet)
+  for (const std::pair<const TypeNode, std::unordered_set<Node> >& rst : repSet)
   {
     // get partition of strings of equal lengths, per type
     std::map<TypeNode, std::vector<std::vector<Node> > > colT;
@@ -241,12 +239,11 @@ bool TheoryStrings::collectModelValues(TheoryModel* m,
   return true;
 }
 
-bool TheoryStrings::collectModelInfoType(
-    TypeNode tn,
-    const std::unordered_set<Node, NodeHashFunction>& repSet,
-    std::vector<std::vector<Node> >& col,
-    std::vector<Node>& lts,
-    TheoryModel* m)
+bool TheoryStrings::collectModelInfoType(TypeNode tn,
+                                         const std::unordered_set<Node>& repSet,
+                                         std::vector<std::vector<Node> >& col,
+                                         std::vector<Node>& lts,
+                                         TheoryModel* m)
 {
   NodeManager* nm = NodeManager::currentNM();
   std::map< Node, Node > processed;
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 01111880d..a671129d4 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -60,8 +60,9 @@ namespace strings {
  */
 class TheoryStrings : public Theory {
   friend class InferenceManager;
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-  typedef context::CDHashSet<TypeNode, TypeNodeHashFunction> TypeNodeSet;
+  typedef context::CDHashSet<Node> NodeSet;
+  typedef context::CDHashSet<TypeNode, std::hash<TypeNode>> TypeNodeSet;
+
  public:
   TheoryStrings(context::Context* c,
                 context::UserContext* u,
@@ -195,12 +196,11 @@ class TheoryStrings : public Theory {
    *
    * Returns false if a conflict is discovered while doing this assignment.
    */
-  bool collectModelInfoType(
-      TypeNode tn,
-      const std::unordered_set<Node, NodeHashFunction>& repSet,
-      std::vector<std::vector<Node> >& col,
-      std::vector<Node>& lts,
-      TheoryModel* m);
+  bool collectModelInfoType(TypeNode tn,
+                            const std::unordered_set<Node>& repSet,
+                            std::vector<std::vector<Node>>& col,
+                            std::vector<Node>& lts,
+                            TheoryModel* m);
 
   /** assert pending fact
    *
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index c3c444fc7..5a4a25e88 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -70,8 +70,8 @@ void flattenOp(Kind k, Node n, std::vector<Node>& conj)
     return;
   }
   // otherwise, traverse
-  std::unordered_set<TNode, TNodeHashFunction> visited;
-  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+  std::unordered_set<TNode> visited;
+  std::unordered_set<TNode>::iterator it;
   std::vector<TNode> visit;
   TNode cur;
   visit.push_back(n);