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 0ab634c884f003c00be2ddd43412a8d5b34066c9..4a6df2fd82d67d88fd684d3429bcb39f92493376 100644 (file)
--- 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 1bf6c63f06f27b54256f7510dedc0d5f45766074..f66dc2d10fde9f074c58bd76f3828c1dbe240d79 100644 (file)
--- 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 (file)
index 0000000..3b7aaf3
--- /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)