From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 19 Jul 2019 13:36:53 +0000 (-0400)
Subject: Fix case of unfolding negative membership in reg exp concatenation (#3101)
X-Git-Tag: cvc5-1.0.0~4087
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9fa66413709fbdb1a02f8986d0c332934523b110;p=cvc5.git

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 0360228c6..0d422e823 100644
--- 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 5079806ac..65d616c3c 100644
--- 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 aae919a2f..af6a9b839 100644
--- 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
index 000000000..3f99f8507
--- /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)