Remove parsing/printing of meta-info command. (#3260)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c6b7de42c16348bb68fdaa5a5bf90ce60b63c09f..6a0bf2188d444e8f66699f6738952380c7104e6b 100644 (file)
--- 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 e02d308dab07027fc9b1b95ac87108612883b3e1..bd2d053e5a1548427235485365d00e49dc49d0b0 100644 (file)
--- 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 << ")";
 }