diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-27 23:16:38 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-27 23:16:38 -0500 |
commit | 675e82e32a34911163f9de0e6389eb107be5b0f1 (patch) | |
tree | a3215999b2f1550325b77d19e14a61793dafce35 /src/util | |
parent | 1fe3247a0bf4b806f99c161dcc9c6644aabb38c1 (diff) |
Improve strings rewriter for contains (#1207)
* Work on rewriter for string contains.
* Add rewrites that mix str.to.int and str.contains. Documentation, add regression.
* Minor
* Minor
* Address review, add a few TODOs. Improve some non-digit -> not is number.
* Fix
* Simplify.
* Clang format, minor fixing of comments.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/regexp.cpp | 10 | ||||
-rw-r--r-- | src/util/regexp.h | 30 |
2 files changed, 36 insertions, 4 deletions
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index 681b574a3..d93c5426e 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -357,14 +357,20 @@ bool String::isNumber() const { return false; } for (unsigned character : d_str) { - unsigned char c = convertUnsignedIntToChar(character); - if (c < '0' || c > '9') { + if (!isDigit(character)) + { return false; } } return true; } +bool String::isDigit(unsigned character) +{ + unsigned char c = convertUnsignedIntToChar(character); + return c >= '0' && c <= '9'; +} + int String::toNumber() const { if (isNumber()) { int ret = 0; diff --git a/src/util/regexp.h b/src/util/regexp.h index 9d351dde4..d51ef4372 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -127,15 +127,41 @@ 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); } - // if y=y1...yn and overlap returns m, then this is x1...y1...ym + /** string overlap + * + * if overlap returns m>0, + * then the maximal suffix of this string that is a prefix of y is of length m. + * + * For example, if x is "abcdef", then: + * x.overlap("defg") = 3 + * x.overlap("ab") = 0 + * x.overlap("d") = 0 + * x.overlap("bcdefdef") = 5 + */ std::size_t overlap(const String& y) const; - // if y=y1...yn and overlap returns m, then this is y(n+1-m)...yn...xk + /** string reverse overlap + * + * if roverlap returns m>0, + * then the maximal prefix of this string that is a suffix of y is of length m. + * + * For example, if x is "abcdef", then: + * x.roverlap("aaabc") = 3 + * x.roverlap("def") = 0 + * x.roverlap("d") = 0 + * x.roverlap("defabcde") = 5 + * + * Notice that x.overlap(y) = y.roverlap(x) + */ std::size_t roverlap(const String& y) const; bool isNumber() const; int toNumber() const; const std::vector<unsigned>& getVec() const { return d_str; } + /** is the unsigned a digit? + * The input should be the same type as the element type of d_str + */ + static bool isDigit(unsigned character); private: // guarded |