diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-03-05 16:17:15 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-06 00:17:15 +0000 |
commit | c6fffe4fd328401f7f7e0757303e8dea5f6c14a4 (patch) | |
tree | 84bbb3f44fa7ffbeba0c0baf9b7b22f036d2e9f4 /src/parser | |
parent | 555e4b0b6b10e9170676c0a3ef9b778322f3327f (diff) |
Remove SMT-LIB 2.5 and 2.0 support. (#6068)
This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 38 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 36 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 14 |
3 files changed, 10 insertions, 78 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 7ef7edbbe..ea45e2e61 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -480,12 +480,6 @@ command [std::unique_ptr<CVC4::Command>* cmd] /* New SMT-LIB 2.5 command set */ | smt25Command[cmd] - { if(PARSER_STATE->v2_0() && PARSER_STATE->strictModeEnabled()) { - PARSER_STATE->parseError( - "SMT-LIB 2.5 commands are not permitted while operating in strict " - "compliance mode and in SMT-LIB 2.0 mode."); - } - } /* CVC4-extended SMT-LIB commands */ | extendedCommand[cmd] @@ -900,9 +894,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] } /* Extended SMT-LIB set of commands syntax, not permitted in * --smtlib2 compliance mode. */ - : DECLARE_DATATYPES_2_5_TOK datatypes_2_5_DefCommand[false, cmd] - | DECLARE_CODATATYPES_2_5_TOK datatypes_2_5_DefCommand[true, cmd] - | DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd] + : DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd] | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] /* Support some of Z3's extended SMT-LIB commands */ @@ -1081,32 +1073,6 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] ) ; - -datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd] -@declarations { - std::vector<api::DatatypeDecl> dts; - std::string name; - std::vector<api::Sort> sorts; - std::vector<std::string> dnames; - std::vector<unsigned> arities; -} - : { PARSER_STATE->checkThatLogicIsSet(); - /* open a scope to keep the UnresolvedTypes contained */ - PARSER_STATE->pushScope(); } - LPAREN_TOK /* parametric sorts */ - ( symbol[name,CHECK_UNDECLARED,SYM_SORT] - { - sorts.push_back(PARSER_STATE->mkSort(name)); - } - )* - RPAREN_TOK - LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK - { PARSER_STATE->popScope(); - cmd->reset(new DatatypeDeclarationCommand( - PARSER_STATE->bindMutualDatatypeTypes(dts, true))); - } - ; - datatypeDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd] @declarations { std::vector<api::DatatypeDecl> dts; @@ -2226,7 +2192,7 @@ GET_PROOF_TOK : 'get-proof'; GET_UNSAT_ASSUMPTIONS_TOK : 'get-unsat-assumptions'; GET_UNSAT_CORE_TOK : 'get-unsat-core'; EXIT_TOK : 'exit'; -RESET_TOK : { PARSER_STATE->v2_5() }? 'reset'; +RESET_TOK : 'reset'; RESET_ASSERTIONS_TOK : 'reset-assertions'; LET_TOK : 'let'; ATTRIBUTE_TOK : '!'; 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 diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index ed329675d..be1476fad 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -227,18 +227,6 @@ class Smt2 : public Parser api::Grammar* mkGrammar(const std::vector<api::Term>& boundVars, const std::vector<api::Term>& ntSymbols); - bool v2_0() const - { - return getLanguage() == language::input::LANG_SMTLIB_V2_0; - } - /** - * Are we using smtlib 2.5 or above? If exact=true, then this method returns - * false if the input language is not exactly SMT-LIB 2.5. - */ - bool v2_5(bool exact = false) const - { - return language::isInputLang_smt2_5(getLanguage(), exact); - } /** * Are we using smtlib 2.6 or above? If exact=true, then this method returns * false if the input language is not exactly SMT-LIB 2.6. @@ -257,7 +245,7 @@ class Smt2 : public Parser * and SyGuS) treats duplicate double quotes ("") as an escape sequence * denoting a single double quote ("). */ - bool escapeDupDblQuote() const { return v2_5() || sygus(); } + bool escapeDupDblQuote() const { return v2_6() || sygus(); } void checkThatLogicIsSet(); |