diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-08 14:50:47 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-08 14:50:47 -0500 |
commit | f5e3739358b98d9a6ebc16fbc5aed9edee1483dc (patch) | |
tree | 6659d344360af9964266614f33dd16f24ed39923 /src/util | |
parent | 4f3416bf998cdf3fc8b6adf6debb7e65d663bd7c (diff) |
Support for str.<= and str.< (#1882)
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/regexp.cpp | 20 | ||||
-rw-r--r-- | src/util/regexp.h | 2 |
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(); } |