diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-21 13:36:01 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-21 11:36:00 -0800 |
| commit | 18eb247c3f14761dc0e1981d4faf11833f069b9d (patch) | |
| tree | d29f8b299a61509d9ffeb9db51137371135731c8 /src/parser/smt2/smt2.cpp | |
| parent | be7ed89f137f4d0d64cf66ec40880370fbff2d4d (diff) | |
Simple changes towards unicode string standard (#3791)
This updates --lang=smt2.6.1 with the minor syntactic differences from the current syntax and the standard here: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.
The next steps will be to address the more invasive changes required to support the standard.
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 23 |
1 files changed, 16 insertions, 7 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 11dedb259..a7033b277 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -163,7 +163,6 @@ void Smt2::addStringOperators() { addOperator(kind::STRING_CHARAT, "str.at" ); addOperator(kind::STRING_STRIDOF, "str.indexof" ); addOperator(kind::STRING_STRREPL, "str.replace" ); - addOperator(kind::STRING_STRREPLALL, "str.replaceall"); if (!strictModeEnabled()) { addOperator(kind::STRING_TOLOWER, "str.tolower"); @@ -175,10 +174,12 @@ void Smt2::addStringOperators() { // at the moment, we only use this syntax for smt2.6.1 if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1) { - addOperator(kind::STRING_ITOS, "str.from-int"); - 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_ITOS, "str.from_int"); + 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_STRREPLALL, "str.replace_all"); } else { @@ -186,6 +187,8 @@ 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_STRREPLALL, "str.replaceall"); } addOperator(kind::REGEXP_CONCAT, "re.++"); @@ -196,7 +199,6 @@ void Smt2::addStringOperators() { addOperator(kind::REGEXP_OPT, "re.opt"); addOperator(kind::REGEXP_RANGE, "re.range"); addOperator(kind::REGEXP_LOOP, "re.loop"); - addOperator(kind::STRING_CODE, "str.code"); addOperator(kind::STRING_LT, "str.<"); addOperator(kind::STRING_LEQ, "str.<="); } @@ -365,7 +367,14 @@ void Smt2::addTheory(Theory theory) { defineType("RegLan", getExprManager()->regExpType()); defineType("Int", getExprManager()->integerType()); - defineVar("re.nostr", d_solver->mkRegexpEmpty().getExpr()); + if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1) + { + defineVar("re.none", d_solver->mkRegexpEmpty().getExpr()); + } + else + { + defineVar("re.nostr", d_solver->mkRegexpEmpty().getExpr()); + } defineVar("re.allchar", d_solver->mkRegexpSigma().getExpr()); addStringOperators(); |