From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 31 Aug 2021 14:07:48 +0000 (-0500)
Subject: Fix normal forms context-dependent simplification for strings (#7090)
X-Git-Tag: cvc5-1.0.0~1315
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=54991eb9fa2e21c8c4705c5522ad99a9ccd9b41b;p=cvc5.git

Fix normal forms context-dependent simplification for strings (#7090)

This corrects an issue in our context-dependent simplification which limited the cases it was applied.

Previously, we were using a best content heuristic when it was applicable to compute the substitution, even if we were in an effort where normal forms had been computed. The latter should always be used if possible, since normal forms always have at least as much or more concrete components.
---

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index b25f8f021..5e685576c 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -358,59 +358,53 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
         }
         Trace("strings-debug") << std::endl;
       }
-      size_t count = 0;
       size_t countc = 0;
       std::vector<Node> exp;
       // non-constant vector
       std::vector<Node> vecnc;
       size_t contentSize = 0;
-      while (count < n.getNumChildren())
+      for (size_t count = 0, nchild = n.getNumChildren(); count < nchild;
+           ++count)
       {
         // Add explanations for the empty children
         Node emps;
-        while (count < n.getNumChildren()
-               && d_state.isEqualEmptyWord(n[count], emps))
+        if (d_state.isEqualEmptyWord(n[count], emps))
         {
           d_im.addToExplanation(n[count], emps, exp);
-          count++;
+          continue;
         }
-        if (count < n.getNumChildren())
+        else if (vecc[countc].isNull())
         {
-          if (vecc[countc].isNull())
-          {
-            Assert(!isConst);
-            // no constant for this component, leave it as is
-            vecnc.push_back(n[count]);
-          }
-          else
-          {
-            if (!isConst)
-            {
-              // use the constant
-              vecnc.push_back(vecc[countc]);
-              Assert(vecc[countc].isConst());
-              contentSize += Word::getLength(vecc[countc]);
-            }
-            Trace("strings-debug") << "...explain " << n[count] << " "
-                                   << vecc[countc] << std::endl;
-            if (!d_state.areEqual(n[count], vecc[countc]))
-            {
-              Node nrr = d_state.getRepresentative(n[count]);
-              Assert(!d_eqcInfo[nrr].d_bestContent.isNull()
-                     && d_eqcInfo[nrr].d_bestContent.isConst());
-              // must flatten to avoid nested AND in explanations
-              utils::flattenOp(AND, d_eqcInfo[nrr].d_exp, exp);
-              // now explain equality to base
-              d_im.addToExplanation(n[count], d_eqcInfo[nrr].d_base, exp);
-            }
-            else
-            {
-              d_im.addToExplanation(n[count], vecc[countc], exp);
-            }
-            countc++;
-          }
-          count++;
+          Assert(!isConst);
+          // no constant for this component, leave it as is
+          vecnc.push_back(n[count]);
+          continue;
+        }
+        // if we are not entirely a constant
+        if (!isConst)
+        {
+          // use the constant component
+          vecnc.push_back(vecc[countc]);
+          Assert(vecc[countc].isConst());
+          contentSize += Word::getLength(vecc[countc]);
+        }
+        Trace("strings-debug")
+            << "...explain " << n[count] << " " << vecc[countc] << std::endl;
+        if (!d_state.areEqual(n[count], vecc[countc]))
+        {
+          Node nrr = d_state.getRepresentative(n[count]);
+          Assert(!d_eqcInfo[nrr].d_bestContent.isNull()
+                 && d_eqcInfo[nrr].d_bestContent.isConst());
+          // must flatten to avoid nested AND in explanations
+          utils::flattenOp(AND, d_eqcInfo[nrr].d_exp, exp);
+          // now explain equality to base
+          d_im.addToExplanation(n[count], d_eqcInfo[nrr].d_base, exp);
+        }
+        else
+        {
+          d_im.addToExplanation(n[count], vecc[countc], exp);
         }
+        countc++;
       }
       // exp contains an explanation of n==c
       Assert(!isConst || countc == vecc.size());
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 32726f4ae..d5b1b7088 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -678,12 +678,8 @@ Node ExtfSolver::getCurrentSubstitutionFor(int effort,
     return mv;
   }
   Node nr = d_state.getRepresentative(n);
-  Node c = d_bsolver.explainBestContentEqc(n, nr, exp);
-  if (!c.isNull())
-  {
-    return c;
-  }
-  else if (effort >= 1 && n.getType().isStringLike())
+  // if the normal form is available, use it
+  if (effort >= 1 && n.getType().isStringLike())
   {
     Assert(effort < 3);
     // normal forms
@@ -697,6 +693,12 @@ Node ExtfSolver::getCurrentSubstitutionFor(int effort,
     }
     return ns;
   }
+  // otherwise, we use the best content heuristic
+  Node c = d_bsolver.explainBestContentEqc(n, nr, exp);
+  if (!c.isNull())
+  {
+    return c;
+  }
   return n;
 }