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/parser | |
| 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/parser')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ef13d379e..94a273193 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -171,7 +171,9 @@ void Smt2::addStringOperators() { } addOperator(kind::STRING_PREFIX, "str.prefixof" ); addOperator(kind::STRING_SUFFIX, "str.suffixof" ); + addOperator(kind::STRING_FROM_CODE, "str.from_code"); addOperator(kind::STRING_IS_DIGIT, "str.is_digit" ); + // at the moment, we only use this syntax for smt2.6.1 if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1 || getLanguage() == language::input::LANG_SYGUS_V2) @@ -180,7 +182,7 @@ void Smt2::addStringOperators() { addOperator(kind::STRING_STOI, "str.to_int"); addOperator(kind::STRING_IN_REGEXP, "str.in_re"); addOperator(kind::STRING_TO_REGEXP, "str.to_re"); - addOperator(kind::STRING_CODE, "str.to_code"); + addOperator(kind::STRING_TO_CODE, "str.to_code"); addOperator(kind::STRING_STRREPLALL, "str.replace_all"); } else @@ -189,7 +191,7 @@ void Smt2::addStringOperators() { addOperator(kind::STRING_STOI, "str.to.int"); addOperator(kind::STRING_IN_REGEXP, "str.in.re"); addOperator(kind::STRING_TO_REGEXP, "str.to.re"); - addOperator(kind::STRING_CODE, "str.code"); + addOperator(kind::STRING_TO_CODE, "str.code"); addOperator(kind::STRING_STRREPLALL, "str.replaceall"); } |