diff options
| -rw-r--r-- | src/parser/smt2/Smt2.g | 11 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 13 |
2 files changed, 5 insertions, 19 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index c6b7de42c..6a0bf2188 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -239,7 +239,7 @@ command [std::unique_ptr<CVC4::Command>* cmd] cmd->reset(PARSER_STATE->setLogic(name)); } | /* set-info */ - SET_INFO_TOK metaInfoInternal[cmd] + SET_INFO_TOK setInfoInternal[cmd] | /* get-info */ GET_INFO_TOK KEYWORD { cmd->reset(new GetInfoCommand( @@ -1153,8 +1153,7 @@ sygusGrammar[CVC4::Type & ret, } ; -// Separate this into its own rule (can be invoked by set-info or meta-info) -metaInfoInternal[std::unique_ptr<CVC4::Command>* cmd] +setInfoInternal[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::string name; SExpr sexpr; @@ -1203,11 +1202,8 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] std::vector<Type> sorts; std::vector<Expr> flattenVars; } - /* meta-info */ - : META_INFO_TOK metaInfoInternal[cmd] - /* declare-const */ - | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } + : DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_NONE,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } sortSymbol[t,CHECK_DECLARED] @@ -2814,7 +2810,6 @@ RPAREN_TOK : ')'; INDEX_TOK : '_'; SET_LOGIC_TOK : 'set-logic'; SET_INFO_TOK : 'set-info'; -META_INFO_TOK : 'meta-info'; GET_INFO_TOK : 'get-info'; SET_OPTION_TOK : 'set-option'; GET_OPTION_TOK : 'get-option'; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index e02d308da..bd2d053e5 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1835,11 +1835,7 @@ static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c, Variant v) { - if(v == z3str_variant || v == smt2_0_variant) { - out << "(set-info :status " << c->getStatus() << ")"; - } else { - out << "(meta-info :status " << c->getStatus() << ")"; - } + out << "(set-info :status " << c->getStatus() << ")"; } static void toStream(std::ostream& out, @@ -1856,12 +1852,7 @@ static void toStream(std::ostream& out, static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v) { - if(v == z3str_variant || v == smt2_0_variant) { - out << "(set-info :" << c->getFlag() << " "; - } else { - out << "(meta-info :" << c->getFlag() << " "; - } - + out << "(set-info :" << c->getFlag() << " "; SExpr::toStream(out, c->getSExpr(), variantToLanguage(v)); out << ")"; } |