From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 2 Apr 2021 16:43:53 +0000 (-0500)
Subject: Fix case where RE unfolding generates a trivially true lemma (#6267)
X-Git-Tag: cvc5-1.0.0~1983
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c6c40d12c38fb30d0c4f503353532b93f03e745a;p=cvc5.git

Fix case where RE unfolding generates a trivially true lemma (#6267)

An RE unfolding lemma may rewrite to true for tautological RE memberships that our rewriter does not rewrite the membership to true.

An example is (str.in_re x (re.* (re.union (str.to_re "A") (str.to_re x))).

This PR ensures we are robust to these cases.

This fixes benchmarks 3-5 from #6203. Benchmark 3 is added here, 4-5 time out.
---

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 7737a90f7..0db536d1b 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -284,16 +284,21 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
             }
             InferenceId inf =
                 polarity ? InferenceId::STRINGS_RE_UNFOLD_POS : InferenceId::STRINGS_RE_UNFOLD_NEG;
-            d_im.sendInference(iexp, noExplain, conc, inf);
-            addedLemma = true;
-            processed.push_back(assertion);
-            if (e == 0)
+            // in very rare cases, we may find out that the unfolding lemma
+            // for a membership is equivalent to true, in spite of the RE
+            // not being rewritten to true.
+            if (d_im.sendInference(iexp, noExplain, conc, inf))
             {
-              // Remember that we have unfolded a membership for x
-              // notice that we only do this here, after we have definitely
-              // added a lemma.
-              repUnfold.insert(rep);
+              addedLemma = true;
+              if (e == 0)
+              {
+                // Remember that we have unfolded a membership for x
+                // notice that we only do this here, after we have definitely
+                // added a lemma.
+                repUnfold.insert(rep);
+              }
             }
+            processed.push_back(assertion);
           }
           else
           {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 64c584f7a..81c2bdba3 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1111,6 +1111,7 @@ set(regress_0_tests
   regress0/strings/issue5771-eager-pp.smt2
   regress0/strings/issue5816-re-kind.smt2
   regress0/strings/issue5915-repl-ctn-rewrite.smt2
+  regress0/strings/issue6203-3-unfold-trivial-true.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2
diff --git a/test/regress/regress0/strings/issue6203-3-unfold-trivial-true.smt2 b/test/regress/regress0/strings/issue6203-3-unfold-trivial-true.smt2
new file mode 100644
index 000000000..1ef762df3
--- /dev/null
+++ b/test/regress/regress0/strings/issue6203-3-unfold-trivial-true.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun s () String)
+(assert (str.in_re s (re.* (re.union (str.to_re "A") (str.to_re s)))))
+(assert (not (str.in_re s (re.* (re.opt (re.comp (str.to_re "A")))))))
+(check-sat)