Simplify caching of regular expression unfolding (#6262)

This ensures that we always cache regular expressions in a user-dependent manner. Previously, we were erroneously caching in a SAT-dependent way for very rare cases when non-constant regular expressions were used. Since we never dependent on current assertions for the unfolding, there is no need to cache in the SAT context.

This fixes the second benchmark from #6203.

This PR also improves our traces for checking models in strings.

1 files changed, 1 insertions, 15 deletions

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 2d4404c10..7737a90f7 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -96,7 +96,6 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
   bool addedLemma = false;
   bool changed = false;
   std::vector<Node> processed;
-  std::vector<Node> cprocessed;
 
   Trace("regexp-process") << "Checking Memberships ... " << std::endl;
   for (const std::pair<const Node, std::vector<Node> >& mr : mems)
@@ -287,14 +286,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
                 polarity ? InferenceId::STRINGS_RE_UNFOLD_POS : InferenceId::STRINGS_RE_UNFOLD_NEG;
             d_im.sendInference(iexp, noExplain, conc, inf);
             addedLemma = true;
-            if (changed)
-            {
-              cprocessed.push_back(assertion);
-            }
-            else
-            {
-              processed.push_back(assertion);
-            }
+            processed.push_back(assertion);
             if (e == 0)
             {
               // Remember that we have unfolded a membership for x
@@ -326,12 +318,6 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
             << "...add " << processed[i] << " to u-cache." << std::endl;
         d_regexp_ucached.insert(processed[i]);
       }
-      for (unsigned i = 0; i < cprocessed.size(); i++)
-      {
-        Trace("strings-regexp")
-            << "...add " << cprocessed[i] << " to c-cache." << std::endl;
-        d_regexp_ccached.insert(cprocessed[i]);
-      }
     }
   }
 }