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

4 files changed, 55 insertions, 19 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;
       }
     }
   }
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index cea3c3515..7b6bbdc99 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -4023,10 +4023,9 @@ void TheoryStrings::registerTerm( Node n, int effort ) {
   else if (n.getKind() == STRING_STRIDOF)
   {
     Node len = mkLength(n[0]);
-    Node lem = nm->mkNode(
-        AND,
-        nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))),
-        nm->mkNode(LT, n, len));
+    Node lem = nm->mkNode(AND,
+                          nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))),
+                          nm->mkNode(LT, n, len));
     d_out->lemma(lem);
   }
 }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f3abe2c87..3c5d82fa8 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1580,6 +1580,7 @@ set(regress_1_tests
   regress1/strings/regexp001.smt2
   regress1/strings/regexp002.smt2
   regress1/strings/regexp003.smt2
+  regress1/strings/regexp-strat-fix.smt2
   regress1/strings/reloop.smt2
   regress1/strings/repl-empty-sem.smt2
   regress1/strings/repl-soundness-sem.smt2
diff --git a/test/regress/regress1/strings/regexp-strat-fix.smt2 b/test/regress/regress1/strings/regexp-strat-fix.smt2
new file mode 100644
index 000000000..9ff78c935
--- /dev/null
+++ b/test/regress/regress1/strings/regexp-strat-fix.smt2
@@ -0,0 +1,8 @@
+(set-info :smt-lib-version 2.5)
+(set-logic QF_S)
+(set-info :status unsat)
+(set-option :strings-exp true)
+(declare-fun var0 () String)
+(assert (str.in.re var0 (re.* (re.* (str.to.re "0")))))
+(assert (not (str.in.re var0 (re.union (re.+ (str.to.re "0")) (re.* (str.to.re "1"))))))
+(check-sat)