diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 36 |
1 files changed, 7 insertions, 29 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 049bf8b4d..ed3abc166 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -180,26 +180,12 @@ void Smt2::addStringOperators() { addOperator(api::SEQ_UNIT, "seq.unit"); addOperator(api::SEQ_NTH, "seq.nth"); } - // at the moment, we only use this syntax for smt2.6 - if (getLanguage() == language::input::LANG_SMTLIB_V2_6 - || getLanguage() == language::input::LANG_SYGUS_V2) - { - addOperator(api::STRING_FROM_INT, "str.from_int"); - addOperator(api::STRING_TO_INT, "str.to_int"); - addOperator(api::STRING_IN_REGEXP, "str.in_re"); - addOperator(api::STRING_TO_REGEXP, "str.to_re"); - addOperator(api::STRING_TO_CODE, "str.to_code"); - addOperator(api::STRING_REPLACE_ALL, "str.replace_all"); - } - else - { - addOperator(api::STRING_FROM_INT, "int.to.str"); - addOperator(api::STRING_TO_INT, "str.to.int"); - addOperator(api::STRING_IN_REGEXP, "str.in.re"); - addOperator(api::STRING_TO_REGEXP, "str.to.re"); - addOperator(api::STRING_TO_CODE, "str.code"); - addOperator(api::STRING_REPLACE_ALL, "str.replaceall"); - } + addOperator(api::STRING_FROM_INT, "str.from_int"); + addOperator(api::STRING_TO_INT, "str.to_int"); + addOperator(api::STRING_IN_REGEXP, "str.in_re"); + addOperator(api::STRING_TO_REGEXP, "str.to_re"); + addOperator(api::STRING_TO_CODE, "str.to_code"); + addOperator(api::STRING_REPLACE_ALL, "str.replace_all"); addOperator(api::REGEXP_CONCAT, "re.++"); addOperator(api::REGEXP_UNION, "re.union"); @@ -656,15 +642,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) defineType("RegLan", d_solver->getRegExpSort(), true, true); defineType("Int", d_solver->getIntegerSort(), true, true); - if (getLanguage() == language::input::LANG_SMTLIB_V2_6 - || getLanguage() == language::input::LANG_SYGUS_V2) - { - defineVar("re.none", d_solver->mkRegexpEmpty()); - } - else - { - defineVar("re.nostr", d_solver->mkRegexpEmpty()); - } + defineVar("re.none", d_solver->mkRegexpEmpty()); defineVar("re.allchar", d_solver->mkRegexpSigma()); // Boolean is a placeholder |