From d4f887d72b2bd48b2935838e2e0cf98ba049b96c Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 17 Dec 2021 15:19:46 -0800
Subject: [PATCH] [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.
---
 src/theory/strings/core_solver.cpp    | 23 +----------------------
 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());
-- 
2.30.2