From 46591b1c92fc9ecd4a0997242030a1a48166301b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 28 Jun 2020 08:34:44 -0500 Subject: Fix non-termination issues in simpleRegExpConsume (#4667) There were two issues related to RE in bodies of re.* that accepted the empty string that led to non-termination in the rewriter for regular expressions. This also improves trace messages for simpleRegExpConsume. Fixes #4662. --- test/regress/regress0/strings/issue4662-consume-nterm.smt2 | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 test/regress/regress0/strings/issue4662-consume-nterm.smt2 (limited to 'test/regress/regress0/strings') diff --git a/test/regress/regress0/strings/issue4662-consume-nterm.smt2 b/test/regress/regress0/strings/issue4662-consume-nterm.smt2 new file mode 100644 index 000000000..a87279b4c --- /dev/null +++ b/test/regress/regress0/strings/issue4662-consume-nterm.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_S) +(set-info :status unsat) +(declare-fun a () String) +(define-fun b () RegLan (str.to_re "A")) +(assert (str.in_re (str.++ "B" a) (re.+ (re.++ (re.opt b) (re.opt b))))) +(check-sat) -- cgit v1.2.3 From ffed5a43764641d4808aa77bb0e393623fd4442d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 30 Jun 2020 18:08:54 -0500 Subject: Fix normal form for re.comp (#4676) Fixes #4674. --- src/theory/strings/regexp_solver.cpp | 1 + test/regress/CMakeLists.txt | 1 + test/regress/regress0/strings/issue4674-recomp-nf.smt2 | 5 +++++ 3 files changed, 7 insertions(+) create mode 100644 test/regress/regress0/strings/issue4674-recomp-nf.smt2 (limited to 'test/regress/regress0/strings') diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 627258a4c..53c6c9acc 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -672,6 +672,7 @@ Node RegExpSolver::getNormalSymRegExp(Node r, std::vector& nf_exp) case REGEXP_UNION: case REGEXP_INTER: case REGEXP_STAR: + case REGEXP_COMPLEMENT: { std::vector vec_nodes; for (const Node& cr : r) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9a58457e6..10e2f414e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -967,6 +967,7 @@ set(regress_0_tests regress0/strings/issue4070.smt2 regress0/strings/issue4376.smt2 regress0/strings/issue4662-consume-nterm.smt2 + regress0/strings/issue4674-recomp-nf.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue4674-recomp-nf.smt2 b/test/regress/regress0/strings/issue4674-recomp-nf.smt2 new file mode 100644 index 000000000..2096d51ef --- /dev/null +++ b/test/regress/regress0/strings/issue4674-recomp-nf.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_S) +(set-info :status sat) +(declare-fun a () String) +(assert (str.in_re "" (re.++ (str.to_re a) (re.comp re.allchar)))) +(check-sat) -- cgit v1.2.3