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

diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index a0d806c527ca6edfb6beef1bc036e5740f8253b5..74981628073ccd8f36e5b050fb9ee8f1da5ccf01 100644 (file)
--- 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);
       }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 97b1fb99bb3e4396c2c64402f9de712db814e5b0..e0e57acf9bfd3673b2c8b9e2d4f5ae364a95526d 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1735,6 +1735,7 @@ set(regress_2_tests
   regress2/strings/repl-repl.smt2
   regress2/strings/replaceall-diffrange.smt2
   regress2/strings/replaceall-len-c.smt2
+  regress2/strings/small-1.smt2
   regress2/sygus/MPwL_d1s3.sy
   regress2/sygus/array_sum_dd.sy
   regress2/sygus/cegisunif-depth1-bv.sy

diff --git a/test/regress/regress2/strings/small-1.smt2 b/test/regress/regress2/strings/small-1.smt2
new file mode 100644 (file)
index 0000000..9fc2c9f
--- /dev/null
+++ b/test/regress/regress2/strings/small-1.smt2
@@ -0,0 +1,8 @@
+(set-info :smt-lib-version 2.5)
+(set-logic ALL)
+(set-info :status sat)
+(set-option :strings-exp true)
+(set-option :re-elim true)
+(declare-const x String)
+(assert (str.in.re x (re.++ (str.to.re "example-bucket/") (re.* re.allchar) (str.to.re "/") re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar (str.to.re "-") re.allchar re.allchar re.allchar re.allchar (str.to.re "-") re.allchar re.allchar re.allchar re.allchar (str.to.re "-") re.allchar re.allchar re.allchar re.allchar (str.to.re "-") re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar re.allchar (str.to.re "/foo"))))
+(check-sat)