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/parser | |
| 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/parser')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index d915d2ab4..ff155d0f9 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -171,6 +171,7 @@ void Smt2::addStringOperators() { } addOperator(kind::STRING_PREFIX, "str.prefixof" ); addOperator(kind::STRING_SUFFIX, "str.suffixof" ); + 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) @@ -201,6 +202,7 @@ void Smt2::addStringOperators() { addOperator(kind::REGEXP_RANGE, "re.range"); addOperator(kind::REGEXP_LOOP, "re.loop"); addOperator(kind::REGEXP_COMPLEMENT, "re.comp"); + addOperator(kind::REGEXP_DIFF, "re.diff"); addOperator(kind::STRING_LT, "str.<"); addOperator(kind::STRING_LEQ, "str.<="); } |