Support for str.<= and str.< (#1882)

2 files changed, 22 insertions, 0 deletions

diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 4cbda5147..bfd9cc3a7 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -298,6 +298,26 @@ std::string String::toString(bool useEscSequences) const {
   return str;
 }
 
+bool String::isLeq(const String &y) const
+{
+  for (unsigned i = 0; i < size(); ++i)
+  {
+    if (i >= y.size())
+    {
+      return false;
+    }
+    if (d_str[i] > y.d_str[i])
+    {
+      return false;
+    }
+    if (d_str[i] < y.d_str[i])
+    {
+      return true;
+    }
+  }
+  return true;
+}
+
 bool String::isRepeated() const {
   if (size() > 1) {
     unsigned int f = d_str[0];
diff --git a/src/util/regexp.h b/src/util/regexp.h
index c8b491475..8b99dfd87 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -131,6 +131,8 @@ class CVC4_PUBLIC String {
   bool empty() const { return d_str.empty(); }
   /** is this the empty string? */
   bool isEmptyString() const { return empty(); }
+  /** is less than or equal to string y */
+  bool isLeq(const String& y) const;
   /** Return the length of the string */
   std::size_t size() const { return d_str.size(); }