diff options
Diffstat (limited to 'src/theory/subs_minimize.cpp')
-rw-r--r-- | src/theory/subs_minimize.cpp | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp index b58ffad33..e2a81f54a 100644 --- a/src/theory/subs_minimize.cpp +++ b/src/theory/subs_minimize.cpp @@ -73,9 +73,9 @@ bool SubstitutionMinimize::findWithImplied(Node t, std::vector<Node> tconj; getConjuncts(t, tconj); // map from conjuncts to their free symbols - std::map<Node, std::unordered_set<Node, NodeHashFunction> > tcFv; + std::map<Node, std::unordered_set<Node> > tcFv; - std::unordered_set<Node, NodeHashFunction> reqSet; + std::unordered_set<Node> reqSet; std::vector<Node> reqSubs; std::map<Node, unsigned> reqVarToIndex; for (const Node& v : reqVars) @@ -104,8 +104,7 @@ bool SubstitutionMinimize::findWithImplied(Node t, for (const Node& tc : tconj) { // ensure we've computed its free symbols - std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator - itf = tcFv.find(tc); + std::map<Node, std::unordered_set<Node> >::iterator itf = tcFv.find(tc); if (itf == tcFv.end()) { expr::getSymbols(tc, tcFv[tc]); @@ -181,8 +180,8 @@ bool SubstitutionMinimize::findInternal(Node n, Trace("subs-min") << "--- Compute values for subterms..." << std::endl; // the value of each subterm in n under the substitution - std::unordered_map<TNode, Node, TNodeHashFunction> value; - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::unordered_map<TNode, Node> value; + std::unordered_map<TNode, Node>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(n); @@ -262,12 +261,12 @@ bool SubstitutionMinimize::findInternal(Node n, } Trace("subs-min") << "--- Compute relevant variables..." << std::endl; - std::unordered_set<Node, NodeHashFunction> rlvFv; + std::unordered_set<Node> rlvFv; // only variables that occur in assertions are relevant visit.push_back(n); - std::unordered_set<TNode, TNodeHashFunction> visited; - std::unordered_set<TNode, TNodeHashFunction>::iterator itv; + std::unordered_set<TNode> visited; + std::unordered_set<TNode>::iterator itv; do { cur = visit.back(); |