11 files changed, 17 insertions, 20 deletions
diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h
index b2279344d..b0a4fd859 100644
--- a/src/theory/arith/nl/ext/ext_state.h
+++ b/src/theory/arith/nl/ext/ext_state.h
@@ -86,7 +86,7 @@ struct ExtState
   // ( x*y, x*z, y ) for each pair of monomials ( x*y, x*z ) with common factors
   std::map<Node, std::map<Node, Node> > d_mono_diff;
   /** the set of monomials we should apply tangent planes to */
-  std::unordered_set<Node, NodeHashFunction> d_tplane_refine;
+  std::unordered_set<Node> d_tplane_refine;
 };
 
 }  // namespace nl
diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index 6df35c71d..404916453 100644
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -238,7 +238,7 @@ void MonomialCheck::checkMagnitude(unsigned c)
   Trace("nl-ext-comp") << "Compute redundancies for " << lemmas.size()
                        << " lemmas." << std::endl;
   // naive
-  std::unordered_set<Node, NodeHashFunction> r_lemmas;
+  std::unordered_set<Node> r_lemmas;
   for (std::map<int, std::map<Node, std::map<Node, Node> > >::iterator itb =
            cmp_infers.begin();
        itb != cmp_infers.end();
diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h
index b42c7932d..c50737d51 100644
--- a/src/theory/arith/nl/ext/split_zero_check.h
+++ b/src/theory/arith/nl/ext/split_zero_check.h
@@ -40,7 +40,7 @@ class SplitZeroCheck
   void check();
 
  private:
-  using NodeSet = context::CDHashSet<Node, NodeHashFunction>;
+  using NodeSet = context::CDHashSet<Node>;
 
   /** Basic data that is shared with other checks */
   ExtState* d_data;
diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index 676390478..c80edbeb3 100644
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -39,7 +39,7 @@ class NlModel;
  */
 class IAndSolver
 {
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashSet<Node> NodeSet;
 
  public:
   IAndSolver(InferenceManager& im, ArithState& state, NlModel& model);
diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp
index 6e96cfe7b..9cd74883b 100644
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -67,7 +67,7 @@ inline std::ostream& operator<<(std::ostream& os, const IAWrapper& iaw)
 
 std::vector<Node> ICPSolver::collectVariables(const Node& n) const
 {
-  std::unordered_set<TNode, TNodeHashFunction> tmp;
+  std::unordered_set<TNode> tmp;
   expr::getVariables(n, tmp);
   std::vector<Node> res;
   for (const auto& t : tmp)
@@ -93,7 +93,7 @@ std::vector<Candidate> ICPSolver::constructCandidates(const Node& n)
   auto poly = std::get<0>(comp);
 
   std::vector<Candidate> result;
-  std::unordered_set<TNode, TNodeHashFunction> vars;
+  std::unordered_set<TNode> vars;
   expr::getVariables(n, vars);
   for (const auto& v : vars)
   {
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index 9b1246f67..ed4a5318f 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -242,7 +242,7 @@ bool NlModel::checkModel(const std::vector<Node>& assertions,
   // all remaining variables are constrained to their exact model values
   Trace("nl-ext-cm-debug") << "  set exact bounds for remaining variables..."
                            << std::endl;
-  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode> visited;
   std::vector<TNode> visit;
   TNode cur;
   for (const Node& a : assertions)
@@ -479,10 +479,10 @@ bool NlModel::solveEqualitySimple(Node eq,
   NodeManager* nm = NodeManager::currentNM();
   // the list of variables that occur as a monomial in msum, and whose value
   // is so far unconstrained in the model.
-  std::unordered_set<Node, NodeHashFunction> unc_vars;
+  std::unordered_set<Node> unc_vars;
   // the list of variables that occur as a factor in a monomial, and whose
   // value is so far unconstrained in the model.
-  std::unordered_set<Node, NodeHashFunction> unc_vars_factor;
+  std::unordered_set<Node> unc_vars_factor;
   for (std::pair<const Node, Node>& m : msum)
   {
     Node v = m.first;
@@ -797,7 +797,7 @@ bool NlModel::simpleCheckModelLit(Node lit)
   Trace("nl-ext-cms-debug")
       << "* Try univariate quadratic analysis..." << std::endl;
   std::vector<Node> vs_invalid;
-  std::unordered_set<Node, NodeHashFunction> vs;
+  std::unordered_set<Node> vs;
   std::map<Node, Node> v_a;
   std::map<Node, Node> v_b;
   // get coefficients...
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index 600dbd02c..acf5ee7f5 100644
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -322,7 +322,7 @@ class NlModel
    * These literals are exempt from check-model, since they are satisfied by
    * definition of our model construction.
    */
-  std::unordered_map<Node, Node, NodeHashFunction> d_check_model_solved;
+  std::unordered_map<Node, Node> d_check_model_solved;
   /** did we use an approximation on this call to last-call effort? */
   bool d_used_approx;
 }; /* class NlModel */
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index a3b32c6e9..8221e18d5 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -123,7 +123,7 @@ void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
 
   BoundInference bounds;
 
-  std::unordered_set<Node, NodeHashFunction> init_assertions;
+  std::unordered_set<Node> init_assertions;
 
   for (Theory::assertions_iterator it = d_containing.facts_begin();
        it != d_containing.facts_end();
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index e39f97402..4e029be7c 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -80,7 +80,7 @@ class NlLemma;
  */
 class NonlinearExtension
 {
-  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
+  typedef context::CDHashSet<Node> NodeSet;
 
  public:
   NonlinearExtension(TheoryArith& containing,
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index 62d101686..0d5e5ad04 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -291,8 +291,7 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d)
 
   // compute the concavity
   int region = -1;
-  std::unordered_map<Node, int, NodeHashFunction>::iterator itr =
-      d_tstate.d_tf_region.find(tf);
+  std::unordered_map<Node, int>::iterator itr = d_tstate.d_tf_region.find(tf);
   if (itr != d_tstate.d_tf_region.end())
   {
     region = itr->second;
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index f98986fad..74f005294 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -201,7 +201,7 @@ struct TranscendentalState
    * arguments that contain transcendental functions.
    */
   std::map<Node, Node> d_trMaster;
-  std::map<Node, std::unordered_set<Node, NodeHashFunction>> d_trSlaves;
+  std::map<Node, std::unordered_set<Node>> d_trSlaves;
 
   /** concavity region for transcendental functions
    *
@@ -223,7 +223,7 @@ struct TranscendentalState
    * of transcendental functions whose arguments have model
    * values that reside in valid regions.
    */
-  std::unordered_map<Node, int, NodeHashFunction> d_tf_region;
+  std::unordered_map<Node, int> d_tf_region;
   /**
    * Maps representives of a congruence class to the members of that class.
    *
@@ -253,9 +253,7 @@ struct TranscendentalState
    * each transcendental function application. We store this set for each
    * Taylor degree.
    */
-  std::unordered_map<Node,
-                     std::map<unsigned, std::vector<Node>>,
-                     NodeHashFunction>
+  std::unordered_map<Node, std::map<unsigned, std::vector<Node>>>
       d_secant_points;
 
   /** PI