diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-23 16:09:20 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-23 16:09:20 -0600 |
| commit | 07c7b873c5c2ee81cb2672428ca1de0d75bb1ae8 (patch) | |
| tree | c89e29818dc79cd6cc37360f9ce71257520f5406 | |
| parent | a6c001e078767a2de6f36a2fa1333b98e39a6ec8 (diff) | |
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.
| -rw-r--r-- | src/theory/strings/regexp_entail.cpp | 12 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue5510-re-consume.smt2 | 9 |
3 files changed, 17 insertions, 5 deletions
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) |