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.

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 39bcb8f536c019f3c49cc2305a109db5b2b48763..fd50e78eeea2ebc8664999eaafab12fe7a2d9332 100644 (file)
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -85,7 +85,7 @@ bool ExtfSolver::doReduction(int effort, Node n)
   if (d_reduced.find(n)!=d_reduced.end())
   {
     // already sent a reduction lemma
-  Trace("strings-extf-debug") << "...skip due to reduced" << std::endl;
+    Trace("strings-extf-debug") << "...skip due to reduced" << std::endl;
     return false;
   }
   // determine the effort level to process the extf at
@@ -157,8 +157,7 @@ bool ExtfSolver::doReduction(int effort, Node n)
   }
   if (effort != r_effort)
   {
-    
-  Trace("strings-extf-debug") << "...skip due to effort" << std::endl;
+    Trace("strings-extf-debug") << "...skip due to effort" << std::endl;
     // not the right effort level to reduce
     return false;
   }
@@ -722,6 +721,32 @@ bool StringsExtfCallback::getCurrentSubstitution(
   return true;
 }
 
+std::string ExtfSolver::debugPrintModel()
+{
+  std::stringstream ss;
+  std::vector<Node> extf;
+  d_extt.getTerms(extf);
+  // each extended function should have at least one annotation below
+  for (const Node& n : extf)
+  {
+    ss << "- " << n;
+    if (!d_extt.isActive(n))
+    {
+      ss << " :extt-inactive";
+    }
+    if (!d_extfInfoTmp[n].d_modelActive)
+    {
+      ss << " :model-inactive";
+    }
+    if (d_reduced.find(n) != d_reduced.end())
+    {
+      ss << " :reduced";
+    }
+    ss << std::endl;
+  }
+  return ss.str();
+}
+
 }  // namespace strings
 }  // namespace theory
 }  // namespace cvc5

diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h
index 3cfe2309c7a47e41a3de1ac6b3ffe9675dc70706..bbc32e7a229a3134ea5dc14cdf7af634aa25291d 100644 (file)
--- a/src/theory/strings/extf_solver.h
+++ b/src/theory/strings/extf_solver.h
@@ -153,6 +153,12 @@ class ExtfSolver
    */
   std::vector<Node> getActive(Kind k) const;
   //---------------------------------- end information about ExtTheory
+  /**
+   * Print the relevant information regarding why we have a model, return as a
+   * string.
+   */
+  std::string debugPrintModel();
+
  private:
   /** do reduction
    *

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 2d4404c10f887b9dd6275d3355de6d0286df8b48..7737a90f7d43be3bd1d937d6d84800cff2f815cb 100644 (file)
--- 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]);
-      }
     }
   }
 }

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 5bd92267ecf48242159d49249950c80505389612..f2f584da7d1cbf1ef6bb18f22e39294c6b6c8b50 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -203,13 +203,16 @@ void TheoryStrings::presolve() {
 bool TheoryStrings::collectModelValues(TheoryModel* m,
                                        const std::set<Node>& termSet)
 {
-  if (Trace.isOn("strings-model"))
+  if (Trace.isOn("strings-debug-model"))
   {
-    Trace("strings-model") << "TheoryStrings : Collect model values"
-                           << std::endl;
-    Trace("strings-model") << "Equivalence classes are:" << std::endl;
-    Trace("strings-model") << debugPrintStringsEqc() << std::endl;
+    Trace("strings-debug-model")
+        << "TheoryStrings::collectModelValues" << std::endl;
+    Trace("strings-debug-model") << "Equivalence classes are:" << std::endl;
+    Trace("strings-debug-model") << debugPrintStringsEqc() << std::endl;
+    Trace("strings-debug-model") << "Extended functions are:" << std::endl;
+    Trace("strings-debug-model") << d_esolver.debugPrintModel() << std::endl;
   }
+  Trace("strings-model") << "TheoryStrings::collectModelValues" << std::endl;
   std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > repSet;
   // Generate model
   // get the relevant string equivalence classes

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 232a7f7ab6051e993dcb1000c2aa8b30e2cf376d..64c584f7a4f631e6e1602430d20d1151437c5c61 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2040,6 +2040,7 @@ set(regress_1_tests
   regress1/strings/issue6132-non-unique-skolem.smt2
   regress1/strings/issue6142-repl-inv-rew.smt2
   regress1/strings/issue6191-replace-all.smt2
+  regress1/strings/issue6203-2-re-ccache.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/regress1/strings/issue6203-2-re-ccache.smt2 b/test/regress/regress1/strings/issue6203-2-re-ccache.smt2
new file mode 100644 (file)
index 0000000..2deffda
--- /dev/null
+++ b/test/regress/regress1/strings/issue6203-2-re-ccache.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () String)
+(assert
+ (xor (str.in_re a (re.++ (re.* re.allchar) (str.to_re "A") re.allchar (re.* re.allchar)))
+ (str.in_re a (re.++ (re.* (str.to_re a)) (str.to_re "A") re.allchar))))
+(check-sat)