Eager conflict detection in strings based on constant prefix/suffix (#3110)

2 files changed, 41 insertions, 0 deletions

diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index ed9455e6d..a76e9084b 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -394,6 +394,43 @@ std::size_t String::rfind(const String &y, const std::size_t start) const {
   return std::string::npos;
 }
 
+bool String::hasPrefix(const String& y) const
+{
+  size_t s = size();
+  size_t ys = y.size();
+  if (ys > s)
+  {
+    return false;
+  }
+  for (size_t i = 0; i < ys; i++)
+  {
+    if (d_str[i] != y.d_str[i])
+    {
+      return false;
+    }
+  }
+  return true;
+}
+
+bool String::hasSuffix(const String& y) const
+{
+  size_t s = size();
+  size_t ys = y.size();
+  if (ys > s)
+  {
+    return false;
+  }
+  size_t idiff = s - ys;
+  for (size_t i = 0; i < ys; i++)
+  {
+    if (d_str[i + idiff] != y.d_str[i])
+    {
+      return false;
+    }
+  }
+  return true;
+}
+
 String String::replace(const String &s, const String &t) const {
   std::size_t ret = find(s);
   if (ret != std::string::npos) {
diff --git a/src/util/regexp.h b/src/util/regexp.h
index f7c6fb2ae..d1cb197fb 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -142,6 +142,10 @@ class CVC4_PUBLIC String {
 
   std::size_t find(const String& y, const std::size_t start = 0) const;
   std::size_t rfind(const String& y, const std::size_t start = 0) const;
+  /** Returns true if y is a prefix of this */
+  bool hasPrefix(const String& y) const;
+  /** Returns true if y is a suffix of this */
+  bool hasSuffix(const String& y) const;
 
   String replace(const String& s, const String& t) const;
   String substr(std::size_t i) const;