From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 23 Nov 2020 22:09:20 +0000 (-0600)
Subject: Fix regular expression consume for nested star (#5518)
X-Git-Tag: cvc5-1.0.0~2556
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=07c7b873c5c2ee81cb2672428ca1de0d75bb1ae8;p=cvc5.git

Fix regular expression consume for nested star (#5518)

The issue was caused by simple regular expression consume being too aggressive when a recursive call was made to the method. In particular, we were assuming that the body of the star must be unrolled to fully consume a string, when it can be skipped if we are not at top level.

Fixes #5510.
---

diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp
index 0ab634c88..4a6df2fd8 100644
--- a/src/theory/strings/regexp_entail.cpp
+++ b/src/theory/strings/regexp_entail.cpp
@@ -252,9 +252,11 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
             {
               if (children_s.empty())
               {
-                // check if beyond this, we can't do it or there is nothing
-                // left, if so, repeat
-                bool can_skip = false;
+                // Check if beyond this, we hit a conflict. In this case, we
+                // must repeat.  Notice that we do not treat the case where
+                // there are no more strings to consume as a failure, since
+                // we may be within a recursive call, see issue #5510.
+                bool can_skip = true;
                 if (children.size() > 1)
                 {
                   std::vector<Node> mchildren_ss;
@@ -273,9 +275,9 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
                   Trace("regexp-ext-rewrite-debug") << push;
                   Node rets = simpleRegexpConsume(mchildren_ss, children_ss, t);
                   Trace("regexp-ext-rewrite-debug") << pop;
-                  if (rets.isNull())
+                  if (!rets.isNull())
                   {
-                    can_skip = true;
+                    can_skip = false;
                   }
                 }
                 if (!can_skip)
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1bf6c63f0..f66dc2d10 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1863,6 +1863,7 @@ set(regress_1_tests
   regress1/strings/issue5330_2.smt2
   regress1/strings/issue5374-proxy-i.smt2
   regress1/strings/issue5483-pp-leq.smt2
+  regress1/strings/issue5510-re-consume.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
diff --git a/test/regress/regress1/strings/issue5510-re-consume.smt2 b/test/regress/regress1/strings/issue5510-re-consume.smt2
new file mode 100644
index 000000000..3b7aaf344
--- /dev/null
+++ b/test/regress/regress1/strings/issue5510-re-consume.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic QF_S)
+(set-info :status sat)
+(declare-fun x () String)
+(declare-fun y () String)
+(assert (str.in_re (str.++ x "B" y) (re.* (re.++ (str.to_re "A") (re.union (re.* (str.to_re "A")) (str.to_re "B"))))))
+(assert (str.in_re y (str.to_re "A")))
+(check-sat)