diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 02c0c3130..06a39ec64 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -210,7 +210,7 @@ bool TheoryStrings::collectModelValues(TheoryModel* m, Trace("strings-debug-model") << d_esolver.debugPrintModel() << std::endl; } Trace("strings-model") << "TheoryStrings::collectModelValues" << std::endl; - std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > repSet; + std::map<TypeNode, std::unordered_set<Node> > repSet; // Generate model // get the relevant string equivalence classes for (const Node& s : termSet) @@ -222,9 +222,7 @@ bool TheoryStrings::collectModelValues(TheoryModel* m, repSet[tn].insert(r); } } - for (const std::pair<const TypeNode, - std::unordered_set<Node, NodeHashFunction> >& rst : - repSet) + for (const std::pair<const TypeNode, std::unordered_set<Node> >& rst : repSet) { // get partition of strings of equal lengths, per type std::map<TypeNode, std::vector<std::vector<Node> > > colT; @@ -241,12 +239,11 @@ bool TheoryStrings::collectModelValues(TheoryModel* m, return true; } -bool TheoryStrings::collectModelInfoType( - TypeNode tn, - const std::unordered_set<Node, NodeHashFunction>& repSet, - std::vector<std::vector<Node> >& col, - std::vector<Node>& lts, - TheoryModel* m) +bool TheoryStrings::collectModelInfoType(TypeNode tn, + const std::unordered_set<Node>& repSet, + std::vector<std::vector<Node> >& col, + std::vector<Node>& lts, + TheoryModel* m) { NodeManager* nm = NodeManager::currentNM(); std::map< Node, Node > processed; |