diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-05-21 23:40:44 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-21 23:40:44 -0500 |
commit | 026f7ae7bb3678281fb46defff4a1202c69d5f4e (patch) | |
tree | 46789ea4793e51f8f7154a7422c44d8d74457c48 /src/api | |
parent | 0f9b0dd69bef6a108b1ccc185223733f1d8fa40d (diff) |
Update string kind names in new API (#4509)
To match the smt2 Unicode standard. The internal ones are left unchanged for now.
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 24 | ||||
-rw-r--r-- | src/api/cvc4cppkind.h | 12 |
2 files changed, 18 insertions, 18 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index d990b3e22..052b62efc 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -253,10 +253,10 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {STRING_LENGTH, CVC4::Kind::STRING_LENGTH}, {STRING_SUBSTR, CVC4::Kind::STRING_SUBSTR}, {STRING_CHARAT, CVC4::Kind::STRING_CHARAT}, - {STRING_STRCTN, CVC4::Kind::STRING_STRCTN}, - {STRING_STRIDOF, CVC4::Kind::STRING_STRIDOF}, - {STRING_STRREPL, CVC4::Kind::STRING_STRREPL}, - {STRING_STRREPLALL, CVC4::Kind::STRING_STRREPLALL}, + {STRING_CONTAINS, CVC4::Kind::STRING_STRCTN}, + {STRING_INDEXOF, CVC4::Kind::STRING_STRIDOF}, + {STRING_REPLACE, CVC4::Kind::STRING_STRREPL}, + {STRING_REPLACE_ALL, CVC4::Kind::STRING_STRREPLALL}, {STRING_TOLOWER, CVC4::Kind::STRING_TOLOWER}, {STRING_TOUPPER, CVC4::Kind::STRING_TOUPPER}, {STRING_REV, CVC4::Kind::STRING_REV}, @@ -267,8 +267,8 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {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}, + {STRING_FROM_INT, CVC4::Kind::STRING_ITOS}, + {STRING_TO_INT, CVC4::Kind::STRING_STOI}, {CONST_STRING, CVC4::Kind::CONST_STRING}, {STRING_TO_REGEXP, CVC4::Kind::STRING_TO_REGEXP}, {REGEXP_CONCAT, CVC4::Kind::REGEXP_CONCAT}, @@ -522,10 +522,10 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::STRING_LENGTH, STRING_LENGTH}, {CVC4::Kind::STRING_SUBSTR, STRING_SUBSTR}, {CVC4::Kind::STRING_CHARAT, STRING_CHARAT}, - {CVC4::Kind::STRING_STRCTN, STRING_STRCTN}, - {CVC4::Kind::STRING_STRIDOF, STRING_STRIDOF}, - {CVC4::Kind::STRING_STRREPL, STRING_STRREPL}, - {CVC4::Kind::STRING_STRREPLALL, STRING_STRREPLALL}, + {CVC4::Kind::STRING_STRCTN, STRING_CONTAINS}, + {CVC4::Kind::STRING_STRIDOF, STRING_INDEXOF}, + {CVC4::Kind::STRING_STRREPL, STRING_REPLACE}, + {CVC4::Kind::STRING_STRREPLALL, STRING_REPLACE_ALL}, {CVC4::Kind::STRING_TOLOWER, STRING_TOLOWER}, {CVC4::Kind::STRING_TOUPPER, STRING_TOUPPER}, {CVC4::Kind::STRING_REV, STRING_REV}, @@ -536,8 +536,8 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {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::STRING_ITOS, STRING_FROM_INT}, + {CVC4::Kind::STRING_STOI, STRING_TO_INT}, {CVC4::Kind::CONST_STRING, CONST_STRING}, {CVC4::Kind::STRING_TO_REGEXP, STRING_TO_REGEXP}, {CVC4::Kind::REGEXP_CONCAT, REGEXP_CONCAT}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 05423a952..e084daf1e 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1961,7 +1961,7 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, Term child1, Term child2) * mkTerm(Kind kind, const std::vector<Term>& children) */ - STRING_STRCTN, + STRING_CONTAINS, /** * String index-of. * Returns the index of a substring s2 in a string s1 starting at index i. If @@ -1975,7 +1975,7 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, Term child1, Term child2, Term child3) * mkTerm(Kind kind, const std::vector<Term>& children) */ - STRING_STRIDOF, + STRING_INDEXOF, /** * String replace. * Replaces a string s2 in a string s1 with string s3. If s2 does not appear @@ -1988,7 +1988,7 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, Term child1, Term child2, Term child3) * mkTerm(Kind kind, const std::vector<Term>& children) */ - STRING_STRREPL, + STRING_REPLACE, /** * String replace all. * Replaces all occurrences of a string s2 in a string s1 with string s3. @@ -2001,7 +2001,7 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, Term child1, Term child2, Term child3) * mkTerm(Kind kind, const std::vector<Term>& children) */ - STRING_STRREPLALL, + STRING_REPLACE_ALL, /** * String to lower case. * Parameters: 1 @@ -2113,7 +2113,7 @@ enum CVC4_PUBLIC Kind : int32_t * Create with: * mkTerm(Kind kind, Term child) */ - STRING_ITOS, + STRING_FROM_INT, /** * String to integer (total function). * If the string does not contain an integer or the integer is negative, the @@ -2123,7 +2123,7 @@ enum CVC4_PUBLIC Kind : int32_t * Create with: * mkTerm(Kind kind, Term child) */ - STRING_STOI, + STRING_TO_INT, /** * Constant string. * Parameters: |