Stratify unfolding of regular expressions based on polarity (#3067)

1 files changed, 43 insertions, 15 deletions

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index f0e68890a..bf3a170df 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];
@@ -228,7 +240,16 @@ void RegExpSolver::check()
             break;
           }
         }
-
+        if (e == 1 && 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 (polarity)
         {
           flag = checkPDerivative(x, r, atom, addedLemma, rnfexp);
@@ -269,11 +290,18 @@ void RegExpSolver::check()
           {
             processed.push_back(assertion);
           }
+          if (e == 0)
+          {
+            // Remember that we have unfolded a membership for x
+            // notice that we only do this here, after we have definitely
+            // added a lemma.
+            repUnfold.insert(x);
+          }
+        }
+        if (d_parent.inConflict())
+        {
+          break;
         }
-      }
-      if (d_parent.inConflict())
-      {
-        break;
       }
     }
   }