1 files changed, 15 insertions, 18 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index 3c8320d8c..426ad07ef 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -38,8 +38,8 @@ void SygusInterpol::collectSymbols(const std::vector<Node>& axioms,
                                    const Node& conj)
 {
   Trace("sygus-interpol-debug") << "Collect symbols..." << std::endl;
-  std::unordered_set<Node, NodeHashFunction> symSetAxioms;
-  std::unordered_set<Node, NodeHashFunction> symSetConj;
+  std::unordered_set<Node> symSetAxioms;
+  std::unordered_set<Node> symSetConj;
   for (size_t i = 0, size = axioms.size(); i < size; i++)
   {
     expr::getSymbols(axioms[i], symSetAxioms);
@@ -96,7 +96,7 @@ void SygusInterpol::createVariables(bool needsShared)
 void SygusInterpol::getIncludeCons(
     const std::vector<Node>& axioms,
     const Node& conj,
-    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& result)
+    std::map<TypeNode, std::unordered_set<Node>>& result)
 {
   NodeManager* nm = NodeManager::currentNM();
   Assert(options::produceInterpols() != options::ProduceInterpols::NONE);
@@ -116,38 +116,35 @@ void SygusInterpol::getIncludeCons(
   else if (options::produceInterpols() == options::ProduceInterpols::SHARED)
   {
     // Get operators from axioms
-    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>
-        include_cons_axioms;
+    std::map<TypeNode, std::unordered_set<Node>> include_cons_axioms;
     Node tmpAssumptions =
         (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms));
     expr::getOperatorsMap(tmpAssumptions, include_cons_axioms);
 
     // Get operators from conj
-    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>
-        include_cons_conj;
+    std::map<TypeNode, std::unordered_set<Node>> include_cons_conj;
     expr::getOperatorsMap(conj, include_cons_conj);
 
     // Compute intersection
-    for (std::map<TypeNode,
-                  std::unordered_set<Node, NodeHashFunction>>::iterator it =
+    for (std::map<TypeNode, std::unordered_set<Node>>::iterator it =
              include_cons_axioms.begin();
          it != include_cons_axioms.end();
          it++)
     {
       TypeNode tn = it->first;
-      std::unordered_set<Node, NodeHashFunction> axiomsOps = it->second;
-      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator
-          concIter = include_cons_conj.find(tn);
+      std::unordered_set<Node> axiomsOps = it->second;
+      std::map<TypeNode, std::unordered_set<Node>>::iterator concIter =
+          include_cons_conj.find(tn);
       if (concIter != include_cons_conj.end())
       {
-        std::unordered_set<Node, NodeHashFunction> conjOps = concIter->second;
+        std::unordered_set<Node> conjOps = concIter->second;
         for (const Node& n : axiomsOps)
         {
           if (conjOps.find(n) != conjOps.end())
           {
             if (result.find(tn) == result.end())
             {
-              result[tn] = std::unordered_set<Node, NodeHashFunction>();
+              result[tn] = std::unordered_set<Node>();
             }
             result[tn].insert(n);
           }
@@ -184,11 +181,11 @@ TypeNode SygusInterpol::setSynthGrammar(const TypeNode& itpGType,
   else
   {
     // set default grammar
-    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons;
-    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> exclude_cons;
-    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> include_cons;
+    std::map<TypeNode, std::unordered_set<Node>> extra_cons;
+    std::map<TypeNode, std::unordered_set<Node>> exclude_cons;
+    std::map<TypeNode, std::unordered_set<Node>> include_cons;
     getIncludeCons(axioms, conj, include_cons);
-    std::unordered_set<Node, NodeHashFunction> terms_irrelevant;
+    std::unordered_set<Node> terms_irrelevant;
     itpGTypeS = CegGrammarConstructor::mkSygusDefaultType(
         NodeManager::currentNM()->booleanType(),
         d_ibvlShared,