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.

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 0db536d1b3e78258280dbb9cd97654ee591aaab4..7510b26ca079c276c2d3faa97592195b4d54d30d 100644 (file)
--- 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 78576a3f85ba26bde43a50bb4d5513cb112a266b..6bff05bdbe56ff29f9e38472da4f157197d2178c 100644 (file)
--- 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 (file)
index 0000000..7883221
--- /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 (file)
index 0000000..f2db302
--- /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)