diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-10 12:50:52 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-10 12:50:52 -0700 |
| commit | 2da2646dd65e0458311a2dccfb04850c0b7d9e3c (patch) | |
| tree | 00d31835b3ad0c00064ae2b43a2a59844f418dd0 /src/api | |
| parent | 05c099890ae908e495ceaf26509b87896fd0ad54 (diff) | |
Add support for str.replace_re/str.replace_re_all (#4594)
This commit adds support for the last remaining string operators from
the new SMT-LIB standard for the theory of strings. The commit adds the
kinds, type checking, reductions, and evaluation rewrites for
`str.replace_re` and `str.replace_re_all`.
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 4 | ||||
| -rw-r--r-- | src/api/cvc4cppkind.h | 27 |
2 files changed, 31 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 325da8cdb..f0d28401e 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -257,6 +257,8 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {STRING_INDEXOF, CVC4::Kind::STRING_STRIDOF}, {STRING_REPLACE, CVC4::Kind::STRING_STRREPL}, {STRING_REPLACE_ALL, CVC4::Kind::STRING_STRREPLALL}, + {STRING_REPLACE_RE, CVC4::Kind::STRING_REPLACE_RE}, + {STRING_REPLACE_RE_ALL, CVC4::Kind::STRING_REPLACE_RE_ALL}, {STRING_TOLOWER, CVC4::Kind::STRING_TOLOWER}, {STRING_TOUPPER, CVC4::Kind::STRING_TOUPPER}, {STRING_REV, CVC4::Kind::STRING_REV}, @@ -526,6 +528,8 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::STRING_STRIDOF, STRING_INDEXOF}, {CVC4::Kind::STRING_STRREPL, STRING_REPLACE}, {CVC4::Kind::STRING_STRREPLALL, STRING_REPLACE_ALL}, + {CVC4::Kind::STRING_REPLACE_RE, STRING_REPLACE_RE}, + {CVC4::Kind::STRING_REPLACE_RE_ALL, STRING_REPLACE_RE_ALL}, {CVC4::Kind::STRING_TOLOWER, STRING_TOLOWER}, {CVC4::Kind::STRING_TOUPPER, STRING_TOUPPER}, {CVC4::Kind::STRING_REV, STRING_REV}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 02f13310a..82f1eb379 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -2003,6 +2003,33 @@ enum CVC4_PUBLIC Kind : int32_t */ STRING_REPLACE_ALL, /** + * String replace regular expression match. + * Replaces the first match of a regular expression r in string s1 with + * string s2. If r does not match a substring of s1, s1 is returned + * unmodified. + * Parameters: 3 + * -[1]: Term of sort String (string s1) + * -[2]: Term of sort Regexp (regexp r) + * -[3]: Term of sort String (string s2) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + STRING_REPLACE_RE, + /** + * String replace all regular expression matches. + * Replaces all matches of a regular expression r in string s1 with string + * s2. If r does not match a substring of s1, s1 is returned unmodified. + * Parameters: 3 + * -[1]: Term of sort String (string s1) + * -[2]: Term of sort Regexp (regexp r) + * -[3]: Term of sort String (string s2) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + STRING_REPLACE_RE_ALL, + /** * String to lower case. * Parameters: 1 * -[1]: Term of String sort |