[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.

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index eb3c70a830d95e7516d5e1b70f91ad73ad659f9d..84fd3af717760a18c8768176d30eaa4d47c09ff3 100644 (file)
--- 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 4c60b5141bd39664f2dad1426470e6da26db68fb..6f19a5aaf35597d4017a5abcf9e766e6d159f978 100644 (file)
--- 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());