From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 5 Apr 2021 20:52:20 +0000 (-0500)
Subject: Fix spurious antecedant for symbolic regular expressions (#6284)
X-Git-Tag: cvc5-1.0.0~1968
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c98bb2;p=cvc5.git

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 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)