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

Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.

4 files changed, 26 insertions, 26 deletions

diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp
index 6b8c27c17..e96d3ec9e 100644
--- a/test/unit/node/node_algorithm_black.cpp
+++ b/test/unit/node/node_algorithm_black.cpp
@@ -40,7 +40,7 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_symbols1)
   // The only symbol in ~x (x is a boolean varible) should be x
   Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
   Node n = d_nodeManager->mkNode(NOT, x);
-  std::unordered_set<Node, NodeHashFunction> syms;
+  std::unordered_set<Node> syms;
   getSymbols(n, syms);
   ASSERT_EQ(syms.size(), 1);
   ASSERT_NE(syms.find(x), syms.end());
@@ -69,7 +69,7 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2)
   Node res = d_nodeManager->mkNode(AND, left, right);
 
   // symbols
-  std::unordered_set<Node, NodeHashFunction> syms;
+  std::unordered_set<Node> syms;
   getSymbols(res, syms);
 
   // assertions
@@ -82,8 +82,8 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2)
 TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map)
 {
   // map to store result
-  std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > result =
-      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> >();
+  std::map<TypeNode, std::unordered_set<Node> > result =
+      std::map<TypeNode, std::unordered_set<Node> >();
 
   // create test formula
   Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType());
@@ -146,7 +146,7 @@ TEST_F(TestNodeBlackNodeAlgorithm, match)
   Node a = d_skolemManager->mkDummySkolem("a", integer);
 
   Node n1 = d_nodeManager->mkNode(MULT, two, x);
-  std::unordered_map<Node, Node, NodeHashFunction> subs;
+  std::unordered_map<Node, Node> subs;
 
   // check reflexivity
   ASSERT_TRUE(match(n1, n1, subs));
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index 5905f8404..839b516e4 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -924,7 +924,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique1)
       d_two);
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
   ASSERT_EQ(res.size(), 3);
@@ -1030,7 +1030,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2)
       d_two);
 
   std::vector<Node> eqs = {eq1, eq2, eq3};
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   BVGauss::Result ret = BVGauss::gaussElimRewriteForUrem(eqs, res);
   ASSERT_EQ(ret, BVGauss::Result::UNIQUE);
   ASSERT_EQ(res.size(), 3);
@@ -1041,7 +1041,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2)
 
 TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a)
 {
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   BVGauss::Result ret;
 
   /* -------------------------------------------------------------------
@@ -1167,7 +1167,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1a)
 
 TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b)
 {
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   BVGauss::Result ret;
 
   /* -------------------------------------------------------------------
@@ -1291,7 +1291,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial1b)
 
 TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial2)
 {
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   BVGauss::Result ret;
 
   /* -------------------------------------------------------------------
@@ -1380,7 +1380,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial2)
 
 TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial3)
 {
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   BVGauss::Result ret;
 
   /* -------------------------------------------------------------------
@@ -1509,7 +1509,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial3)
 
 TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4)
 {
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   BVGauss::Result ret;
 
   /* -------------------------------------------------------------------
@@ -1660,7 +1660,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial4)
 
 TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial5)
 {
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   BVGauss::Result ret;
 
   /* -------------------------------------------------------------------
@@ -1772,7 +1772,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial5)
 
 TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6)
 {
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   BVGauss::Result ret;
 
   /* -------------------------------------------------------------------
@@ -1860,7 +1860,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_partial6)
 
 TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial)
 {
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   BVGauss::Result ret;
 
   /* -------------------------------------------------------------------
@@ -2011,7 +2011,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_with_expr_partial)
 
 TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
 {
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   BVGauss::Result ret;
 
   /* -------------------------------------------------------------------
@@ -2182,7 +2182,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
 
 TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid1)
 {
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   BVGauss::Result ret;
 
   /* -------------------------------------------------------------------
@@ -2230,7 +2230,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid1)
 
 TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid2)
 {
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   BVGauss::Result ret;
 
   /* -------------------------------------------------------------------
@@ -2301,7 +2301,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid2)
 
 TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_invalid)
 {
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   BVGauss::Result ret;
 
   /* -------------------------------------------------------------------
@@ -2401,7 +2401,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique1)
   AssertionPipeline apipe;
   apipe.push_back(a);
   passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
   ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
   Node resx = d_nodeManager->mkNode(
@@ -2490,7 +2490,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_unique2)
   apipe.push_back(eq4);
   apipe.push_back(eq5);
   passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
   ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
   Node resx1 = d_nodeManager->mkNode(
@@ -2542,7 +2542,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_partial)
   apipe.push_back(eq1);
   apipe.push_back(eq2);
   passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
-  std::unordered_map<Node, Node, NodeHashFunction> res;
+  std::unordered_map<Node, Node> res;
   PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
   ASSERT_EQ(pres, PreprocessingPassResult::NO_CONFLICT);
   ASSERT_EQ(apipe.size(), 4);
diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
index 211552590..85f14b245 100644
--- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
+++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
@@ -113,7 +113,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvMult)
   Node zero = mkZero(32);
   Node one = mkOne(32);
   BvLinearAttribute is_linear;
-  std::unordered_map<Node, bool, NodeHashFunction> contains_x;
+  std::unordered_map<Node, bool> contains_x;
 
   contains_x[x] = true;
   contains_x[neg_x] = true;
@@ -211,7 +211,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvPlus)
   Node c = mkVar(32);
   Node d = mkVar(32);
   BvLinearAttribute is_linear;
-  std::unordered_map<Node, bool, NodeHashFunction> contains_x;
+  std::unordered_map<Node, bool> contains_x;
 
   contains_x[x] = true;
   contains_x[neg_x] = true;
@@ -334,7 +334,7 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvEqual)
   Node one = mkOne(32);
   Node ntrue = mkTrue();
   BvLinearAttribute is_linear;
-  std::unordered_map<Node, bool, NodeHashFunction> contains_x;
+  std::unordered_map<Node, bool> contains_x;
 
   contains_x[x] = true;
   contains_x[neg_x] = true;
diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp
index ab77a74ce..baf3af40e 100644
--- a/test/unit/theory/type_enumerator_white.cpp
+++ b/test/unit/theory/type_enumerator_white.cpp
@@ -248,7 +248,7 @@ TEST_F(TestTheoryWhiteTypeEnumerator, arrays_infinite)
 {
   TypeEnumerator te(d_nodeManager->mkArrayType(d_nodeManager->integerType(),
                                                d_nodeManager->integerType()));
-  std::unordered_set<Node, NodeHashFunction> elts;
+  std::unordered_set<Node> elts;
   for (uint32_t i = 0; i < 1000; ++i)
   {
     ASSERT_FALSE(te.isFinished());