Stratify unfolding of regular expressions based on polarity

1 files changed, 41 insertions, 14 deletions

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index f0e68890a..97fec0340 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -172,23 +172,35 @@ void RegExpSolver::check()
   if (!addedLemma)
   {
     NodeManager* nm = NodeManager::currentNM();
-    for (unsigned i = 0; i < d_regexp_memberships.size(); i++)
+    // representatives of strings that are the LHS of positive memberships that
+    // we unfolded
+    std::unordered_set<Node, NodeHashFunction> repUnfold;
+    // check positive (e=0), then negative (e=1) memberships
+    for (unsigned e = 0; e < 2; e++)
     {
-      // check regular expression membership
-      Node assertion = d_regexp_memberships[i];
-      Trace("regexp-debug")
-          << "Check : " << assertion << " "
-          << (d_regexp_ucached.find(assertion) == d_regexp_ucached.end()) << " "
-          << (d_regexp_ccached.find(assertion) == d_regexp_ccached.end())
-          << std::endl;
-      if (d_regexp_ucached.find(assertion) == d_regexp_ucached.end()
-          && d_regexp_ccached.find(assertion) == d_regexp_ccached.end())
+      for (const Node& assertion : d_regexp_memberships)
       {
+        // check regular expression membership
+        Trace("regexp-debug")
+            << "Check : " << assertion << " "
+            << (d_regexp_ucached.find(assertion) == d_regexp_ucached.end())
+            << " "
+            << (d_regexp_ccached.find(assertion) == d_regexp_ccached.end())
+            << std::endl;
+        if (d_regexp_ucached.find(assertion) != d_regexp_ucached.end()
+            || d_regexp_ccached.find(assertion) != d_regexp_ccached.end())
+        {
+          continue;
+        }
         Trace("strings-regexp")
             << "We have regular expression assertion : " << assertion
             << std::endl;
         Node atom = assertion.getKind() == NOT ? assertion[0] : assertion;
         bool polarity = assertion.getKind() != NOT;
+        if (polarity != (e == 0))
+        {
+          continue;
+        }
         bool flag = true;
         Node x = atom[0];
         Node r = atom[1];
@@ -206,6 +218,21 @@ void RegExpSolver::check()
         }
         Trace("strings-regexp-nf") << "Term " << atom << " is normalized to "
                                    << x << " IN " << r << std::endl;
+        if (e == 0)
+        {
+          // remember that we have unfolded a membership for x
+          repUnfold.insert(x);
+        }
+        else if (repUnfold.find(x) != repUnfold.end())
+        {
+          // do not unfold negative memberships of strings that have new
+          // positive unfoldings. For example:
+          //   x in ("A")* ^ NOT x in ("B")*
+          // We unfold x = "A" ++ x' only. The intution here is that positive
+          // unfoldings lead to stronger constraints (equalities are stronger
+          // than disequalities), and are easier to check.
+          continue;
+        }
         if (changed)
         {
           Node tmp = Rewriter::rewrite(nm->mkNode(STRING_IN_REGEXP, x, r));
@@ -270,10 +297,10 @@ void RegExpSolver::check()
             processed.push_back(assertion);
           }
         }
-      }
-      if (d_parent.inConflict())
-      {
-        break;
+        if (d_parent.inConflict())
+        {
+          break;
+        }
       }
     }
   }