Optimization for strings normalize disequalities (#3047)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 1947f173013c3829a123e4ba406e3ba525384af6..67f0321938cb54259c3a3554e7f3826b73c4c733 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -4468,19 +4468,29 @@ void TheoryStrings::checkNormalFormsDeq()
         for( unsigned j=0; j<cols[i].size(); j++ ){
           for( unsigned k=(j+1); k<cols[i].size(); k++ ){
             //for strings that are disequal, but have the same length
-            if( areDisequal( cols[i][j], cols[i][k] ) ){
-              Assert( !d_conflict );
-              if (Trace.isOn("strings-solve"))
+            if (cols[i][j].isConst() && cols[i][k].isConst())
+            {
+              // if both are constants, they should be distinct, and its trivial
+              Assert(cols[i][j] != cols[i][k]);
+            }
+            else
+            {
+              if (areDisequal(cols[i][j], cols[i][k]))
               {
-                Trace("strings-solve") << "- Compare " << cols[i][j] << " ";
-                printConcat(getNormalForm(cols[i][j]).d_nf, "strings-solve");
-                Trace("strings-solve") << " against " << cols[i][k] << " ";
-                printConcat(getNormalForm(cols[i][k]).d_nf, "strings-solve");
-                Trace("strings-solve") << "..." << std::endl;
-              }
-              processDeq( cols[i][j], cols[i][k] );
-              if( hasProcessed() ){
-                return;
+                Assert(!d_conflict);
+                if (Trace.isOn("strings-solve"))
+                {
+                  Trace("strings-solve") << "- Compare " << cols[i][j] << " ";
+                  printConcat(getNormalForm(cols[i][j]).d_nf, "strings-solve");
+                  Trace("strings-solve") << " against " << cols[i][k] << " ";
+                  printConcat(getNormalForm(cols[i][k]).d_nf, "strings-solve");
+                  Trace("strings-solve") << "..." << std::endl;
+                }
+                processDeq(cols[i][j], cols[i][k]);
+                if (hasProcessed())
+                {
+                  return;
+                }
               }
             }
           }