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.
CVC4 · Jun 12, 2020 · 4d547e5 · 4d547e5
1 parent ad87bbc
commit 4d547e5
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 0 deletions.
diff --git 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
@@ -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
@@ -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;
 }