Fix case of unfolding negative membership in reg exp concatenation (#3101)

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 0360228c67712ed421d634d615021e6f15720366..0d422e823d5022e00fa7c2432edfdcea01118da8 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -850,14 +850,18 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes
         {
           b1 = reLength;
         }
-        Node s1 = nm->mkNode(STRING_SUBSTR, s, d_zero, b1);
-        Node s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(MINUS, lens, b1));
-        if (indexRm != 0)
+        Node s1;
+        Node s2;
+        if (indexRm == 0)
         {
-          // swap if we are removing from the end
-          Node sswap = s1;
-          s1 = s2;
-          s2 = sswap;
+          s1 = nm->mkNode(STRING_SUBSTR, s, d_zero, b1);
+          s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(MINUS, lens, b1));
+        }
+        else
+        {
+          s1 = nm->mkNode(STRING_SUBSTR, s, nm->mkNode(MINUS, lens, b1), b1);
+          s2 =
+              nm->mkNode(STRING_SUBSTR, s, d_zero, nm->mkNode(MINUS, lens, b1));
         }
         Node s1r1 = nm->mkNode(STRING_IN_REGEXP, s1, r[indexRm]).negate();
         std::vector<Node> nvec;

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 5079806ac78d220d672591c89acb6c9415cd7f69..65d616c3cd0b974b0a2a52810b8ea857af3f89af 100644 (file)
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -281,7 +281,6 @@ void RegExpSolver::check()
           std::vector<Node> exp_n;
           exp_n.push_back(assertion);
           Node conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(AND, nvec);
-          conc = Rewriter::rewrite(conc);
           d_im.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold");
           addedLemma = true;
           if (changed)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index aae919a2f5b5a5e638bc397892228623f321c2c2..af6a9b839f8f160e41dd7a2da5917860a3de4ba8 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1580,6 +1580,7 @@ set(regress_1_tests
   regress1/strings/re-agg-total2.smt2
   regress1/strings/re-elim-exact.smt2
   regress1/strings/re-neg-concat-reduct.smt2
+  regress1/strings/re-neg-unfold-rev-a.smt2
   regress1/strings/re-unsound-080718.smt2
   regress1/strings/regexp001.smt2
   regress1/strings/regexp002.smt2

diff --git a/test/regress/regress1/strings/re-neg-unfold-rev-a.smt2 b/test/regress/regress1/strings/re-neg-unfold-rev-a.smt2
new file mode 100644 (file)
index 0000000..3f99f85
--- /dev/null
+++ b/test/regress/regress1/strings/re-neg-unfold-rev-a.smt2
@@ -0,0 +1,10 @@
+(set-info :smt-lib-version 2.5)
+(set-logic QF_S)
+(set-info :status unsat)
+(set-option :strings-exp true)
+
+(declare-const x String)
+(declare-const y String)
+(assert (and (= y "foobar") (str.in.re x (re.++ (str.to.re "ab") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b")))))
+(assert (not (and (= y "foobar") (str.in.re x (re.++ (str.to.re "a") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b"))))))
+(check-sat)