diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-23 17:18:19 -0600 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-23 15:18:19 -0800 |
| commit | b3471b719f1cd031d35e9a431027088b0dec156b (patch) | |
| tree | bc5e55a278f9e927471ce99146e9fdc992bc716b /src/theory/strings/kinds | |
| parent | f5ca3e5d09b457ac21b10793eb5d1efe3fbe40f6 (diff) | |
Initial support for string reverse (#3581)
Type rules, parsing and printing, basic rewriting including constant evaluation, reduction for string reverse (`str.rev`).
Also improves support in a few places for tolower/toupper.
Diffstat (limited to 'src/theory/strings/kinds')
| -rw-r--r-- | src/theory/strings/kinds | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 4e90d1583..aa1e2627a 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -30,6 +30,7 @@ operator STRING_STOI 1 "string to integer (total function)" operator STRING_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise" operator STRING_TOLOWER 1 "string to lowercase conversion" operator STRING_TOUPPER 1 "string to uppercase conversion" +operator STRING_REV 1 "string reverse" sort STRING_TYPE \ Cardinality::INTEGERS \ @@ -104,6 +105,7 @@ typerule STRING_STOI "SimpleTypeRule<RInteger, AString>" typerule STRING_CODE "SimpleTypeRule<RInteger, AString>" typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>" typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>" +typerule STRING_REV "SimpleTypeRule<RString, AString>" typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>" |