diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-12-17 15:19:46 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-12-17 23:19:46 +0000 |
commit | d4f887d72b2bd48b2935838e2e0cf98ba049b96c (patch) | |
tree | 7aebad5efbac15c3391df86cf00c7694946866f4 | |
parent | c67bbf88a0da5c7c066de5ba9e31b58f00594b9b (diff) |
[Strings] Minor fixes/improvements (#7837)
This is a quick follow-up for PR #7815. My comments didn't make it in
before the PR was merged, so this commit fixes some of the minor issues
I found.
-rw-r--r-- | src/theory/strings/core_solver.cpp | 23 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 3 |
2 files changed, 3 insertions, 23 deletions
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index eb3c70a83..84fd3af71 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -102,27 +102,6 @@ void CoreSolver::debugPrintFlatForms( const char * tc ){ Trace( tc ) << std::endl; } -struct sortConstLength { - std::map< Node, unsigned > d_const_length; - bool operator() (Node i, Node j) { - std::map< Node, unsigned >::iterator it_i = d_const_length.find( i ); - std::map< Node, unsigned >::iterator it_j = d_const_length.find( j ); - if( it_i==d_const_length.end() ){ - if( it_j==d_const_length.end() ){ - return i<j; - }else{ - return false; - } - }else{ - if( it_j==d_const_length.end() ){ - return true; - }else{ - return it_i->second<it_j->second; - } - } - } -}; - void CoreSolver::checkCycles() { // first check for cycles, while building ordering of equivalence classes @@ -1988,7 +1967,7 @@ void CoreSolver::processDeq(Node ni, Node nj) { // If using the sequence update solver, we always apply extensionality. // This is required for model soundness currently, although we could - // investigate determine cases where the disequality is already + // investigate determining cases where the disequality is already // satisfied (for optimization). if (options().strings.seqArray != options::SeqArrayMode::NONE) { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4c60b5141..6f19a5aaf 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -268,7 +268,8 @@ struct SortSeqIndex { SortSeqIndex() {} /** the comparison */ - bool operator()(std::pair<Node, Node> i, std::pair<Node, Node> j) + bool operator()(const std::pair<Node, Node>& i, + const std::pair<Node, Node>& j) { Assert(i.first.isConst() && i.first.getType().isInteger() && j.first.isConst() && j.first.getType().isInteger()); |