diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 38 |
1 files changed, 2 insertions, 36 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 : '!'; |