From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 12 Jun 2020 02:25:07 +0000 (-0500)
Subject: Add rewrite for str.replace_re. (#4601)
X-Git-Tag: cvc5-1.0.0~3226
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4d547e52d3f2b54a0af7270d2b653d2cb24edb57;p=cvc5.git

Add rewrite for str.replace_re. (#4601)

This was discovered due to a proof checking abnormality, where the checker surprisingly succeeded in proving that the reduced form for a str.replace_re was equivalent for 2 different sets of skolems after rewriting.
---

diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp
index 5f3c83869..b67315935 100644
--- a/src/theory/strings/rewrites.cpp
+++ b/src/theory/strings/rewrites.cpp
@@ -113,6 +113,7 @@ const char* toString(Rewrite r)
     case Rewrite::RPL_X_Y_X_SIMP: return "RPL_X_Y_X_SIMP";
     case Rewrite::REPLACE_RE_EVAL: return "REPLACE_RE_EVAL";
     case Rewrite::REPLACE_RE_ALL_EVAL: return "REPLACE_RE_ALL_EVAL";
+    case Rewrite::REPLACE_RE_EMP_RE: return "REPLACE_RE_EMP_RE";
     case Rewrite::SPLIT_EQ: return "SPLIT_EQ";
     case Rewrite::SPLIT_EQ_STRIP_L: return "SPLIT_EQ_STRIP_L";
     case Rewrite::SPLIT_EQ_STRIP_R: return "SPLIT_EQ_STRIP_R";
diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h
index 62350c403..3b23e1e39 100644
--- a/src/theory/strings/rewrites.h
+++ b/src/theory/strings/rewrites.h
@@ -118,6 +118,7 @@ enum class Rewrite : uint32_t
   RPL_X_Y_X_SIMP,
   REPLACE_RE_EVAL,
   REPLACE_RE_ALL_EVAL,
+  REPLACE_RE_EMP_RE,
   SPLIT_EQ,
   SPLIT_EQ_STRIP_L,
   SPLIT_EQ_STRIP_R,
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 3c40062f5..befe52574 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -2948,6 +2948,13 @@ Node SequencesRewriter::rewriteReplaceRe(Node node)
       return returnRewrite(node, x, Rewrite::REPLACE_RE_EVAL);
     }
   }
+  // str.replace_re( x, y, z ) ---> z ++ x if "" in y ---> true
+  String emptyStr("");
+  if (RegExpEntail::testConstStringInRegExp(emptyStr, 0, y))
+  {
+    Node ret = nm->mkNode(STRING_CONCAT, z, x);
+    return returnRewrite(node, ret, Rewrite::REPLACE_RE_EMP_RE);
+  }
   return node;
 }