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 5f3c83869d53eb7842b64b3e6ecc892dd847c454..b673159353a71114623ca826e1587f977575565b 100644 (file)
--- 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 62350c403bf9fdaa7232d54a288a051cde36e503..3b23e1e39caf412648820036c9562e9aa5f5de3e 100644 (file)
--- 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 3c40062f5de98efba8d0f81662613c36de53eeb7..befe525742d225bf2c3d862ee812aeb97891e8df 100644 (file)
--- 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;
 }