From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 19 Mar 2019 19:15:24 +0000 (-0500)
Subject: Make declare-datatype(s) a standard, non-extended command in the Smt2 parser. (#2874)
X-Git-Tag: cvc5-1.0.0~4231
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=96b6b3a172d76753355e258edadcf977b39edcb8;p=cvc5.git

Make declare-datatype(s) a standard, non-extended command in the Smt2 parser. (#2874)
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 81f01c138..d3e0ba70e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -407,6 +407,8 @@ command [std::unique_ptr<CVC4::Command>* cmd]
                                            ExprManager::VAR_FLAG_DEFINED, true);
       cmd->reset(new DefineFunctionCommand(name, func, terms, expr));
     }
+  | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
+  | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
   | /* value query */
     GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
@@ -1211,9 +1213,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
      * --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_DATATYPE_TOK datatypeDefCommand[false, cmd]
   | DECLARE_CODATATYPE_TOK datatypeDefCommand[true, cmd]
-  | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
   | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd]
   | rewriterulesCommand[cmd]