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

Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.

7 files changed, 23 insertions, 26 deletions

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 2d0b83c33..9901fb18b 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -75,8 +75,7 @@ class CnfStream {
       LiteralToNodeMap;
 
   /** Cache of what literals have been registered to a node. */
-  typedef context::CDInsertHashMap<Node, SatLiteral, NodeHashFunction>
-      NodeToLiteralMap;
+  typedef context::CDInsertHashMap<Node, SatLiteral> NodeToLiteralMap;
 
   /**
    * Constructs a CnfStream that performs equisatisfiable CNF transformations
@@ -223,7 +222,7 @@ class CnfStream {
   context::CDList<TNode> d_booleanVariables;
 
   /** Formulas that we translated that we are notifying */
-  context::CDHashSet<Node, NodeHashFunction> d_notifyFormulas;
+  context::CDHashSet<Node> d_notifyFormulas;
 
   /** Map from nodes to literals */
   NodeToLiteralMap d_nodeToLiteralMap;
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 5fdc0eb79..60a4c9704 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -330,8 +330,8 @@ void SatProofManager::processRedundantLit(
                      !negated);
 }
 
-void SatProofManager::explainLit(
-    SatLiteral lit, std::unordered_set<TNode, TNodeHashFunction>& premises)
+void SatProofManager::explainLit(SatLiteral lit,
+                                 std::unordered_set<TNode>& premises)
 {
   Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit;
   Node litNode = getClauseNode(lit);
@@ -393,7 +393,7 @@ void SatProofManager::explainLit(
     {
       continue;
     }
-    std::unordered_set<TNode, TNodeHashFunction> childPremises;
+    std::unordered_set<TNode> childPremises;
     explainLit(~currLit, childPremises);
     // save to resolution chain premises / arguments
     Assert(d_cnfStream->getNodeCache().find(currLit)
@@ -462,7 +462,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
     Trace("sat-proof-debug2")
         << push << "SatProofManager::finalizeProof: saved proofs in chain:\n";
     std::map<Node, std::shared_ptr<ProofNode>> links = d_resChains.getLinks();
-    std::unordered_set<Node, NodeHashFunction> skip;
+    std::unordered_set<Node> skip;
     for (const std::pair<const Node, std::shared_ptr<ProofNode>>& link : links)
     {
       if (skip.count(link.first))
@@ -546,12 +546,12 @@ void SatProofManager::finalizeProof(Node inConflictNode,
   // we call explainLit on each ~l_i while accumulating the children and
   // arguments for the resolution step to conclude false.
   std::vector<Node> children{inConflictNode}, args;
-  std::unordered_set<TNode, TNodeHashFunction> premises;
+  std::unordered_set<TNode> premises;
   for (unsigned i = 0, size = inConflict.size(); i < size; ++i)
   {
     Assert(d_cnfStream->getNodeCache().find(inConflict[i])
            != d_cnfStream->getNodeCache().end());
-    std::unordered_set<TNode, TNodeHashFunction> childPremises;
+    std::unordered_set<TNode> childPremises;
     explainLit(~inConflict[i], childPremises);
     Node negatedLitNode = d_cnfStream->getNodeCache()[~inConflict[i]];
     // save to resolution chain premises / arguments
@@ -659,7 +659,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
       // mark another iteration for the loop, as some resolution link may be
       // connected because of the new justifications
       expanded = true;
-      std::unordered_set<TNode, TNodeHashFunction> childPremises;
+      std::unordered_set<TNode> childPremises;
       explainLit(it->second, childPremises);
       // add the premises used in the justification. We know they will have
       // been as expanded as possible
diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h
index 8f2923981..a53f66cec 100644
--- a/src/prop/sat_proof_manager.h
+++ b/src/prop/sat_proof_manager.h
@@ -493,8 +493,7 @@ class SatProofManager
    * have been used as premises of resolution steps while explaining
    * propagations
    */
-  void explainLit(prop::SatLiteral lit,
-                  std::unordered_set<TNode, TNodeHashFunction>& premises);
+  void explainLit(prop::SatLiteral lit, std::unordered_set<TNode>& premises);
 
   /** Build refutation proof starting from conflict clause
    *
@@ -568,7 +567,7 @@ class SatProofManager
 
   /** All clauses added to the SAT solver, kept in a context-dependent manner.
    */
-  context::CDHashSet<Node, NodeHashFunction> d_assumptions;
+  context::CDHashSet<Node> d_assumptions;
 
   /**
    * A placeholder that may be used to store the literal with the final
diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp
index 873a748ae..5b51d730c 100644
--- a/src/prop/skolem_def_manager.cpp
+++ b/src/prop/skolem_def_manager.cpp
@@ -52,7 +52,7 @@ void SkolemDefManager::notifyAsserted(TNode literal,
                                       std::vector<TNode>& activatedSkolems,
                                       bool useDefs)
 {
-  std::unordered_set<Node, NodeHashFunction> skolems;
+  std::unordered_set<Node> skolems;
   getSkolems(literal, skolems);
   for (const Node& k : skolems)
   {
@@ -90,8 +90,8 @@ typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr;
 
 bool SkolemDefManager::hasSkolems(TNode n) const
 {
-  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);
@@ -145,11 +145,11 @@ bool SkolemDefManager::hasSkolems(TNode n) const
   return n.getAttribute(HasSkolemAttr());
 }
 
-void SkolemDefManager::getSkolems(
-    TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const
+void SkolemDefManager::getSkolems(TNode n,
+                                  std::unordered_set<Node>& skolems) const
 {
-  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);
diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h
index 475f40c85..d3b59f895 100644
--- a/src/prop/skolem_def_manager.h
+++ b/src/prop/skolem_def_manager.h
@@ -41,8 +41,8 @@ namespace prop {
  */
 class SkolemDefManager
 {
-  using NodeNodeMap = context::CDInsertHashMap<Node, Node, NodeHashFunction>;
-  using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+  using NodeNodeMap = context::CDInsertHashMap<Node, Node>;
+  using NodeSet = context::CDHashSet<Node>;
 
  public:
   SkolemDefManager(context::Context* context,
@@ -81,8 +81,7 @@ class SkolemDefManager
    * @param n The node to traverse
    * @param skolems The set where the skolems are added
    */
-  void getSkolems(TNode n,
-                  std::unordered_set<Node, NodeHashFunction>& skolems) const;
+  void getSkolems(TNode n, std::unordered_set<Node>& skolems) const;
   /** Does n have skolems having definitions managed by this class? */
   bool hasSkolems(TNode n) const;
 
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 090b44b90..b764695cc 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -217,7 +217,7 @@ void TheoryProxy::getSkolems(TNode node,
                              std::vector<Node>& skAsserts,
                              std::vector<Node>& sks)
 {
-  std::unordered_set<Node, NodeHashFunction> skolems;
+  std::unordered_set<Node> skolems;
   d_skdm->getSkolems(node, skolems);
   for (const Node& k : skolems)
   {
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index bc834d205..afd99ae83 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -155,7 +155,7 @@ class TheoryProxy : public Registrar
    * Set of all lemmas that have been "shared" in the portfolio---i.e.,
    * all imported and exported lemmas.
    */
-  std::unordered_set<Node, NodeHashFunction> d_shared;
+  std::unordered_set<Node> d_shared;
 
   /** The theory preprocessor */
   theory::TheoryPreprocessor d_tpp;