Add rewrite for contains + const strings replace (#2828)

1 files changed, 16 insertions, 0 deletions

diff --git a/src/util/regexp.h b/src/util/regexp.h
index 2ab6b659c..1588b5174 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -149,6 +149,22 @@ class CVC4_PUBLIC String {
 
   String prefix(std::size_t i) const { return substr(0, i); }
   String suffix(std::size_t i) const { return substr(size() - i, i); }
+
+  /**
+   * Checks if there is any overlap between this string and another string. This
+   * corresponds to checking whether one string contains the other and wether a
+   * substring of one is a prefix of the other and vice-versa.
+   *
+   * @param y The other string
+   * @return True if there is an overlap, false otherwise
+   */
+  bool noOverlapWith(const String& y) const
+  {
+    return y.find(*this) == std::string::npos
+           && this->find(y) == std::string::npos && this->overlap(y) == 0
+           && y.overlap(*this) == 0;
+  }
+
   /** string overlap
   *
   * if overlap returns m>0,