diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-26 21:54:29 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-26 21:54:29 -0600 |
| commit | 87f3741db6ed41d3a776774bc1b60fd696585391 (patch) | |
| tree | 26f2498075d175ecc6c18743cb21ff3998ccc008 /src/api | |
| parent | cca153771119b70cbf01a3d05d8e2fd8d7e8636a (diff) | |
Add support for is_digit and regular expression difference (#3828)
Towards support for the strings standard. This adds support for str.is_digit and re.diff, which both can be eliminated eager during preprocessing.
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 4 | ||||
| -rw-r--r-- | src/api/cvc4cppkind.h | 19 |
2 files changed, 23 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 02fbbc42c..0a365a4d5 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -263,6 +263,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {STRING_LEQ, CVC4::Kind::STRING_LEQ}, {STRING_PREFIX, CVC4::Kind::STRING_PREFIX}, {STRING_SUFFIX, CVC4::Kind::STRING_SUFFIX}, + {STRING_IS_DIGIT, CVC4::Kind::STRING_IS_DIGIT}, {STRING_ITOS, CVC4::Kind::STRING_ITOS}, {STRING_STOI, CVC4::Kind::STRING_STOI}, {CONST_STRING, CVC4::Kind::CONST_STRING}, @@ -270,6 +271,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {REGEXP_CONCAT, CVC4::Kind::REGEXP_CONCAT}, {REGEXP_UNION, CVC4::Kind::REGEXP_UNION}, {REGEXP_INTER, CVC4::Kind::REGEXP_INTER}, + {REGEXP_DIFF, CVC4::Kind::REGEXP_DIFF}, {REGEXP_STAR, CVC4::Kind::REGEXP_STAR}, {REGEXP_PLUS, CVC4::Kind::REGEXP_PLUS}, {REGEXP_OPT, CVC4::Kind::REGEXP_OPT}, @@ -527,6 +529,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::STRING_LEQ, STRING_LEQ}, {CVC4::Kind::STRING_PREFIX, STRING_PREFIX}, {CVC4::Kind::STRING_SUFFIX, STRING_SUFFIX}, + {CVC4::Kind::STRING_IS_DIGIT, STRING_IS_DIGIT}, {CVC4::Kind::STRING_ITOS, STRING_ITOS}, {CVC4::Kind::STRING_STOI, STRING_STOI}, {CVC4::Kind::CONST_STRING, CONST_STRING}, @@ -534,6 +537,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::REGEXP_CONCAT, REGEXP_CONCAT}, {CVC4::Kind::REGEXP_UNION, REGEXP_UNION}, {CVC4::Kind::REGEXP_INTER, REGEXP_INTER}, + {CVC4::Kind::REGEXP_DIFF, REGEXP_DIFF}, {CVC4::Kind::REGEXP_STAR, REGEXP_STAR}, {CVC4::Kind::REGEXP_PLUS, REGEXP_PLUS}, {CVC4::Kind::REGEXP_OPT, REGEXP_OPT}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index ca5696537..eb8575907 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -2046,6 +2046,16 @@ enum CVC4_PUBLIC Kind : int32_t */ STRING_SUFFIX, /** + * String is-digit. + * Returns true if string s is digit (it is one of "0", ..., "9"). + * Parameters: 1 + * -[1]: Term of sort String + * Create with: + * mkTerm(Kind kind, Term child1) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + STRING_IS_DIGIT, + /** * Integer to string. * If the integer is negative this operator returns the empty string. * Parameters: 1 @@ -2111,6 +2121,15 @@ enum CVC4_PUBLIC Kind : int32_t */ REGEXP_INTER, /** + * Regexp difference. + * Parameters: 2 + * -[1]..[2]: Terms of Regexp sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + REGEXP_DIFF, + /** * Regexp *. * Parameters: 1 * -[1]: Term of sort Regexp |