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

Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.

19 files changed, 39 insertions, 46 deletions

diff --git a/src/smt/abstract_values.h b/src/smt/abstract_values.h
index 1c9069ed0..32cff9378 100644
--- a/src/smt/abstract_values.h
+++ b/src/smt/abstract_values.h
@@ -34,7 +34,8 @@ namespace smt {
  */
 class AbstractValues
 {
-  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
+  typedef std::unordered_map<Node, Node> NodeToNodeHashMap;
+
  public:
   AbstractValues(NodeManager* nm);
   ~AbstractValues();
diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index 3d5429635..0bc7ce99b 100644
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -53,7 +53,7 @@ void CheckModels::checkModel(Model* m,
 
   theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get();
   Trace("check-model") << "checkModel: Check assertions..." << std::endl;
-  std::unordered_map<Node, Node, NodeHashFunction> cache;
+  std::unordered_map<Node, Node> cache;
   // the list of assertions that did not rewrite to true
   std::vector<Node> noCheckList;
   // Now go through all our user assertions checking if they're satisfied.
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index 349736d15..91287e5f9 100644
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -42,17 +42,16 @@ ExpandDefs::ExpandDefs(Env& env, SmtEngineStatistics& stats)
 
 ExpandDefs::~ExpandDefs() {}
 
-Node ExpandDefs::expandDefinitions(
-    TNode n, std::unordered_map<Node, Node, NodeHashFunction>& cache)
+Node ExpandDefs::expandDefinitions(TNode n,
+                                   std::unordered_map<Node, Node>& cache)
 {
   TrustNode trn = expandDefinitions(n, cache, nullptr);
   return trn.isNull() ? Node(n) : trn.getNode();
 }
 
-TrustNode ExpandDefs::expandDefinitions(
-    TNode n,
-    std::unordered_map<Node, Node, NodeHashFunction>& cache,
-    TConvProofGenerator* tpg)
+TrustNode ExpandDefs::expandDefinitions(TNode n,
+                                        std::unordered_map<Node, Node>& cache,
+                                        TConvProofGenerator* tpg)
 {
   const TNode orig = n;
   std::stack<std::tuple<Node, Node, bool>> worklist;
@@ -87,8 +86,7 @@ TrustNode ExpandDefs::expandDefinitions(
       }
 
       // maybe it's in the cache
-      std::unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit =
-          cache.find(n);
+      std::unordered_map<Node, Node>::iterator cacheHit = cache.find(n);
       if (cacheHit != cache.end())
       {
         TNode ret = (*cacheHit).second;
diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index d4e591c31..801622e27 100644
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -51,8 +51,7 @@ class ExpandDefs
    * @param cache Cache of previous results
    * @return The expanded term.
    */
-  Node expandDefinitions(
-      TNode n, std::unordered_map<Node, Node, NodeHashFunction>& cache);
+  Node expandDefinitions(TNode n, std::unordered_map<Node, Node>& cache);
 
   /**
    * Set proof node manager, which signals this class to enable proofs using the
@@ -65,10 +64,9 @@ class ExpandDefs
    * Helper function for above, called to specify if we want proof production
    * based on the optional argument tpg.
    */
-  theory::TrustNode expandDefinitions(
-      TNode n,
-      std::unordered_map<Node, Node, NodeHashFunction>& cache,
-      TConvProofGenerator* tpg);
+  theory::TrustNode expandDefinitions(TNode n,
+                                      std::unordered_map<Node, Node>& cache,
+                                      TConvProofGenerator* tpg);
   /** Reference to the environment. */
   Env& d_env;
   /** Reference to the SMT stats */
diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
index 04613f848..cbc388331 100644
--- a/src/smt/model_blocker.cpp
+++ b/src/smt/model_blocker.cpp
@@ -72,9 +72,9 @@ Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions,
     }
 
     Node formula = asserts.size() > 1 ? nm->mkNode(AND, asserts) : asserts[0];
-    std::unordered_map<TNode, Node, TNodeHashFunction> visited;
-    std::unordered_map<TNode, Node, TNodeHashFunction> implicant;
-    std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+    std::unordered_map<TNode, Node> visited;
+    std::unordered_map<TNode, Node> implicant;
+    std::unordered_map<TNode, Node>::iterator it;
     std::vector<TNode> visit;
     TNode cur;
     visit.push_back(formula);
@@ -235,7 +235,7 @@ Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions,
     {
       Trace("model-blocker")
           << "no specific terms to block recognized" << std::endl;
-      std::unordered_set<Node, NodeHashFunction> symbols;
+      std::unordered_set<Node> symbols;
       for (Node n : tlAsserts)
       {
         expr::getSymbols(n, symbols);
@@ -253,7 +253,7 @@ Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions,
     // otherwise, block all terms that were specified in get-value
     else
     {
-      std::unordered_set<Node, NodeHashFunction> terms;
+      std::unordered_set<Node> terms;
       for (Node n : nodesToBlock)
       {
         Node v = m->getValue(n);
diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp
index 5b6df3c1a..0395a32fd 100644
--- a/src/smt/model_core_builder.cpp
+++ b/src/smt/model_core_builder.cpp
@@ -41,7 +41,7 @@ bool ModelCoreBuilder::setModelCore(const std::vector<Node>& assertions,
   std::vector<Node> vars;
   std::vector<Node> subs;
   Trace("model-core") << "Assignments: " << std::endl;
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode> visited;
   std::vector<TNode> visit;
   TNode cur;
   visit.push_back(formula);
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index ea5d28a23..3ae03e58f 100644
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -126,7 +126,7 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
                     << ") input " << f << std::endl;
   Node curr = f;
   std::vector<Node> transChildren;
-  std::unordered_set<Node, NodeHashFunction> processed;
+  std::unordered_set<Node> processed;
   bool success;
   // we connect the proof of f to its source via the map d_src until we
   // discover that its source is a preprocessing lemma (a lemma stored in d_src)
diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index d1373a9d3..140a7c91a 100644
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -55,8 +55,7 @@ namespace smt {
  */
 class PreprocessProofGenerator : public ProofGenerator
 {
-  typedef context::CDHashMap<Node, theory::TrustNode, NodeHashFunction>
-      NodeTrustNodeMap;
+  typedef context::CDHashMap<Node, theory::TrustNode> NodeTrustNodeMap;
 
  public:
   /**
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index a222568d3..7406b922e 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -112,12 +112,12 @@ void Preprocessor::cleanup() { d_processor.cleanup(); }
 
 Node Preprocessor::expandDefinitions(const Node& n)
 {
-  std::unordered_map<Node, Node, NodeHashFunction> cache;
+  std::unordered_map<Node, Node> cache;
   return expandDefinitions(n, cache);
 }
 
-Node Preprocessor::expandDefinitions(
-    const Node& node, std::unordered_map<Node, Node, NodeHashFunction>& cache)
+Node Preprocessor::expandDefinitions(const Node& node,
+                                     std::unordered_map<Node, Node>& cache)
 {
   Trace("smt") << "SMT expandDefinitions(" << node << ")" << endl;
   // Substitute out any abstract values in node.
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 4c60a2898..3a1f9f080 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -89,8 +89,7 @@ class Preprocessor
    */
   Node expandDefinitions(const Node& n);
   /** Same as above, with a cache of previous results. */
-  Node expandDefinitions(
-      const Node& n, std::unordered_map<Node, Node, NodeHashFunction>& cache);
+  Node expandDefinitions(const Node& n, std::unordered_map<Node, Node>& cache);
   /**
    * Set proof node manager. Enables proofs in this preprocessor.
    */
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index 3cdf8a463..80219eb3c 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -57,7 +57,7 @@ class ProcessAssertions
 {
   /** The types for the recursive function definitions */
   typedef context::CDList<Node> NodeList;
-  typedef std::unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
+  typedef std::unordered_map<Node, bool> NodeToBoolHashMap;
 
  public:
   ProcessAssertions(SmtEngine& smt,
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index b36b00bd5..618cdebac 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -166,7 +166,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
   // get crowding lits and the position of the last clause that includes
   // them. The factoring step must be added after the last inclusion and before
   // its elimination.
-  std::unordered_set<TNode, TNodeHashFunction> crowding;
+  std::unordered_set<TNode> crowding;
   std::vector<std::pair<Node, size_t>> lastInclusion;
   // positions of eliminators of crowding literals, which are the positions of
   // the clauses that eliminate crowding literals *after* their last inclusion
@@ -752,7 +752,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
       // We build it rather than taking conclusionLits because the order may be
       // different
       std::vector<Node> factoredLits;
-      std::unordered_set<TNode, TNodeHashFunction> clauseSet;
+      std::unordered_set<TNode> clauseSet;
       for (size_t i = 0, size = chainConclusionLits.size(); i < size; ++i)
       {
         if (clauseSet.count(chainConclusionLits[i]))
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 780ed78ce..67273f854 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1330,7 +1330,7 @@ std::vector<Node> SmtEngine::getExpandedAssertions()
   std::vector<Node> easserts = getAssertions();
   // must expand definitions
   std::vector<Node> eassertsProc;
-  std::unordered_map<Node, Node, NodeHashFunction> cache;
+  std::unordered_map<Node, Node> cache;
   for (const Node& e : easserts)
   {
     Node eae = d_pp->expandDefinitions(e, cache);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 22316b872..924e3c974 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -37,7 +37,6 @@ template <bool ref_count> class NodeTemplate;
 typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
 class TypeNode;
-struct NodeHashFunction;
 
 class Env;
 class NodeManager;
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 317bb2646..37d752230 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -285,7 +285,7 @@ void SygusSolver::checkSynthSolution(Assertions& as)
   }
   Trace("check-synth-sol") << "Got solution map:\n";
   // the set of synthesis conjectures in our assertions
-  std::unordered_set<Node, NodeHashFunction> conjs;
+  std::unordered_set<Node> conjs;
   // For each of the above conjectures, the functions-to-synthesis and their
   // solutions. This is used as a substitution below.
   std::map<Node, std::vector<Node>> fvarMap;
@@ -317,7 +317,7 @@ void SygusSolver::checkSynthSolution(Assertions& as)
   // auxiliary assertions
   std::vector<Node> auxAssertions;
   // expand definitions cache
-  std::unordered_map<Node, Node, NodeHashFunction> cache;
+  std::unordered_map<Node, Node> cache;
   for (Node assertion : *alist)
   {
     Notice() << "SygusSolver::checkSynthSolution(): checking assertion "
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 823511b02..34ef53194 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -516,7 +516,7 @@ Node RemoveTermFormulas::runCurrent(std::pair<Node, uint32_t>& curr,
 
 Node RemoveTermFormulas::getSkolemForNode(Node k) const
 {
-  context::CDInsertHashMap<Node, Node, NodeHashFunction>::const_iterator itk =
+  context::CDInsertHashMap<Node, Node>::const_iterator itk =
       d_skolem_cache.find(k);
   if (itk != d_skolem_cache.end())
   {
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 1eeed5543..6a3a1c019 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -127,7 +127,7 @@ class RemoveTermFormulas {
   typedef context::CDInsertHashMap<
       std::pair<Node, uint32_t>,
       Node,
-      PairHashFunction<Node, uint32_t, NodeHashFunction> >
+      PairHashFunction<Node, uint32_t, std::hash<Node>>>
       TermFormulaCache;
   /** term formula removal cache
    *
@@ -155,7 +155,7 @@ class RemoveTermFormulas {
    *   d_skolem_cache[ite( G, a, b )] = k, and
    *   d_tfCache[<ite( G, a, b ),0>] = d_tfCache[<ite( G, a, b ),1>] = k.
    */
-  context::CDInsertHashMap<Node, Node, NodeHashFunction> d_skolem_cache;
+  context::CDInsertHashMap<Node, Node> d_skolem_cache;
 
   /** gets the skolem for node
    *
diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp
index c7e3d3280..8e998b9cf 100644
--- a/src/smt/witness_form.cpp
+++ b/src/smt/witness_form.cpp
@@ -66,7 +66,7 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t)
     // trivial case
     return tw;
   }
-  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+  std::unordered_set<TNode>::iterator it;
   std::vector<TNode> visit;
   TNode cur;
   TNode curw;
@@ -123,8 +123,7 @@ bool WitnessFormGenerator::requiresWitnessFormIntro(Node t) const
   return !tr.isConst() || !tr.getConst<bool>();
 }
 
-const std::unordered_set<Node, NodeHashFunction>&
-WitnessFormGenerator::getWitnessFormEqs() const
+const std::unordered_set<Node>& WitnessFormGenerator::getWitnessFormEqs() const
 {
   return d_eqs;
 }
diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h
index be1c4e534..980cbcadb 100644
--- a/src/smt/witness_form.h
+++ b/src/smt/witness_form.h
@@ -72,7 +72,7 @@ class WitnessFormGenerator : public ProofGenerator
    * where k is a skolem, containing all rewrite steps used in calls to
    * getProofFor during the entire lifetime of this generator.
    */
-  const std::unordered_set<Node, NodeHashFunction>& getWitnessFormEqs() const;
+  const std::unordered_set<Node>& getWitnessFormEqs() const;
 
  private:
   /**
@@ -88,9 +88,9 @@ class WitnessFormGenerator : public ProofGenerator
   /** The term conversion proof generator */
   TConvProofGenerator d_tcpg;
   /** The nodes we have already added rewrite steps for in d_tcpg */
-  std::unordered_set<TNode, TNodeHashFunction> d_visited;
+  std::unordered_set<TNode> d_visited;
   /** The set of equalities added as proof steps */
-  std::unordered_set<Node, NodeHashFunction> d_eqs;
+  std::unordered_set<Node> d_eqs;
   /** Lazy proof storing witness intro steps */
   LazyCDProof d_wintroPf;
   /** CDProof for justifying purification existentials */