Optimize re-elim for re.allchar components (#2725)

1 files changed, 8 insertions, 2 deletions

diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index a0d806c52..749816280 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -110,8 +110,14 @@ Node RegExpElimination::eliminateConcat(Node atom)
       else
       {
         Node curr = nm->mkNode(STRING_SUBSTR, x, currEnd, childLengths[i]);
-        Node currMem = nm->mkNode(STRING_IN_REGEXP, curr, re[i]);
-        conc.push_back(currMem);
+        // We do not need to include memberships of the form
+        //   (str.substr x n 1) in re.allchar
+        // since we know that by construction, n < len( x ).
+        if (re[i].getKind() != REGEXP_SIGMA)
+        {
+          Node currMem = nm->mkNode(STRING_IN_REGEXP, curr, re[i]);
+          conc.push_back(currMem);
+        }
         currEnd = nm->mkNode(PLUS, currEnd, childLengths[i]);
         currEnd = Rewriter::rewrite(currEnd);
       }