diff options
Diffstat (limited to 'src/theory/strings/word.h')
| -rw-r--r-- | src/theory/strings/word.h | 78 |
1 files changed, 42 insertions, 36 deletions
diff --git a/src/theory/strings/word.h b/src/theory/strings/word.h index e4d10247a..74f50ee9a 100644 --- a/src/theory/strings/word.h +++ b/src/theory/strings/word.h @@ -20,6 +20,7 @@ #include <vector> #include "expr/node.h" +#include "expr/type_node.h" namespace CVC4 { namespace theory { @@ -28,7 +29,10 @@ namespace strings { // ------------------------------ for words (string or sequence constants) class Word { -public: + public: + /** make empty constant of type tn */ + static Node mkEmptyWord(TypeNode tn); + /** make empty constant of kind k */ static Node mkEmptyWord(Kind k); @@ -45,9 +49,9 @@ public: static std::size_t find(TNode x, TNode y, std::size_t start = 0); /** - * Return the first position y occurs in x searching from the end of x, or - * std::string::npos otherwise - */ + * Return the first position y occurs in x searching from the end of x, or + * std::string::npos otherwise + */ static std::size_t rfind(TNode x, TNode y, std::size_t start = 0); /** Returns true if y is a prefix of x */ @@ -62,8 +66,9 @@ public: /** Return the substring/subsequence of x starting at index i */ static Node substr(TNode x, std::size_t i); - /** Return the substring/subsequence of x starting at index i with size at most - * j */ + /** Return the substring/subsequence of x starting at index i with size at + * most + * j */ static Node substr(TNode x, std::size_t i, std::size_t j); /** Return the prefix of x of size at most i */ @@ -73,42 +78,43 @@ public: static Node suffix(TNode x, std::size_t i); /** - * Checks if there is any overlap between word x and another word y. This - * corresponds to checking whether one string contains the other and whether a - * substring/subsequence of one is a prefix of the other and vice-versa. - * - * @param x The first string - * @param y The second string - * @return True if there is an overlap, false otherwise - */ + * Checks if there is any overlap between word x and another word y. This + * corresponds to checking whether one string contains the other and whether a + * substring/subsequence of one is a prefix of the other and vice-versa. + * + * @param x The first string + * @param y The second string + * @return True if there is an overlap, false otherwise + */ static bool noOverlapWith(TNode x, TNode y); /** 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 - */ + * + * 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 + */ static std::size_t overlap(TNode x, TNode y); /** reverse overlap - * - * if roverlap returns m>0, - * then the maximal prefix of this word 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) - */ + * + * if roverlap returns m>0, + * then the maximal prefix of this word 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) + */ static std::size_t roverlap(TNode x, TNode y); }; |