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

Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.

23 files changed, 84 insertions, 89 deletions

diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index 67a04bfea..7eea90cdc 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -32,17 +32,16 @@ namespace bv {
 typedef std::vector<TNode> ArgsVec;
 
 class AbstractionModule {
-  using NodeVecMap =
-      std::unordered_map<Node, std::vector<Node>, NodeHashFunction>;
-  using NodeTNodeMap = std::unordered_map<Node, TNode, NodeHashFunction>;
-  using TNodeTNodeMap = std::unordered_map<TNode, TNode, TNodeHashFunction>;
-  using NodeNodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
-  using TNodeNodeMap = std::unordered_map<Node, TNode, NodeHashFunction>;
-  using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
+  using NodeVecMap = std::unordered_map<Node, std::vector<Node>>;
+  using NodeTNodeMap = std::unordered_map<Node, TNode>;
+  using TNodeTNodeMap = std::unordered_map<TNode, TNode>;
+  using NodeNodeMap = std::unordered_map<Node, Node>;
+  using TNodeNodeMap = std::unordered_map<Node, TNode>;
+  using TNodeSet = std::unordered_set<TNode>;
   using IntNodeMap = std::unordered_map<unsigned, Node>;
   using IndexMap = std::unordered_map<unsigned, unsigned>;
   using SkolemMap = std::unordered_map<unsigned, std::vector<Node> >;
-  using SignatureMap = std::unordered_map<TNode, unsigned, TNodeHashFunction>;
+  using SignatureMap = std::unordered_map<TNode, unsigned>;
 
   struct Statistics {
     SizeStat<NodeNodeMap> d_numFunctionsAbstracted;
@@ -77,15 +76,15 @@ class AbstractionModule {
   };
 
   class ArgsTable {
-    std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data;
+    std::unordered_map<TNode, ArgsTableEntry> d_data;
     bool hasEntry(TNode signature) const;
   public:
-    typedef std::unordered_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator;
-    ArgsTable() {}
-    void addEntry(TNode signature, const ArgsVec& args);
-    ArgsTableEntry& getEntry(TNode signature);
-    iterator begin() { return d_data.begin(); }
-    iterator end() { return d_data.end(); }
+   typedef std::unordered_map<TNode, ArgsTableEntry>::iterator iterator;
+   ArgsTable() {}
+   void addEntry(TNode signature, const ArgsVec& args);
+   ArgsTableEntry& getEntry(TNode signature);
+   iterator begin() { return d_data.begin(); }
+   iterator end() { return d_data.end(); }
   };
 
   /**
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index a7dfb00e5..39ecbc12c 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -56,8 +56,8 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*>
   static Abc_Ntk_t* currentAigNtk();
 
  private:
-  typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction> TNodeAigMap;
-  typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction> NodeAigMap;
+  typedef std::unordered_map<TNode, Abc_Obj_t*> TNodeAigMap;
+  typedef std::unordered_map<Node, Abc_Obj_t*> NodeAigMap;
 
   static thread_local Abc_Ntk_t* s_abcAigNetwork;
   std::unique_ptr<context::Context> d_nullContext;
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index 2a7931aa0..a669e4a86 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -38,8 +38,8 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
-typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
-typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_set<Node> NodeSet;
+typedef std::unordered_set<TNode> TNodeSet;
 
 /**
  * The Bitblaster that manages the mapping between Nodes
@@ -52,9 +52,9 @@ class TBitblaster
 {
  protected:
   typedef std::vector<T> Bits;
-  typedef std::unordered_map<Node, Bits, NodeHashFunction> TermDefMap;
-  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
-  typedef std::unordered_map<Node, Node, NodeHashFunction> ModelCache;
+  typedef std::unordered_map<Node, Bits> TermDefMap;
+  typedef std::unordered_set<TNode> TNodeSet;
+  typedef std::unordered_map<Node, Node> ModelCache;
 
   typedef void (*TermBBStrategy)(TNode, Bits&, TBitblaster<T>*);
   typedef T (*AtomBBStrategy)(TNode, TBitblaster<T>*);
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index 765f3051e..9e5ace9d8 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -56,7 +56,7 @@ class EagerBitblaster : public TBitblaster<Node>
  private:
   context::Context* d_context;
 
-  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef std::unordered_set<TNode> TNodeSet;
   std::unique_ptr<prop::SatSolver> d_satSolver;
   std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
 
diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp
index 09448da8a..4d6501673 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.cpp
+++ b/src/theory/bv/bitblast/proof_bitblaster.cpp
@@ -81,7 +81,7 @@ void BBProof::bbAtom(TNode node)
 {
   std::vector<TNode> visit;
   visit.push_back(node);
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode> visited;
 
   bool fproofs =
       options::proofGranularityMode() != options::ProofGranularityMode::OFF;
diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h
index 6cd4960fb..ef23c05c0 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.h
+++ b/src/theory/bv/bitblast/proof_bitblaster.h
@@ -60,7 +60,7 @@ class BBProof
   /** The associated term conversion proof generator. */
   TConvProofGenerator* d_tcpg;
   /** Map bit-vector nodes to bit-blasted nodes. */
-  std::unordered_map<Node, Node, NodeHashFunction> d_bbMap;
+  std::unordered_map<Node, Node> d_bbMap;
 };
 
 }  // namespace bv
diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h
index 04a35bc4f..ebbb2891f 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.h
+++ b/src/theory/bv/bitblast/simple_bitblaster.h
@@ -68,7 +68,7 @@ class BBSimple : public TBitblaster<Node>
   /** Caches variables for which we already created bits. */
   TNodeSet d_variables;
   /** Stores bit-blasted atoms. */
-  std::unordered_map<Node, Node, NodeHashFunction> d_bbAtoms;
+  std::unordered_map<Node, Node> d_bbAtoms;
   /** Theory state. */
   TheoryState* d_state;
 };
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 4b6c4fc5b..ab51ea844 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -45,8 +45,8 @@ class EagerBitblastSolver {
   bool collectModelInfo(theory::TheoryModel* m, bool fullModel);
 
  private:
-  context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
-  context::CDHashSet<Node, NodeHashFunction> d_assumptionSet;
+  context::CDHashSet<Node> d_assertionSet;
+  context::CDHashSet<Node> d_assumptionSet;
   context::Context* d_context;
 
   /** Bitblasters */
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 0fa96e619..32b6dbd7a 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -99,17 +99,18 @@ class InequalityGraph : public context::ContextNotifyObj{
 
       return (*(d_model->find(left))).second.value < (*(d_model->find(right))).second.value; 
     }
-  }; 
+  };
 
-  typedef std::unordered_map<TNode, ReasonId, TNodeHashFunction> ReasonToIdMap;
-  typedef std::unordered_map<TNode, TermId, TNodeHashFunction> TermNodeToIdMap;
+  typedef std::unordered_map<TNode, ReasonId> ReasonToIdMap;
+  typedef std::unordered_map<TNode, TermId> TermNodeToIdMap;
 
   typedef std::vector<InequalityEdge> Edges; 
   typedef std::unordered_set<TermId> TermIdSet;
 
-  typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator> BFSQueue; 
-  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
-  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+  typedef std::priority_queue<TermId, std::vector<TermId>, QueueComparator>
+      BFSQueue;
+  typedef std::unordered_set<TNode> TNodeSet;
+  typedef std::unordered_set<Node> NodeSet;
 
   std::vector<InequalityNode> d_ineqNodes;
   std::vector< Edges > d_ineqEdges;
@@ -206,7 +207,7 @@ class InequalityGraph : public context::ContextNotifyObj{
   
   /*** The currently asserted disequalities */
   context::CDQueue<TNode> d_disequalities;
-  typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+  typedef context::CDHashSet<Node> CDNodeSet;
   CDNodeSet d_disequalitiesAlreadySplit; 
   Node makeDiseqSplitLemma(TNode diseq); 
   /** Backtracking mechanisms **/
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index f22f298ac..d1411d784 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -100,8 +100,7 @@ class BVQuickCheck
   bool collectModelValues(theory::TheoryModel* model,
                           const std::set<Node>& termSet);
 
-  typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator
-      vars_iterator;
+  typedef std::unordered_set<TNode>::const_iterator vars_iterator;
   vars_iterator beginVars();
   vars_iterator endVars();
 
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index a9d46f068..ecf2bafb6 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -261,7 +261,7 @@ Node BVSolverBitblast::getValue(TNode node)
         nb << cur.getOperator();
       }
 
-      std::unordered_map<Node, Node, NodeHashFunction>::iterator iit;
+      std::unordered_map<Node, Node>::iterator iit;
       for (const TNode& child : cur)
       {
         iit = d_modelCache.find(child);
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index 384017f5f..36c06209a 100644
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -87,7 +87,7 @@ class BVSolverBitblast : public BVSolver
    * Is cleared at the beginning of a getValue() call if the
    * `d_invalidateModelCache` flag is set to true.
    */
-  std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
+  std::unordered_map<Node, Node> d_modelCache;
 
   /** Bit-blaster used to bit-blast atoms/terms. */
   std::unique_ptr<BBSimple> d_bitblaster;
@@ -123,8 +123,7 @@ class BVSolverBitblast : public BVSolver
   BVProofRuleChecker d_bvProofChecker;
 
   /** Stores the SatLiteral for a given fact. */
-  context::CDHashMap<Node, prop::SatLiteral, NodeHashFunction>
-      d_factLiteralCache;
+  context::CDHashMap<Node, prop::SatLiteral> d_factLiteralCache;
 
   /** Reverse map of `d_factLiteralCache`. */
   context::CDHashMap<prop::SatLiteral, Node, prop::SatLiteralHashFunction>
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index 57b3e0a08..9b3a2f1fa 100644
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -49,8 +49,8 @@ class BVSolverLazy : public BVSolver
   context::Context* d_context;
 
   /** Context dependent set of atoms we already propagated */
-  context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
-  context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
+  context::CDHashSet<Node> d_alreadyPropagatedSet;
+  context::CDHashSet<Node> d_sharedTermsSet;
 
   std::vector<std::unique_ptr<SubtheorySolver>> d_subtheories;
   std::unordered_map<SubTheory, SubtheorySolver*, std::hash<int>>
@@ -122,11 +122,11 @@ class BVSolverLazy : public BVSolver
   void check(Theory::Effort e);
   void spendResource(Resource r);
 
-  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
-  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+  typedef std::unordered_set<TNode> TNodeSet;
+  typedef std::unordered_set<Node> NodeSet;
   NodeSet d_staticLearnCache;
 
-  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
+  typedef std::unordered_map<Node, Node> NodeToNode;
 
   context::CDO<bool> d_lemmasAdded;
 
@@ -149,7 +149,7 @@ class BVSolverLazy : public BVSolver
    * Keeps a map from nodes to the subtheory that propagated it so that we can
    * explain it properly.
    */
-  typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
+  typedef context::CDHashMap<Node, SubTheory> PropagatedMap;
   PropagatedMap d_propagatedBy;
 
   std::unique_ptr<EagerBitblastSolver> d_eagerSolver;
diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp
index 52f5d52ac..3faad29a9 100644
--- a/src/theory/bv/bv_solver_simple.cpp
+++ b/src/theory/bv/bv_solver_simple.cpp
@@ -38,10 +38,10 @@ bool isBVAtom(TNode n)
 }
 
 /* Traverse Boolean nodes and collect BV atoms. */
-void collectBVAtoms(TNode n, std::unordered_set<Node, NodeHashFunction>& atoms)
+void collectBVAtoms(TNode n, std::unordered_set<Node>& atoms)
 {
   std::vector<TNode> visit;
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode> visited;
 
   visit.push_back(n);
 
@@ -138,7 +138,7 @@ bool BVSolverSimple::preNotifyFact(
       d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_LEMMA);
     }
 
-    std::unordered_set<Node, NodeHashFunction> bv_atoms;
+    std::unordered_set<Node> bv_atoms;
     collectBVAtoms(n, bv_atoms);
     for (const Node& nn : bv_atoms)
     {
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 90276f8b1..3a9e460fe 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -47,7 +47,7 @@ namespace {
 void collectVariables(TNode node, utils::NodeSet& vars)
 {
   std::vector<TNode> stack;
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode> visited;
 
   stack.push_back(node);
   while (!stack.empty())
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index 670adafa3..b93ff235f 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -58,10 +58,8 @@ class SubstitutionEx
     }
   };
 
-  typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction>
-      Substitutions;
-  typedef std::unordered_map<Node, SubstitutionElement, NodeHashFunction>
-      SubstitutionsCache;
+  typedef std::unordered_map<Node, SubstitutionElement> Substitutions;
+  typedef std::unordered_map<Node, SubstitutionElement> SubstitutionsCache;
 
   Substitutions d_substitutions;
   SubstitutionsCache d_cache;
@@ -103,9 +101,9 @@ struct WorklistElement
   WorklistElement() : node(), id(-1) {}
 };
 
-typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
-typedef std::unordered_map<Node, unsigned, NodeHashFunction> NodeIdMap;
-typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_map<Node, Node> NodeNodeMap;
+typedef std::unordered_map<Node, unsigned> NodeIdMap;
+typedef std::unordered_set<TNode> TNodeSet;
 
 class ExtractSkolemizer
 {
@@ -124,7 +122,7 @@ class ExtractSkolemizer
     ExtractList() : base(1), extracts() {}
     void addExtract(Extract& e);
   };
-  typedef std::unordered_map<Node, ExtractList, NodeHashFunction> VarExtractMap;
+  typedef std::unordered_map<Node, ExtractList> VarExtractMap;
   context::Context d_emptyContext;
   VarExtractMap d_varToExtract;
   theory::SubstitutionMap* d_modelMap;
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 903a5136e..439bd33ed 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -49,7 +49,7 @@ class BitblastSolver : public SubtheorySolver
   context::CDQueue<TNode> d_bitblastQueue;
   Statistics d_statistics;
 
-  typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+  typedef std::unordered_map<Node, Node> NodeMap;
   NodeMap d_modelCache;
   context::CDO<bool> d_validModelCache;
 
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 52d9e739a..0dfcfdde4 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -50,10 +50,9 @@ class CoreSolverExtTheoryCallback : public ExtTheoryCallback
  * Bitvector equality solver
  */
 class CoreSolver : public SubtheorySolver {
-  typedef std::unordered_map<TNode, Node, TNodeHashFunction> ModelValue;
-  typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
-  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
-
+  typedef std::unordered_map<TNode, Node> ModelValue;
+  typedef std::unordered_map<TNode, bool> TNodeBoolMap;
+  typedef std::unordered_set<TNode> TNodeSet;
 
   struct Statistics {
     IntStat d_numCallstoCheck;
@@ -103,7 +102,7 @@ class CoreSolver : public SubtheorySolver {
   std::unique_ptr<ExtTheory> d_extTheory;
 
   /** To make sure we keep the explanations */
-  context::CDHashSet<Node, NodeHashFunction> d_reasons;
+  context::CDHashSet<Node> d_reasons;
   ModelValue d_modelValues;
   void buildModel();
   bool assertFactToEqualityEngine(TNode fact, TNode reason);
@@ -113,8 +112,8 @@ class CoreSolver : public SubtheorySolver {
   /** Whether we need a last call effort check */
   bool d_needsLastCallCheck;
   /** For extended functions */
-  context::CDHashSet<Node, NodeHashFunction> d_extf_range_infer;
-  context::CDHashSet<Node, NodeHashFunction> d_extf_collapse_infer;
+  context::CDHashSet<Node> d_extf_range_infer;
+  context::CDHashSet<Node> d_extf_collapse_infer;
 
   /** do extended function inferences
    *
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 65eee95e1..f8a7bf113 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -51,11 +51,11 @@ class InequalitySolver : public SubtheorySolver
     Statistics();
   };
 
-  context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
+  context::CDHashSet<Node> d_assertionSet;
   InequalityGraph d_inequalityGraph;
-  context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations;
+  context::CDHashMap<Node, TNode> d_explanations;
   context::CDO<bool> d_isComplete;
-  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+  typedef std::unordered_set<Node> NodeSet;
   NodeSet d_ineqTerms;
   bool isInequalityOnly(TNode node);
   bool addInequality(TNode a, TNode b, bool strict, TNode fact);
diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h
index 7fb463721..f8717e045 100644
--- a/src/theory/bv/int_blaster.h
+++ b/src/theory/bv/int_blaster.h
@@ -87,7 +87,7 @@ namespace cvc5 {
 **/
 class IntBlaster
 {
-  using CDNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>;
+  using CDNodeMap = context::CDHashMap<Node, Node>;
 
  public:
   /**
@@ -319,13 +319,13 @@ class IntBlaster
    * Range constraints of the form 0 <= x < 2^k
    * These are added for every new integer variable that we introduce.
    */
-  context::CDHashSet<Node, NodeHashFunction> d_rangeAssertions;
+  context::CDHashSet<Node> d_rangeAssertions;
 
   /**
    * A set of "bitwise" equalities over integers for BITVECTOR_AND
    *   used in for options::SolveBVAsIntMode::BITWISE
    */
-  context::CDHashSet<Node, NodeHashFunction> d_bitwiseAssertions;
+  context::CDHashSet<Node> d_bitwiseAssertions;
 
   /** Useful constants */
   Node d_zero;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 63d618da2..4a2d2943d 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -1047,7 +1047,10 @@ struct Count {
   {}
 };
 
-inline static void insert(std::unordered_map<TNode, Count, TNodeHashFunction>& map, TNode node, bool neg) {
+inline static void insert(std::unordered_map<TNode, Count>& map,
+                          TNode node,
+                          bool neg)
+{
   if(map.find(node) == map.end()) {
     Count c = neg? Count(0,1) : Count(1, 0);
     map[node] = c; 
@@ -1073,7 +1076,7 @@ inline Node RewriteRule<AndSimplify>::apply(TNode node)
 
   NodeManager *nm = NodeManager::currentNM();
   // this will remove duplicates
-  std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
+  std::unordered_map<TNode, Count> subterms;
   unsigned size = utils::getSize(node);
   BitVector constant = BitVector::mkOnes(size);
   for (unsigned i = 0; i < node.getNumChildren(); ++i)
@@ -1110,8 +1113,7 @@ inline Node RewriteRule<AndSimplify>::apply(TNode node)
     children.push_back(utils::mkConst(constant)); 
   }
 
-  std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it =
-      subterms.begin();
+  std::unordered_map<TNode, Count>::const_iterator it = subterms.begin();
 
   for (; it != subterms.end(); ++it)
   {
@@ -1163,7 +1165,7 @@ Node RewriteRule<FlattenAssocCommutNoDuplicates>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl;
   std::vector<Node> processingStack;
   processingStack.push_back(node);
-  std::unordered_set<TNode, TNodeHashFunction> processed;
+  std::unordered_set<TNode> processed;
   std::vector<Node> children;
   Kind kind = node.getKind(); 
   
@@ -1200,7 +1202,7 @@ inline Node RewriteRule<OrSimplify>::apply(TNode node)
 
   NodeManager *nm = NodeManager::currentNM();
   // this will remove duplicates
-  std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
+  std::unordered_map<TNode, Count> subterms;
   unsigned size = utils::getSize(node);
   BitVector constant(size, (unsigned)0);
 
@@ -1238,8 +1240,7 @@ inline Node RewriteRule<OrSimplify>::apply(TNode node)
     children.push_back(utils::mkConst(constant));
   }
 
-  std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it =
-      subterms.begin();
+  std::unordered_map<TNode, Count>::const_iterator it = subterms.begin();
 
   for (; it != subterms.end(); ++it)
   {
@@ -1283,7 +1284,7 @@ inline Node RewriteRule<XorSimplify>::apply(TNode node)
                       << std::endl;
 
   NodeManager *nm = NodeManager::currentNM();
-  std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
+  std::unordered_map<TNode, Count> subterms;
   unsigned size = utils::getSize(node);
   BitVector constant;
   bool const_set = false;
@@ -1321,8 +1322,7 @@ inline Node RewriteRule<XorSimplify>::apply(TNode node)
 
   std::vector<Node> children;
 
-  std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it =
-      subterms.begin();
+  std::unordered_map<TNode, Count>::const_iterator it = subterms.begin();
   unsigned true_count = 0;
   bool seen_false = false;
   for (; it != subterms.end(); ++it)
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index eb2fd6527..1549df639 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -140,7 +140,7 @@ static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache)
   TNode t = term.getKind() == kind::NOT ? term[0] : term;
 
   std::vector<TNode> stack;
-  std::unordered_map<TNode, bool, TNodeHashFunction> visited;
+  std::unordered_map<TNode, bool> visited;
   stack.push_back(t);
 
   while (!stack.empty())
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 4844c1a93..8e916e975 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -28,13 +28,13 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
-typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
-typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+typedef std::unordered_set<Node> NodeSet;
+typedef std::unordered_set<TNode> TNodeSet;
 
 namespace utils {
 
-typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
-typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+typedef std::unordered_map<TNode, bool> TNodeBoolMap;
+typedef std::unordered_set<Node> NodeSet;
 
 /* Get the bit-width of given node. */
 unsigned getSize(TNode node);