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/regexp.h | |
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/regexp.h')
-rw-r--r-- | src/util/regexp.h | 30 |
1 files changed, 28 insertions, 2 deletions
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 |