diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-02-28 22:20:18 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-28 22:20:18 -0800 |
| commit | 31efb570a9d5811fd88a34d4915d7d08c81d13fa (patch) | |
| tree | b3b553c8ce5075b40f0a8645aac28edb69b1c253 /src/api | |
| parent | b0609b2d70220064a44bc99e396bf0d2d5ade531 (diff) | |
Add support for str.from_code (#3829)
This commit adds support for `str.from_code`. This is work towards
supporting the new strings standard. The code currently just does an
eager expansion of the operator. The commit also renames `STRING_CODE`
to `STRING_TO_CODE` to better reflect the names of the operators in the
new standard.
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 6 | ||||
| -rw-r--r-- | src/api/cvc4cppkind.h | 15 |
2 files changed, 17 insertions, 4 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 31453b618..0d24139e8 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -258,7 +258,8 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ {STRING_TOLOWER, CVC4::Kind::STRING_TOLOWER}, {STRING_TOUPPER, CVC4::Kind::STRING_TOUPPER}, {STRING_REV, CVC4::Kind::STRING_REV}, - {STRING_CODE, CVC4::Kind::STRING_CODE}, + {STRING_FROM_CODE, CVC4::Kind::STRING_FROM_CODE}, + {STRING_TO_CODE, CVC4::Kind::STRING_TO_CODE}, {STRING_LT, CVC4::Kind::STRING_LT}, {STRING_LEQ, CVC4::Kind::STRING_LEQ}, {STRING_PREFIX, CVC4::Kind::STRING_PREFIX}, @@ -524,7 +525,8 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> {CVC4::Kind::STRING_TOLOWER, STRING_TOLOWER}, {CVC4::Kind::STRING_TOUPPER, STRING_TOUPPER}, {CVC4::Kind::STRING_REV, STRING_REV}, - {CVC4::Kind::STRING_CODE, STRING_CODE}, + {CVC4::Kind::STRING_FROM_CODE, STRING_FROM_CODE}, + {CVC4::Kind::STRING_TO_CODE, STRING_TO_CODE}, {CVC4::Kind::STRING_LT, STRING_LT}, {CVC4::Kind::STRING_LEQ, STRING_LEQ}, {CVC4::Kind::STRING_PREFIX, STRING_PREFIX}, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index eb8575907..d399ad616 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1988,7 +1988,7 @@ enum CVC4_PUBLIC Kind : int32_t */ STRING_REV, /** - * String code. + * String to code. * Returns the code point of a string if it has length one, or returns -1 * otherwise. * Parameters: 1 @@ -1996,7 +1996,18 @@ enum CVC4_PUBLIC Kind : int32_t * Create with: * mkTerm(Kind kind, Term child) */ - STRING_CODE, + STRING_TO_CODE, + /** + * String from code. + * Returns a string containing a single character whose code point matches + * the argument to this function, or the empty string if the argument is + * out-of-bounds. + * Parameters: 1 + * -[1]: Term of Integer sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + STRING_FROM_CODE, /** * String less than. * Returns true if string s1 is (strictly) less than s2 based on a |