diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-09-06 16:42:44 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-06 18:42:44 -0500 |
| commit | 856701f3b2154646eab6b7898fa33e5917322a7b (patch) | |
| tree | 497b4dd461907966316651299ae746494db53e8e /src/parser/smt2 | |
| parent | 91a5055015a97935d19b3dbf18062e189268a1f9 (diff) | |
Remove parsing/printing of meta-info command. (#3260)
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 11 |
1 files changed, 3 insertions, 8 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'; |