From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sat, 2 Feb 2019 08:36:42 +0000 (-0800)
Subject: Fix corner case in stripConstantEndpoints (#2824)
X-Git-Tag: cvc5-1.0.0~4266
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e374c7fbde3b3a5148b6e8fc302277b6e786965e;p=cvc5.git

Fix corner case in stripConstantEndpoints (#2824)

`stripConstantEndpoints()` was returning `true` when the first argument
was a list only containing an empty string, which could lead to rewrite
loops. This commit checks for that case and adds a unit test for it.
---

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 0c8d6ac8d..f90d5bcfd 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -3583,6 +3583,12 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1,
       unsigned index1 = r == 0 ? 0 : n2.size() - 1;
       bool removeComponent = false;
       Node n1cmp = n1[index0];
+
+      if (n1cmp.isConst() && n1cmp.getConst<String>().size() == 0)
+      {
+        return false;
+      }
+
       std::vector<Node> sss;
       std::vector<Node> sls;
       n1cmp = decomposeSubstrChain(n1cmp, sss, sls);
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 5f08ce741..bbaa4733f 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -1180,6 +1180,23 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     }
   }
 
+  void testStripConstantEndpoints()
+  {
+    Node empty = d_nm->mkConst(::CVC4::String(""));
+    Node a = d_nm->mkConst(::CVC4::String("A"));
+
+    {
+      // stripConstantEndpoints({ "" }, { "a" }, {}, {}, 0) ---> false
+      std::vector<Node> n1 = {empty};
+      std::vector<Node> n2 = {a};
+      std::vector<Node> nb;
+      std::vector<Node> ne;
+      bool res =
+          TheoryStringsRewriter::stripConstantEndpoints(n1, n2, nb, ne, 0);
+      TS_ASSERT(!res);
+    }
+  }
+
  private:
   ExprManager* d_em;
   SmtEngine* d_smt;