diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-05 15:52:20 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-05 20:52:20 +0000 |
| commit | 3c98bb2e9abdb2542ac794f161d0f199c1cfaeaf (patch) | |
| tree | 12de562c61aae8ad066fcd33444ab4ee639d822b | |
| parent | e95e704f362690377d851fe80bbc778877bbfc69 (diff) | |
Fix spurious antecedant for symbolic regular expressions (#6284)
Fixes #6271.
This was triggered by recent fixes, this fixes solution soundness issues with symbolic regular expressions due to spuriously included antecedants, which made lemmas SAT-context dependent while being cached as user-context dependent.
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 4 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue6271-2-rnf.smt2 | 8 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue6271-rnf.smt2 | 8 |
4 files changed, 20 insertions, 2 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 0db536d1b..7510b26ca 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -265,11 +265,11 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) // if so, do simple unrolling Trace("strings-regexp") << "Simplify on " << atom << std::endl; Node conc = d_regexp_opr.simplify(atom, polarity); - Trace("strings-regexp") << "...finished" << std::endl; + Trace("strings-regexp") << "...finished, got " << conc << std::endl; // if simplifying successfully generated a lemma if (!conc.isNull()) { - std::vector<Node> iexp = rnfexp; + std::vector<Node> iexp; std::vector<Node> noExplain; iexp.push_back(assertion); noExplain.push_back(assertion); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 78576a3f8..6bff05bdb 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2046,6 +2046,8 @@ set(regress_1_tests regress1/strings/issue6191-replace-all.smt2 regress1/strings/issue6203-1-substr-ctn-strip.smt2 regress1/strings/issue6203-2-re-ccache.smt2 + regress1/strings/issue6271-rnf.smt2 + regress1/strings/issue6271-2-rnf.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue6271-2-rnf.smt2 b/test/regress/regress1/strings/issue6271-2-rnf.smt2 new file mode 100644 index 000000000..788322166 --- /dev/null +++ b/test/regress/regress1/strings/issue6271-2-rnf.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(declare-fun str4 () String) +(declare-fun str5 () String) +(assert (str.in_re str4 (re.+ (str.to_re str5)))) +(assert (= 1 (str.indexof str5 str4 0))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6271-rnf.smt2 b/test/regress/regress1/strings/issue6271-rnf.smt2 new file mode 100644 index 000000000..f2db302d7 --- /dev/null +++ b/test/regress/regress1/strings/issue6271-rnf.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp --strings-fmf +; EXPECT: sat +(set-logic ALL) +(set-option :strings-fmf true) +(declare-fun str7 () String) +(declare-fun str8 () String) +(assert (str.in_re str8 (re.++ re.allchar re.allchar (str.to_re str7)))) +(check-sat) |