Convert most instances of dataypes in parsers to the new API (#4054)

I am still accessing Expr-level Datatypes for the sygus v1/v2 parsers (within smt2). This will be addressed in two ways in the future:
(1) The sygus v1 parser will be deleted,
(2) The sygus v2 parser will be updated to use a "Grammar" object as an extension of the new API, which will hide all calls to the underlying datatype. (See https://github.com/abdoo8080/CVC4/tree/sygus-api). FYI @abdoo8080 .

Note I've renamed "mkMutualDatatypeTypes" to "bindMutualDatatypeTypes" to be more accurate and follow the updated name conventions in the parser.

The next step will be to handle parametric datatypes, which are not specifically addressed by this PR.

1 files changed, 12 insertions, 14 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index abfd363f8..82c0581ce 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -683,7 +683,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
   SExpr sexpr;
   std::string id;
   api::Sort t;
-  std::vector<CVC4::Datatype> dts;
+  std::vector<CVC4::api::DatatypeDecl> dts;
   Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl;
   std::string s;
   api::Term func;
@@ -757,7 +757,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
     END_TOK
     { PARSER_STATE->popScope();
       cmd->reset(new DatatypeDeclarationCommand(
-          api::sortVectorToTypes(PARSER_STATE->mkMutualDatatypeTypes(dts))));
+          api::sortVectorToTypes(PARSER_STATE->bindMutualDatatypeTypes(dts))));
     }
 
   | CONTEXT_TOK
@@ -1204,7 +1204,7 @@ identifier[std::string& id,
  * forward-declaration in CVC language datatype definitions, we have
  * to create types for them on-the-fly).  Before passing CHECK_NONE
  * you really should have a clear idea of WHY you need to parse that
- * way; then you should trace through Parser::mkMutualDatatypeType()
+ * way; then you should trace through Parser::bindMutualDatatypeType()
  * to figure out just what you're in for.
  */
 type[CVC4::api::Sort& t,
@@ -2310,7 +2310,7 @@ iteElseTerm[CVC4::api::Term& f]
 /**
  * Parses a datatype definition
  */
-datatypeDef[std::vector<CVC4::Datatype>& datatypes]
+datatypeDef[std::vector<CVC4::api::DatatypeDecl>& datatypes]
 @init {
   std::string id, id2;
   api::Sort t;
@@ -2331,10 +2331,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
       )* RBRACKET
     )?
     {
-      datatypes.push_back(Datatype(SOLVER->getExprManager(),
-                                   id,
-                                   api::sortVectorToTypes(params),
-                                   false));
+      datatypes.push_back(SOLVER->mkDatatypeDecl(id, params, false));
       if(!PARSER_STATE->isUnresolvedType(id)) {
         // if not unresolved, must be undeclared
         PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT);
@@ -2348,14 +2345,14 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
 /**
  * Parses a constructor defintion for type
  */
-constructorDef[CVC4::Datatype& type]
+constructorDef[CVC4::api::DatatypeDecl& type]
 @init {
   std::string id;
-  std::unique_ptr<CVC4::DatatypeConstructor> ctor;
+  std::unique_ptr<CVC4::api::DatatypeConstructorDecl> ctor;
 }
   : identifier[id,CHECK_UNDECLARED,SYM_SORT]
-    {
-      ctor.reset(new CVC4::DatatypeConstructor(id));
+    { 
+      ctor.reset(new CVC4::api::DatatypeConstructorDecl(id));
     }
     ( LPAREN
       selector[&ctor]
@@ -2368,13 +2365,14 @@ constructorDef[CVC4::Datatype& type]
     }
   ;
 
-selector[std::unique_ptr<CVC4::DatatypeConstructor>* ctor]
+selector[std::unique_ptr<CVC4::api::DatatypeConstructorDecl>* ctor]
 @init {
   std::string id;
   api::Sort t, t2;
 }
   : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON type[t,CHECK_NONE]
-    { (*ctor)->addArg(id, t.getType());
+    {
+      (*ctor)->addSelector(id, t);
       Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
     }
   ;