From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 28 Nov 2018 20:58:33 +0000 (-0600)
Subject: Optimize re-elim for re.allchar components (#2725)
X-Git-Tag: cvc5-1.0.0~4345
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c92e6e49040b3ca4c33fbedb8e2a30ac3318fb8d;p=cvc5.git

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 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);
       }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 97b1fb99b..e0e57acf9 100644
--- 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
index 000000000..9fc2c9f9e
--- /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)