From 3c98bb2e9abdb2542ac794f161d0f199c1cfaeaf Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 5 Apr 2021 15:52:20 -0500 Subject: [PATCH] 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. --- src/theory/strings/regexp_solver.cpp | 4 ++-- test/regress/CMakeLists.txt | 2 ++ test/regress/regress1/strings/issue6271-2-rnf.smt2 | 8 ++++++++ test/regress/regress1/strings/issue6271-rnf.smt2 | 8 ++++++++ 4 files changed, 20 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/strings/issue6271-2-rnf.smt2 create mode 100644 test/regress/regress1/strings/issue6271-rnf.smt2 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 >& 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 iexp = rnfexp; + std::vector iexp; std::vector 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) -- 2.30.2