Fix regular expression aggressive elim (#6627)

Fixes #6620, fixes #6622. Fixes cvc5/cvc5-projects#254.

The benchmarks from the 2 issues timeout, a regression is added for the projects issue.

diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index ac0e487f9fb783847befaeadcd2fd1288caa4b3f..45b1f62fb75a55c6f561fb96abf47240bed20d7e 100644 (file)
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -400,6 +400,12 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
       {
         sStartIndex = lens;
       }
+      else if (r == 1 && sConstraints.size() == 2)
+      {
+        // first and last children cannot overlap
+        Node bound = nm->mkNode(GEQ, sss, sStartIndex);
+        sConstraints.push_back(bound);
+      }
       sLength = nm->mkNode(MINUS, sLength, lens);
     }
     if (r == 1 && !sConstraints.empty())
@@ -417,7 +423,6 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
   }
   if (!sConstraints.empty())
   {
-    Assert(rexpElimChildren.size() + sConstraints.size() == nchildren);
     Node ss = nm->mkNode(STRING_SUBSTR, x, sStartIndex, sLength);
     Assert(!rexpElimChildren.empty());
     Node regElim = utils::mkConcat(rexpElimChildren, nm->regExpType());

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 422acd0489baba77aa9d580a73f992c1a541798f..e10b89c79786ba62467b440c7e446d6667a7c04e 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2133,6 +2133,7 @@ set(regress_1_tests
   regress1/strings/pierre150331.smt2
   regress1/strings/policy_variable.smt2
   regress1/strings/pre_ctn_no_skolem_share.smt2
+  regress1/strings/proj254-re-elim-agg.smt2
   regress1/strings/query4674.smt2
   regress1/strings/query8485.smt2
   regress1/strings/re-all-char-hard.smt2

diff --git a/test/regress/regress1/strings/proj254-re-elim-agg.smt2 b/test/regress/regress1/strings/proj254-re-elim-agg.smt2
new file mode 100644 (file)
index 0000000..cd19dc1
--- /dev/null
+++ b/test/regress/regress1/strings/proj254-re-elim-agg.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :strings-exp true)
+(set-option :re-elim true)
+(set-option :re-elim-agg true)
+(declare-fun a () String)
+(assert (str.in_re a (re.++ (re.+ (str.to_re "AB")) (str.to_re "B"))))
+(assert (<= (str.len a) 4))
+(check-sat)