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

Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.

27 files changed, 271 insertions, 254 deletions

diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index 848d86edd..d97fe1320 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -109,8 +109,8 @@ std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) {
 }
 
 size_t ArrayStoreAllHashFunction::operator()(const ArrayStoreAll& asa) const {
-  return TypeNodeHashFunction()(asa.getType())
-         * NodeHashFunction()(asa.getValue());
+  return std::hash<TypeNode>()(asa.getType())
+         * std::hash<Node>()(asa.getValue());
 }
 
 }  // namespace cvc5
diff --git a/src/expr/ascription_type.cpp b/src/expr/ascription_type.cpp
index e0f1c3ec8..65a686036 100644
--- a/src/expr/ascription_type.cpp
+++ b/src/expr/ascription_type.cpp
@@ -47,7 +47,7 @@ bool AscriptionType::operator!=(const AscriptionType& other) const
 
 size_t AscriptionTypeHashFunction::operator()(const AscriptionType& at) const
 {
-  return TypeNodeHashFunction()(at.getType());
+  return std::hash<TypeNode>()(at.getType());
 }
 
 std::ostream& operator<<(std::ostream& out, AscriptionType at)
diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h
index 3330decff..b619a36e2 100644
--- a/src/expr/bound_var_manager.h
+++ b/src/expr/bound_var_manager.h
@@ -98,7 +98,7 @@ class BoundVarManager
   /** Whether we keep cache values */
   bool d_keepCacheVals;
   /** The set of cache values we have used */
-  std::unordered_set<Node, NodeHashFunction> d_cacheVals;
+  std::unordered_set<Node> d_cacheVals;
 };
 
 }  // namespace cvc5
diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
index 4ac0b9add..2e1ef6c53 100644
--- a/src/expr/buffered_proof_generator.h
+++ b/src/expr/buffered_proof_generator.h
@@ -33,8 +33,7 @@ class ProofStep;
  */
 class BufferedProofGenerator : public ProofGenerator
 {
-  typedef context::CDHashMap<Node, std::shared_ptr<ProofStep>, NodeHashFunction>
-      NodeProofStepMap;
+  typedef context::CDHashMap<Node, std::shared_ptr<ProofStep>> NodeProofStepMap;
 
  public:
   BufferedProofGenerator(context::Context* c, ProofNodeManager* pnm);
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index c1893d3f4..9e09c06e6 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -192,7 +192,7 @@ bool DType::resolve(const std::map<std::string, TypeNode>& resolutions,
   {
     // all datatype constructors should be sygus and have sygus operators whose
     // free variables are subsets of sygus bound var list.
-    std::unordered_set<Node, NodeHashFunction> svs;
+    std::unordered_set<Node> svs;
     for (const Node& sv : d_sygusBvl)
     {
       svs.insert(sv);
@@ -202,7 +202,7 @@ bool DType::resolve(const std::map<std::string, TypeNode>& resolutions,
       Node sop = d_constructors[i]->getSygusOp();
       Assert(!sop.isNull())
           << "Sygus datatype contains a non-sygus constructor";
-      std::unordered_set<Node, NodeHashFunction> fvs;
+      std::unordered_set<Node> fvs;
       expr::getFreeVariables(sop, fvs);
       for (const Node& v : fvs)
       {
@@ -625,10 +625,9 @@ Node DType::mkGroundTermInternal(TypeNode t, bool isValue) const
   return groundTerm;
 }
 
-void DType::getAlienSubfieldTypes(
-    std::unordered_set<TypeNode, TypeNodeHashFunction>& types,
-    std::map<TypeNode, bool>& processed,
-    bool isAlienPos) const
+void DType::getAlienSubfieldTypes(std::unordered_set<TypeNode>& types,
+                                  std::map<TypeNode, bool>& processed,
+                                  bool isAlienPos) const
 {
   std::map<TypeNode, bool>::iterator it = processed.find(d_self);
   if (it != processed.end())
@@ -708,7 +707,7 @@ bool DType::hasNestedRecursion() const
   Trace("datatypes-init") << "Compute simply recursive for " << getName()
                           << std::endl;
   // get the alien subfield types of this datatype
-  std::unordered_set<TypeNode, TypeNodeHashFunction> types;
+  std::unordered_set<TypeNode> types;
   std::map<TypeNode, bool> processed;
   getAlienSubfieldTypes(types, processed, false);
   if (Trace.isOn("datatypes-init"))
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index 6fd334e02..584dc1615 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -542,10 +542,9 @@ class DType
    * @param isAlienPos Whether we are in an alien subfield type position. This
    * flag is true if we have traversed beneath a non-datatype type constructor.
    */
-  void getAlienSubfieldTypes(
-      std::unordered_set<TypeNode, TypeNodeHashFunction>& types,
-      std::map<TypeNode, bool>& processed,
-      bool isAlienPos) const;
+  void getAlienSubfieldTypes(std::unordered_set<TypeNode>& types,
+                             std::map<TypeNode, bool>& processed,
+                             bool isAlienPos) const;
   /** name of this datatype */
   std::string d_name;
   /** the type parameters of this datatype (if this is a parametric datatype)
diff --git a/src/expr/emptybag.cpp b/src/expr/emptybag.cpp
index d85aca30c..b8cb70e16 100644
--- a/src/expr/emptybag.cpp
+++ b/src/expr/emptybag.cpp
@@ -28,7 +28,7 @@ std::ostream& operator<<(std::ostream& out, const EmptyBag& asa)
 
 size_t EmptyBagHashFunction::operator()(const EmptyBag& es) const
 {
-  return TypeNodeHashFunction()(es.getType());
+  return std::hash<TypeNode>()(es.getType());
 }
 
 /**
diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp
index d0d1d4e78..0bd7ee213 100644
--- a/src/expr/emptyset.cpp
+++ b/src/expr/emptyset.cpp
@@ -29,7 +29,7 @@ std::ostream& operator<<(std::ostream& out, const EmptySet& asa) {
 }
 
 size_t EmptySetHashFunction::operator()(const EmptySet& es) const {
-  return TypeNodeHashFunction()(es.getType());
+  return std::hash<TypeNode>()(es.getType());
 }
 
 /**
diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
index 6bec9ffb9..efcda94bd 100644
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -92,8 +92,7 @@ class LazyCDProof : public CDProof
   bool hasGenerator(Node fact) const;
 
  protected:
-  typedef context::CDHashMap<Node, ProofGenerator*, NodeHashFunction>
-      NodeProofGeneratorMap;
+  typedef context::CDHashMap<Node, ProofGenerator*> NodeProofGeneratorMap;
   /** Maps facts that can be proven to generators */
   NodeProofGeneratorMap d_gens;
   /** The default proof generator */
diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index f5cf56983..3ce2212be 100644
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -60,18 +60,15 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
       << "LazyCDProofChain::getProofFor " << fact << "\n";
   // which facts have had proofs retrieved for. This is maintained to avoid
   // cycles. It also saves the proof node of the fact
-  std::unordered_map<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
-      toConnect;
+  std::unordered_map<Node, std::shared_ptr<ProofNode>> toConnect;
   // leaves of proof node links in the chain, i.e. assumptions, yet to be
   // expanded
-  std::unordered_map<Node,
-                     std::vector<std::shared_ptr<ProofNode>>,
-                     NodeHashFunction>
+  std::unordered_map<Node, std::vector<std::shared_ptr<ProofNode>>>
       assumptionsToExpand;
   // invariant of the loop below, the first iteration notwithstanding:
   //   visit = domain(assumptionsToExpand) \ domain(toConnect)
   std::vector<Node> visit{fact};
-  std::unordered_map<Node, bool, NodeHashFunction> visited;
+  std::unordered_map<Node, bool> visited;
   Node cur;
   do
   {
diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
index fa965f8bb..1abb3f84e 100644
--- a/src/expr/lazy_proof_chain.h
+++ b/src/expr/lazy_proof_chain.h
@@ -144,7 +144,7 @@ class LazyCDProofChain : public ProofGenerator
   /** A dummy context used by this class if none is provided */
   context::Context d_context;
   /** Maps facts that can be proven to generators */
-  context::CDHashMap<Node, ProofGenerator*, NodeHashFunction> d_gens;
+  context::CDHashMap<Node, ProofGenerator*> d_gens;
   /** The default proof generator (if one exists) */
   ProofGenerator* d_defGen;
 };
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index e4acfb476..00a530227 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -110,3 +110,17 @@ template bool NodeTemplate<true>::isConst() const;
 template bool NodeTemplate<false>::isConst() const;
 
 }  // namespace cvc5
+
+namespace std {
+
+size_t hash<cvc5::Node>::operator()(const cvc5::Node& node) const
+{
+  return node.getId();
+}
+
+size_t hash<cvc5::TNode>::operator()(const cvc5::TNode& node) const
+{
+  return node.getId();
+}
+
+}  // namespace std
diff --git a/src/expr/node.h b/src/expr/node.h
index 5480b38ae..9258a3264 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -130,6 +130,25 @@ typedef NodeTemplate<true> Node;
  */
 typedef NodeTemplate<false> TNode;
 
+}  // namespace cvc5
+
+namespace std {
+
+template <>
+struct hash<cvc5::Node>
+{
+  size_t operator()(const cvc5::Node& node) const;
+};
+
+template <>
+struct hash<cvc5::TNode>
+{
+  size_t operator()(const cvc5::TNode& node) const;
+};
+
+}  // namespace std
+
+namespace cvc5 {
 namespace expr {
 
 class NodeValue;
@@ -148,14 +167,6 @@ namespace kind {
     }  // namespace metakind
     }  // namespace kind
 
-// for hash_maps, hash_sets..
-struct NodeHashFunction {
-  inline size_t operator()(Node node) const;
-};/* struct NodeHashFunction */
-struct TNodeHashFunction {
-  inline size_t operator()(TNode node) const;
-};/* struct TNodeHashFunction */
-
 /**
  * Encapsulation of an NodeValue pointer.  The reference count is
  * maintained in the NodeValue if ref_count is true.
@@ -226,82 +237,85 @@ public:
    * Cache-aware, recursive version of substitute() used by the public
    * member function with a similar signature.
    */
-  Node substitute(TNode node, TNode replacement,
-                  std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
-
-  /**
-   * Cache-aware, recursive version of substitute() used by the public
-   * member function with a similar signature.
-   */
-  template <class Iterator1, class Iterator2>
-  Node substitute(Iterator1 nodesBegin, Iterator1 nodesEnd,
-                  Iterator2 replacementsBegin, Iterator2 replacementsEnd,
-                  std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
-
-  /**
-   * Cache-aware, recursive version of substitute() used by the public
-   * member function with a similar signature.
-   */
-  template <class Iterator>
-  Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd,
-                  std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
-
-  /** Default constructor, makes a null expression. */
-  NodeTemplate() : d_nv(&expr::NodeValue::null()) { }
-
-  /**
-   * Conversion between nodes that are reference-counted and those that are
-   * not.
-   * @param node the node to make copy of
-   */
-  NodeTemplate(const NodeTemplate<!ref_count>& node);
-
-  /**
-   * Copy constructor.  Note that GCC does NOT recognize an instantiation of
-   * the above template as a copy constructor and problems ensue.  So we
-   * provide an explicit one here.
-   * @param node the node to make copy of
-   */
-  NodeTemplate(const NodeTemplate& node);
-
-  /**
-   * Assignment operator for nodes, copies the relevant information from node
-   * to this node.
-   * @param node the node to copy
-   * @return reference to this node
-   */
-  NodeTemplate& operator=(const NodeTemplate& node);
-
-  /**
-   * Assignment operator for nodes, copies the relevant information from node
-   * to this node.
-   * @param node the node to copy
-   * @return reference to this node
-   */
-  NodeTemplate& operator=(const NodeTemplate<!ref_count>& node);
-
-  /**
-   * Destructor. If ref_count is true it will decrement the reference count
-   * and, if zero, collect the NodeValue.
-   */
-  ~NodeTemplate();
-
-  /**
-   * Return the null node.
-   * @return the null node
-   */
-  static NodeTemplate null() {
-    return s_null;
-  }
-
-  /**
-   * Returns true if this expression is a null expression.
-   * @return true if null
-   */
-  bool isNull() const {
-    assertTNodeNotExpired();
-    return d_nv == &expr::NodeValue::null();
-  }
+ Node substitute(TNode node,
+                 TNode replacement,
+                 std::unordered_map<TNode, TNode>& cache) const;
+
+ /**
+  * Cache-aware, recursive version of substitute() used by the public
+  * member function with a similar signature.
+  */
+ template <class Iterator1, class Iterator2>
+ Node substitute(Iterator1 nodesBegin,
+                 Iterator1 nodesEnd,
+                 Iterator2 replacementsBegin,
+                 Iterator2 replacementsEnd,
+                 std::unordered_map<TNode, TNode>& cache) const;
+
+ /**
+  * Cache-aware, recursive version of substitute() used by the public
+  * member function with a similar signature.
+  */
+ template <class Iterator>
+ Node substitute(Iterator substitutionsBegin,
+                 Iterator substitutionsEnd,
+                 std::unordered_map<TNode, TNode>& cache) const;
+
+ /** Default constructor, makes a null expression. */
+ NodeTemplate() : d_nv(&expr::NodeValue::null()) {}
+
+ /**
+  * Conversion between nodes that are reference-counted and those that are
+  * not.
+  * @param node the node to make copy of
+  */
+ NodeTemplate(const NodeTemplate<!ref_count>& node);
+
+ /**
+  * Copy constructor.  Note that GCC does NOT recognize an instantiation of
+  * the above template as a copy constructor and problems ensue.  So we
+  * provide an explicit one here.
+  * @param node the node to make copy of
+  */
+ NodeTemplate(const NodeTemplate& node);
+
+ /**
+  * Assignment operator for nodes, copies the relevant information from node
+  * to this node.
+  * @param node the node to copy
+  * @return reference to this node
+  */
+ NodeTemplate& operator=(const NodeTemplate& node);
+
+ /**
+  * Assignment operator for nodes, copies the relevant information from node
+  * to this node.
+  * @param node the node to copy
+  * @return reference to this node
+  */
+ NodeTemplate& operator=(const NodeTemplate<!ref_count>& node);
+
+ /**
+  * Destructor. If ref_count is true it will decrement the reference count
+  * and, if zero, collect the NodeValue.
+  */
+ ~NodeTemplate();
+
+ /**
+  * Return the null node.
+  * @return the null node
+  */
+ static NodeTemplate null() { return s_null; }
+
+ /**
+  * Returns true if this expression is a null expression.
+  * @return true if null
+  */
+ bool isNull() const
+ {
+   assertTNodeNotExpired();
+   return d_nv == &expr::NodeValue::null();
+ }
 
   /**
    * Structural comparison operator for expressions.
@@ -500,8 +514,7 @@ public:
   /**
    * Simultaneous substitution of Nodes in cache.
    */
-  Node substitute(
-      std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const;
+  Node substitute(std::unordered_map<TNode, TNode>& cache) const;
 
   /**
    * Returns the kind of this node.
@@ -942,15 +955,8 @@ std::ostream& operator<<(
 
 namespace cvc5 {
 
-inline size_t NodeHashFunction::operator()(Node node) const {
-  return node.getId();
-}
-inline size_t TNodeHashFunction::operator()(TNode node) const {
-  return node.getId();
-}
-
 using TNodePairHashFunction =
-    PairHashFunction<TNode, TNode, TNodeHashFunction, TNodeHashFunction>;
+    PairHashFunction<TNode, TNode, std::hash<TNode>, std::hash<TNode>>;
 
 template <bool ref_count>
 inline size_t NodeTemplate<ref_count>::getNumChildren() const {
@@ -1253,14 +1259,16 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const {
   if (node == *this) {
     return replacement;
   }
-  std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
+  std::unordered_map<TNode, TNode> cache;
   return substitute(node, replacement, cache);
 }
 
 template <bool ref_count>
-Node
-NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
-                                    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
+Node NodeTemplate<ref_count>::substitute(
+    TNode node,
+    TNode replacement,
+    std::unordered_map<TNode, TNode>& cache) const
+{
   Assert(node != *this);
 
   if (getNumChildren() == 0 || node == replacement)
@@ -1269,7 +1277,8 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
   }
 
   // in cache?
-  typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+  typename std::unordered_map<TNode, TNode>::const_iterator i =
+      cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
@@ -1309,21 +1318,23 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
                                     Iterator1 nodesEnd,
                                     Iterator2 replacementsBegin,
                                     Iterator2 replacementsEnd) const {
-  std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
+  std::unordered_map<TNode, TNode> cache;
   return substitute(nodesBegin, nodesEnd,
                     replacementsBegin, replacementsEnd, cache);
 }
 
 template <bool ref_count>
 template <class Iterator1, class Iterator2>
-Node
-NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
-                                    Iterator1 nodesEnd,
-                                    Iterator2 replacementsBegin,
-                                    Iterator2 replacementsEnd,
-                                    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
+Node NodeTemplate<ref_count>::substitute(
+    Iterator1 nodesBegin,
+    Iterator1 nodesEnd,
+    Iterator2 replacementsBegin,
+    Iterator2 replacementsEnd,
+    std::unordered_map<TNode, TNode>& cache) const
+{
   // in cache?
-  typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+  typename std::unordered_map<TNode, TNode>::const_iterator i =
+      cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
@@ -1366,13 +1377,13 @@ template <class Iterator>
 inline Node
 NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
                                     Iterator substitutionsEnd) const {
-  std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
+  std::unordered_map<TNode, TNode> cache;
   return substitute(substitutionsBegin, substitutionsEnd, cache);
 }
 
 template <bool ref_count>
 inline Node NodeTemplate<ref_count>::substitute(
-    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const
+    std::unordered_map<TNode, TNode>& cache) const
 {
   // Since no substitution is given (other than what may already be in the
   // cache), we pass dummy iterators to conform to the main substitute method,
@@ -1382,12 +1393,14 @@ inline Node NodeTemplate<ref_count>::substitute(
 
 template <bool ref_count>
 template <class Iterator>
-Node
-NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
-                                    Iterator substitutionsEnd,
-                                    std::unordered_map<TNode, TNode, TNodeHashFunction>& cache) const {
+Node NodeTemplate<ref_count>::substitute(
+    Iterator substitutionsBegin,
+    Iterator substitutionsEnd,
+    std::unordered_map<TNode, TNode>& cache) const
+{
   // in cache?
-  typename std::unordered_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+  typename std::unordered_map<TNode, TNode>::const_iterator i =
+      cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 0dc8858a2..19955443a 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -30,7 +30,7 @@ bool hasSubterm(TNode n, TNode t, bool strict)
     return true;
   }
 
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode> visited;
   std::vector<TNode> toProcess;
 
   toProcess.push_back(n);
@@ -76,9 +76,9 @@ bool hasSubterm(TNode n, TNode t, bool strict)
 
 bool hasSubtermMulti(TNode n, TNode t)
 {
-  std::unordered_map<TNode, bool, TNodeHashFunction> visited;
-  std::unordered_map<TNode, bool, TNodeHashFunction> contains;
-  std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it;
+  std::unordered_map<TNode, bool> visited;
+  std::unordered_map<TNode, bool> contains;
+  std::unordered_map<TNode, bool>::iterator it;
   std::vector<TNode> visit;
   TNode cur;
   visit.push_back(n);
@@ -131,7 +131,7 @@ bool hasSubtermMulti(TNode n, TNode t)
 
 bool hasSubtermKind(Kind k, Node n)
 {
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode> visited;
   std::vector<TNode> visit;
   TNode cur;
   visit.push_back(n);
@@ -162,7 +162,7 @@ bool hasSubtermKinds(const std::unordered_set<Kind, kind::KindHashFunction>& ks,
   {
     return false;
   }
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode> visited;
   std::vector<TNode> visit;
   TNode cur;
   visit.push_back(n);
@@ -194,7 +194,7 @@ bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict)
     return true;
   }
 
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode> visited;
   std::vector<TNode> toProcess;
 
   toProcess.push_back(n);
@@ -283,7 +283,7 @@ bool hasBoundVar(TNode n)
 
 bool hasFreeVar(TNode n)
 {
-  std::unordered_set<Node, NodeHashFunction> fvs;
+  std::unordered_set<Node> fvs;
   return getFreeVariables(n, fvs, false);
 }
 
@@ -324,20 +324,18 @@ bool hasClosure(Node n)
   return n.getAttribute(HasClosureAttr());
 }
 
-bool getFreeVariables(TNode n,
-                      std::unordered_set<Node, NodeHashFunction>& fvs,
-                      bool computeFv)
+bool getFreeVariables(TNode n, std::unordered_set<Node>& fvs, bool computeFv)
 {
-  std::unordered_set<TNode, TNodeHashFunction> scope;
+  std::unordered_set<TNode> scope;
   return getFreeVariablesScope(n, fvs, scope, computeFv);
 }
 
 bool getFreeVariablesScope(TNode n,
-                           std::unordered_set<Node, NodeHashFunction>& fvs,
-                           std::unordered_set<TNode, TNodeHashFunction>& scope,
+                           std::unordered_set<Node>& fvs,
+                           std::unordered_set<TNode>& scope,
                            bool computeFv)
 {
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode> visited;
   std::vector<TNode> visit;
   TNode cur;
   visit.push_back(n);
@@ -350,8 +348,7 @@ bool getFreeVariablesScope(TNode n,
     {
       continue;
     }
-    std::unordered_set<TNode, TNodeHashFunction>::iterator itv =
-        visited.find(cur);
+    std::unordered_set<TNode>::iterator itv = visited.find(cur);
     if (itv == visited.end())
     {
       visited.insert(cur);
@@ -404,9 +401,9 @@ bool getFreeVariablesScope(TNode n,
   return !fvs.empty();
 }
 
-bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs)
+bool getVariables(TNode n, std::unordered_set<TNode>& vs)
 {
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode> visited;
   std::vector<TNode> visit;
   TNode cur;
   visit.push_back(n);
@@ -414,8 +411,7 @@ bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs)
   {
     cur = visit.back();
     visit.pop_back();
-    std::unordered_set<TNode, TNodeHashFunction>::iterator itv =
-        visited.find(cur);
+    std::unordered_set<TNode>::iterator itv = visited.find(cur);
     if (itv == visited.end())
     {
       if (cur.isVar())
@@ -433,15 +429,15 @@ bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs)
   return !vs.empty();
 }
 
-void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms)
+void getSymbols(TNode n, std::unordered_set<Node>& syms)
 {
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode> visited;
   getSymbols(n, syms, visited);
 }
 
 void getSymbols(TNode n,
-                std::unordered_set<Node, NodeHashFunction>& syms,
-                std::unordered_set<TNode, TNodeHashFunction>& visited)
+                std::unordered_set<Node>& syms,
+                std::unordered_set<TNode>& visited)
 {
   std::vector<TNode> visit;
   TNode cur;
@@ -469,9 +465,9 @@ void getSymbols(TNode n,
 void getKindSubterms(TNode n,
                      Kind k,
                      bool topLevel,
-                     std::unordered_set<Node, NodeHashFunction>& ts)
+                     std::unordered_set<Node>& ts)
 {
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode> visited;
   std::vector<TNode> visit;
   TNode cur;
   visit.push_back(n);
@@ -500,18 +496,15 @@ void getKindSubterms(TNode n,
   } while (!visit.empty());
 }
 
-void getOperatorsMap(
-    TNode n,
-    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops)
+void getOperatorsMap(TNode n, std::map<TypeNode, std::unordered_set<Node>>& ops)
 {
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode> visited;
   getOperatorsMap(n, ops, visited);
 }
 
-void getOperatorsMap(
-    TNode n,
-    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops,
-    std::unordered_set<TNode, TNodeHashFunction>& visited)
+void getOperatorsMap(TNode n,
+                     std::map<TypeNode, std::unordered_set<Node>>& ops,
+                     std::unordered_set<TNode>& visited)
 {
   // nodes that we still need to visit
   std::vector<TNode> visit;
@@ -565,8 +558,8 @@ Node substituteCaptureAvoiding(TNode n,
                                std::vector<Node>& src,
                                std::vector<Node>& dest)
 {
-  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 curr;
   visit.push_back(n);
@@ -654,8 +647,7 @@ Node substituteCaptureAvoiding(TNode n,
   return visited[n];
 }
 
-void getComponentTypes(
-    TypeNode t, std::unordered_set<TypeNode, TypeNodeHashFunction>& types)
+void getComponentTypes(TypeNode t, std::unordered_set<TypeNode>& types)
 {
   std::vector<TypeNode> toProcess;
   toProcess.push_back(t);
@@ -676,14 +668,12 @@ void getComponentTypes(
   } while (!toProcess.empty());
 }
 
-bool match(Node x,
-           Node y,
-           std::unordered_map<Node, Node, NodeHashFunction>& subs)
+bool match(Node x, Node y, std::unordered_map<Node, Node>& subs)
 {
   std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction> visited;
   std::unordered_set<std::pair<TNode, TNode>, TNodePairHashFunction>::iterator
       it;
-  std::unordered_map<Node, Node, NodeHashFunction>::iterator subsIt;
+  std::unordered_map<Node, Node>::iterator subsIt;
 
   std::vector<std::pair<TNode, TNode>> stack;
   stack.emplace_back(x, y);
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 010724c80..b8576f787 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -103,7 +103,7 @@ bool hasClosure(Node n);
  * @return true iff this node contains a free variable.
  */
 bool getFreeVariables(TNode n,
-                      std::unordered_set<Node, NodeHashFunction>& fvs,
+                      std::unordered_set<Node>& fvs,
                       bool computeFv = true);
 /**
  * Get the free variables in n, that is, the subterms of n of kind
@@ -116,8 +116,8 @@ bool getFreeVariables(TNode n,
  * @return true iff this node contains a free variable.
  */
 bool getFreeVariablesScope(TNode n,
-                           std::unordered_set<Node, NodeHashFunction>& fvs,
-                           std::unordered_set<TNode, TNodeHashFunction>& scope,
+                           std::unordered_set<Node>& fvs,
+                           std::unordered_set<TNode>& scope,
                            bool computeFv = true);
 
 /**
@@ -126,7 +126,7 @@ bool getFreeVariablesScope(TNode n,
  * @param vs The set which free variables are added to
  * @return true iff this node contains a free variable.
  */
-bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs);
+bool getVariables(TNode n, std::unordered_set<TNode>& vs);
 
 /**
  * For term n, this function collects the symbols that occur as a subterms
@@ -134,7 +134,7 @@ bool getVariables(TNode n, std::unordered_set<TNode, TNodeHashFunction>& vs);
  * @param n The node under investigation
  * @param syms The set which the symbols of n are added to
  */
-void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms);
+void getSymbols(TNode n, std::unordered_set<Node>& syms);
 
 /**
  * For term n, this function collects the symbols that occur as a subterms
@@ -144,8 +144,8 @@ void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms);
  * @param visited A cache to be used for visited nodes.
  */
 void getSymbols(TNode n,
-                std::unordered_set<Node, NodeHashFunction>& syms,
-                std::unordered_set<TNode, TNodeHashFunction>& visited);
+                std::unordered_set<Node>& syms,
+                std::unordered_set<TNode>& visited);
 
 /**
  * For term n, this function collects the subterms of n whose kind is k.
@@ -157,7 +157,7 @@ void getSymbols(TNode n,
 void getKindSubterms(TNode n,
                      Kind k,
                      bool topLevel,
-                     std::unordered_set<Node, NodeHashFunction>& ts);
+                     std::unordered_set<Node>& ts);
 
 /**
  * For term n, this function collects the operators that occur in n.
@@ -165,9 +165,8 @@ void getKindSubterms(TNode n,
  * @param ops The map (from each type to operators of that type) which the
  * operators of n are added to
  */
-void getOperatorsMap(
-    TNode n,
-    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops);
+void getOperatorsMap(TNode n,
+                     std::map<TypeNode, std::unordered_set<Node>>& ops);
 
 /**
  * For term n, this function collects the operators that occur in n.
@@ -176,10 +175,9 @@ void getOperatorsMap(
  * operators of n are added to
  * @param visited A cache to be used for visited nodes.
  */
-void getOperatorsMap(
-    TNode n,
-    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& ops,
-    std::unordered_set<TNode, TNodeHashFunction>& visited);
+void getOperatorsMap(TNode n,
+                     std::map<TypeNode, std::unordered_set<Node>>& ops,
+                     std::unordered_set<TNode>& visited);
 
 /*
  * Substitution of Nodes in a capture avoiding way.
@@ -208,8 +206,7 @@ Node substituteCaptureAvoiding(TNode n,
  * @param t The type node under investigation
  * @param types The set which component types are added to.
  */
-void getComponentTypes(
-    TypeNode t, std::unordered_set<TypeNode, TypeNodeHashFunction>& types);
+void getComponentTypes(TypeNode t, std::unordered_set<TypeNode>& types);
 
 /** match
  *
@@ -230,9 +227,7 @@ void getComponentTypes(
  * @param subs the mapping from free vars in `n1` to terms in `n2`
  * @return whether or not `n2` is an instance of `n1`
  */
-bool match(Node n1,
-           Node n2,
-           std::unordered_map<Node, Node, NodeHashFunction>& subs);
+bool match(Node n1, Node n2, std::unordered_map<Node, Node>& subs);
 
 }  // namespace expr
 }  // namespace cvc5
diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h
index 6489e19c8..75ae9c068 100644
--- a/src/expr/node_traversal.h
+++ b/src/expr/node_traversal.h
@@ -98,7 +98,7 @@ class NodeDfsIterator
   // Absent if we haven't visited it.
   // Set to `false` if we've already pre-visited it (enqueued its children).
   // Set to `true` if we've also already post-visited it.
-  std::unordered_map<TNode, bool, TNodeHashFunction> d_visited;
+  std::unordered_map<TNode, bool> d_visited;
 
   // The visit order that this iterator is using
   VisitOrder d_order;
diff --git a/src/expr/proof.h b/src/expr/proof.h
index 25ab1fd23..496815938 100644
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -246,8 +246,7 @@ class CDProof : public ProofGenerator
   std::string identify() const override;
 
  protected:
-  typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
-      NodeProofNodeMap;
+  typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap;
   /** The proof manager, used for allocating new ProofNode objects */
   ProofNodeManager* d_manager;
   /** A dummy context used by this class if none is provided */
diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp
index 957893cb3..4bb35b5dc 100644
--- a/src/expr/proof_node_algorithm.cpp
+++ b/src/expr/proof_node_algorithm.cpp
@@ -61,7 +61,7 @@ void getFreeAssumptionsMap(
   //   after postvisiting SCOPE1: { y: 1 }
   //   after postvisiting SCOPE2: {}
   //
-  std::unordered_map<Node, uint32_t, NodeHashFunction> scopeDepth;
+  std::unordered_map<Node, uint32_t> scopeDepth;
   std::shared_ptr<ProofNode> cur;
   visit.push_back(pn);
   do
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index d4a8b604f..c2c72f35d 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -87,19 +87,19 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
   }
   Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl;
   // we first ensure the assumptions are flattened
-  std::unordered_set<Node, NodeHashFunction> ac{assumps.begin(), assumps.end()};
+  std::unordered_set<Node> ac{assumps.begin(), assumps.end()};
   // map from the rewritten form of assumptions to the original. This is only
   // computed in the rare case when we need rewriting to match the
   // assumptions. An example of this is for Boolean constant equalities in
   // scoped proofs from the proof equality engine.
-  std::unordered_map<Node, Node, NodeHashFunction> acr;
+  std::unordered_map<Node, Node> acr;
   // whether we have compute the map above
   bool computedAcr = false;
 
   // The free assumptions of the proof
   std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
   expr::getFreeAssumptionsMap(pf, famap);
-  std::unordered_set<Node, NodeHashFunction> acu;
+  std::unordered_set<Node> acu;
   for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
            fa : famap)
   {
@@ -153,8 +153,7 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
         }
       }
       Node ar = theory::Rewriter::rewrite(a);
-      std::unordered_map<Node, Node, NodeHashFunction>::iterator itr =
-          acr.find(ar);
+      std::unordered_map<Node, Node>::iterator itr = acr.find(ar);
       if (itr != acr.end())
       {
         aMatch = itr->second;
diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp
index 9e68f6cd7..4202c70ec 100644
--- a/src/expr/sequence.cpp
+++ b/src/expr/sequence.cpp
@@ -374,7 +374,7 @@ size_t SequenceHashFunction::operator()(const Sequence& s) const
   const std::vector<Node>& vec = s.getVec();
   for (const Node& n : vec)
   {
-    ret = fnv1a::fnv1a_64(ret, NodeHashFunction()(n));
+    ret = fnv1a::fnv1a_64(ret, std::hash<Node>()(n));
   }
   return ret;
 }
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index b59d01fdd..bb29f84ee 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -243,8 +243,8 @@ Node SkolemManager::getOriginalForm(Node n)
       << "SkolemManager::getOriginalForm " << n << std::endl;
   OriginalFormAttribute ofa;
   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(n);
diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h
index ba8c438b2..bc067f60a 100644
--- a/src/expr/tconv_seq_proof_generator.h
+++ b/src/expr/tconv_seq_proof_generator.h
@@ -102,7 +102,7 @@ class TConvSeqProofGenerator : public ProofGenerator
 
  protected:
   using NodeIndexPairHashFunction =
-      PairHashFunction<Node, size_t, NodeHashFunction>;
+      PairHashFunction<Node, size_t, std::hash<Node>>;
   typedef context::
       CDHashMap<std::pair<Node, size_t>, Node, NodeIndexPairHashFunction>
           NodeIndexNodeMap;
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
index 3d68fd181..0e0ed3165 100644
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -266,11 +266,11 @@ Node TConvProofGenerator::getProofForRewriting(Node t,
   // nodes.
 
   // the final rewritten form of terms
-  std::unordered_map<Node, Node, TNodeHashFunction> visited;
+  std::unordered_map<Node, Node> visited;
   // the rewritten form of terms we have processed so far
-  std::unordered_map<Node, Node, TNodeHashFunction> rewritten;
-  std::unordered_map<Node, Node, TNodeHashFunction>::iterator it;
-  std::unordered_map<Node, Node, TNodeHashFunction>::iterator itr;
+  std::unordered_map<Node, Node> rewritten;
+  std::unordered_map<Node, Node>::iterator it;
+  std::unordered_map<Node, Node>::iterator itr;
   std::map<Node, std::shared_ptr<ProofNode> >::iterator itc;
   Trace("tconv-pf-gen-rewrite")
       << "TConvProofGenerator::getProofForRewriting: " << toStringDebug()
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
index e546d23bd..70e606db4 100644
--- a/src/expr/term_conversion_proof_generator.h
+++ b/src/expr/term_conversion_proof_generator.h
@@ -200,7 +200,7 @@ class TConvProofGenerator : public ProofGenerator
   std::shared_ptr<ProofNode> getProofForRewriting(Node n);
 
  protected:
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+  typedef context::CDHashMap<Node, Node> NodeNodeMap;
   /** A dummy context used by this class if none is provided */
   context::Context d_context;
   /** The (lazy) context dependent proof object. */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index bd435a392..b4f2f7efa 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -29,11 +29,13 @@ namespace cvc5 {
 
 TypeNode TypeNode::s_null( &expr::NodeValue::null() );
 
-TypeNode TypeNode::substitute(const TypeNode& type,
-                              const TypeNode& replacement,
-                              std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const {
+TypeNode TypeNode::substitute(
+    const TypeNode& type,
+    const TypeNode& replacement,
+    std::unordered_map<TypeNode, TypeNode>& cache) const
+{
   // in cache?
-  std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
+  std::unordered_map<TypeNode, TypeNode>::const_iterator i = cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
@@ -683,3 +685,12 @@ TypeNode TypeNode::getBagElementType() const
 }
 
 }  // namespace cvc5
+
+namespace std {
+
+size_t hash<cvc5::TypeNode>::operator()(const cvc5::TypeNode& tn) const
+{
+  return tn.getId();
+}
+
+}  // namespace std
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 0ab1d0217..1840820dc 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -47,15 +47,6 @@ namespace expr {
  */
 class TypeNode {
 
-public:
-
-  // for hash_maps, hash_sets..
-  struct HashFunction {
-    size_t operator()(TypeNode node) const {
-      return (size_t) node.getId();
-    }
-  };/* struct HashFunction */
-
 private:
 
   /**
@@ -92,20 +83,22 @@ private:
    * Cache-aware, recursive version of substitute() used by the public
    * member function with a similar signature.
    */
-  TypeNode substitute(const TypeNode& type, const TypeNode& replacement,
-                      std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const;
+  TypeNode substitute(const TypeNode& type,
+                      const TypeNode& replacement,
+                      std::unordered_map<TypeNode, TypeNode>& cache) const;
 
   /**
    * Cache-aware, recursive version of substitute() used by the public
    * member function with a similar signature.
    */
   template <class Iterator1, class Iterator2>
-  TypeNode substitute(Iterator1 typesBegin, Iterator1 typesEnd,
-                      Iterator2 replacementsBegin, Iterator2 replacementsEnd,
-                      std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const;
-
-public:
+  TypeNode substitute(Iterator1 typesBegin,
+                      Iterator1 typesEnd,
+                      Iterator2 replacementsBegin,
+                      Iterator2 replacementsEnd,
+                      std::unordered_map<TypeNode, TypeNode>& cache) const;
 
+ public:
   /** Default constructor, makes a null expression. */
   TypeNode() : d_nv(&expr::NodeValue::null()) { }
 
@@ -735,10 +728,18 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
   return out;
 }
 
-typedef TypeNode::HashFunction TypeNodeHashFunction;
-
 }  // namespace cvc5
 
+namespace std {
+
+template <>
+struct hash<cvc5::TypeNode>
+{
+  size_t operator()(const cvc5::TypeNode& tn) const;
+};
+
+}  // namespace std
+
 #include "expr/node_manager.h"
 
 namespace cvc5 {
@@ -746,7 +747,7 @@ namespace cvc5 {
 inline TypeNode
 TypeNode::substitute(const TypeNode& type,
                      const TypeNode& replacement) const {
-  std::unordered_map<TypeNode, TypeNode, HashFunction> cache;
+  std::unordered_map<TypeNode, TypeNode> cache;
   return substitute(type, replacement, cache);
 }
 
@@ -756,19 +757,21 @@ TypeNode::substitute(Iterator1 typesBegin,
                      Iterator1 typesEnd,
                      Iterator2 replacementsBegin,
                      Iterator2 replacementsEnd) const {
-  std::unordered_map<TypeNode, TypeNode, HashFunction> cache;
+  std::unordered_map<TypeNode, TypeNode> cache;
   return substitute(typesBegin, typesEnd,
                     replacementsBegin, replacementsEnd, cache);
 }
 
 template <class Iterator1, class Iterator2>
-TypeNode TypeNode::substitute(Iterator1 typesBegin,
-                              Iterator1 typesEnd,
-                              Iterator2 replacementsBegin,
-                              Iterator2 replacementsEnd,
-                              std::unordered_map<TypeNode, TypeNode, HashFunction>& cache) const {
+TypeNode TypeNode::substitute(
+    Iterator1 typesBegin,
+    Iterator1 typesEnd,
+    Iterator2 replacementsBegin,
+    Iterator2 replacementsEnd,
+    std::unordered_map<TypeNode, TypeNode>& cache) const
+{
   // in cache?
-  std::unordered_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
+  std::unordered_map<TypeNode, TypeNode>::const_iterator i = cache.find(*this);
   if(i != cache.end()) {
     return (*i).second;
   }
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index 039a77eb3..ef354568d 100644
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -90,7 +90,7 @@ std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) {
 size_t UninterpretedConstantHashFunction::operator()(
     const UninterpretedConstant& uc) const
 {
-  return TypeNodeHashFunction()(uc.getType())
+  return std::hash<TypeNode>()(uc.getType())
          * IntegerHashFunction()(uc.getIndex());
 }