From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 12 Mar 2020 21:57:42 +0000 (-0500)
Subject: Convert most instances of dataypes in parsers to the new API (#4054)
X-Git-Tag: cvc5-1.0.0~3497
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ef71fc3405900226557dc634dcf69f1a0738fea2;p=cvc5.git

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.
---

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;
     }
   ;
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index e9a037d6e..b36f36a93 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -394,19 +394,12 @@ bool Parser::isUnresolvedType(const std::string& name) {
   return d_unresolved.find(getSort(name)) != d_unresolved.end();
 }
 
-std::vector<api::Sort> Parser::mkMutualDatatypeTypes(
-    std::vector<Datatype>& datatypes, bool doOverload, uint32_t flags)
+std::vector<api::Sort> Parser::bindMutualDatatypeTypes(
+    std::vector<api::DatatypeDecl>& datatypes, bool doOverload)
 {
   try {
-    std::set<Type> tset = api::sortSetToTypes(d_unresolved);
-    std::vector<DatatypeType> dtypes =
-        d_solver->getExprManager()->mkMutualDatatypeTypes(
-            datatypes, tset, flags);
-    std::vector<api::Sort> types;
-    for (unsigned i = 0, dtsize = dtypes.size(); i < dtsize; i++)
-    {
-      types.push_back(api::Sort(dtypes[i]));
-    }
+    std::vector<api::Sort> types =
+        d_solver->mkDatatypeSorts(datatypes, d_unresolved);
 
     assert(datatypes.size() == types.size());
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 1197c1ff6..ecea4d3bd 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -592,19 +592,16 @@ public:
   bool isUnresolvedType(const std::string& name);
 
   /**
-   * Create sorts of mutually-recursive datatypes.
-   * For each symbol defined by the datatype, if a symbol with name already exists,
-   *  then if doOverload is true, we create overloaded operators.
-   *  else if doOverload is false, the existing expression is shadowed by the new expression.
+   * Creates and binds sorts of a list of mutually-recursive datatype
+   * declarations.
    *
-   * flags specify information about the datatype, e.g. whether it should be
-   * printed out as a definition in models or not
-   *   (see enum in expr_manager_template.h).
+   * For each symbol defined by the datatype, if a symbol with name already
+   * exists, then if doOverload is true, we create overloaded operators. Else, if
+   * doOverload is false, the existing expression is shadowed by the new
+   * expression.
    */
-  std::vector<api::Sort> mkMutualDatatypeTypes(
-      std::vector<Datatype>& datatypes,
-      bool doOverload = false,
-      uint32_t flags = ExprManager::DATATYPE_FLAG_NONE);
+  std::vector<api::Sort> bindMutualDatatypeTypes(
+      std::vector<api::DatatypeDecl>& datatypes, bool doOverload = false);
 
   /** make flat function type
    *
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d87c44a68..e54f8eaa9 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -667,7 +667,7 @@ sygusGrammarV1[CVC4::api::Sort & ret,
   std::string name;
   unsigned startIndex = 0;
   std::vector<std::vector<CVC4::SygusGTerm>> sgts;
-  std::vector<CVC4::Datatype> datatypes;
+  std::vector<api::DatatypeDecl> datatypes;
   std::vector<api::Sort> sorts;
   std::vector<std::vector<ParseOp>> ops;
   std::vector<std::vector<std::string>> cnames;
@@ -770,7 +770,7 @@ sygusGrammarV1[CVC4::api::Sort & ret,
             "Internal error : could not infer "
             "builtin sort for nested gterm.");
       }
-      datatypes[i].setSygus(
+      datatypes[i].getDatatype().setSygus(
           sorts[i].getType(), bvl.getExpr(), allow_const[i], false);
       PARSER_STATE->mkSygusDatatype(datatypes[i],
                                     ops[i],
@@ -789,8 +789,7 @@ sygusGrammarV1[CVC4::api::Sort & ret,
                             << std::endl;
     }
     std::vector<api::Sort> datatypeTypes =
-        PARSER_STATE->mkMutualDatatypeTypes(
-            datatypes, false, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+        PARSER_STATE->bindMutualDatatypeTypes(datatypes, false);
     ret = datatypeTypes[0];
   };
 
@@ -942,7 +941,7 @@ sygusGrammar[CVC4::api::Sort & ret,
   CVC4::api::Sort t;
   std::string name;
   CVC4::api::Term e, e2;
-  std::vector<CVC4::Datatype> datatypes;
+  std::vector<api::DatatypeDecl> datatypes;
   std::set<api::Sort> unresTypes;
   std::map<CVC4::api::Term, CVC4::api::Sort> ntsToUnres;
   unsigned dtProcessed = 0;
@@ -959,7 +958,7 @@ sygusGrammar[CVC4::api::Sort & ret,
       Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl;
       // make the datatype, which encodes terms generated by this non-terminal
       std::string dname = i.first;
-      datatypes.push_back(Datatype(SOLVER->getExprManager(), dname));
+      datatypes.push_back(SOLVER->mkDatatypeDecl(dname));
       // make its unresolved type, used for referencing the final version of
       // the datatype
       PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
@@ -1037,7 +1036,7 @@ sygusGrammar[CVC4::api::Sort & ret,
     {
       bool aci = allowConst.find(i)!=allowConst.end();
       api::Sort btt = sortedVarNames[i].second;
-      datatypes[i].setSygus(btt.getType(), bvl.getExpr(), aci, false);
+      datatypes[i].getDatatype().setSygus(btt.getType(), bvl.getExpr(), aci, false);
       Trace("parser-sygus2") << "- " << datatypes[i].getName()
                              << ", #cons= " << datatypes[i].getNumConstructors()
                              << ", aci= " << aci << std::endl;
@@ -1056,11 +1055,8 @@ sygusGrammar[CVC4::api::Sort & ret,
     PARSER_STATE->popScope();
     // now, make the sygus datatype
     Trace("parser-sygus2") << "Make the sygus datatypes..." << std::endl;
-    std::set<Type> utypes = api::sortSetToTypes(unresTypes);
-    std::vector<DatatypeType> datatypeTypes =
-        SOLVER->getExprManager()->mkMutualDatatypeTypes(
-            datatypes, utypes,
-            ExprManager::DATATYPE_FLAG_PLACEHOLDER);
+    std::vector<api::Sort> datatypeTypes =
+      SOLVER->mkDatatypeSorts(datatypes, unresTypes);
     // return is the first datatype
     ret = api::Sort(datatypeTypes[0]);
   }
@@ -1244,7 +1240,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
 
 extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
-  std::vector<CVC4::Datatype> dts;
+  std::vector<api::DatatypeDecl> dts;
   CVC4::api::Term e, e2;
   CVC4::api::Sort t;
   std::string name;
@@ -1443,7 +1439,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
 
 datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
-  std::vector<CVC4::Datatype> dts;
+  std::vector<api::DatatypeDecl> dts;
   std::string name;
   std::vector<api::Sort> sorts;
   std::vector<std::string> dnames;
@@ -1462,13 +1458,14 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
   LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
   { PARSER_STATE->popScope();
     cmd->reset(new DatatypeDeclarationCommand(
-      api::sortVectorToTypes(PARSER_STATE->mkMutualDatatypeTypes(dts, true))));
+      api::sortVectorToTypes(
+        PARSER_STATE->bindMutualDatatypeTypes(dts, true))));
   }
   ;
 
 datatypeDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
-  std::vector<CVC4::Datatype> dts;
+  std::vector<api::DatatypeDecl> dts;
   std::string name;
   std::vector<std::string> dnames;
   std::vector<int> arities;
@@ -1484,7 +1481,7 @@ datatypeDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
 
 datatypesDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
-  std::vector<CVC4::Datatype> dts;
+  std::vector<api::DatatypeDecl> dts;
   std::string name;
   std::vector<std::string> dnames;
   std::vector<int> arities;
@@ -1514,7 +1511,7 @@ datatypesDef[bool isCo,
              const std::vector<int>& arities,
              std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
-  std::vector<CVC4::Datatype> dts;
+  std::vector<api::DatatypeDecl> dts;
   std::string name;
   std::vector<api::Sort> params;
 }
@@ -1537,7 +1534,7 @@ datatypesDef[bool isCo,
           PARSER_STATE->parseError("Wrong number of parameters for datatype.");
         }
         Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
-        dts.push_back(Datatype(SOLVER->getExprManager(), dnames[dts.size()],api::sortVectorToTypes(params),isCo));
+        dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()], params, isCo));
       }
       LPAREN_TOK
       ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
@@ -1547,10 +1544,9 @@ datatypesDef[bool isCo,
           PARSER_STATE->parseError("No parameters given for datatype.");
         }
         Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
-        dts.push_back(Datatype(SOLVER->getExprManager(),
-                               dnames[dts.size()],
-                               api::sortVectorToTypes(params),
-                               isCo));
+        dts.push_back(SOLVER->mkDatatypeDecl(dnames[dts.size()],
+                                             params,
+                                             isCo));
       }
       ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
     )
@@ -1559,7 +1555,8 @@ datatypesDef[bool isCo,
   {
     PARSER_STATE->popScope();
     cmd->reset(new DatatypeDeclarationCommand(
-      api::sortVectorToTypes(PARSER_STATE->mkMutualDatatypeTypes(dts, true))));
+      api::sortVectorToTypes(
+        PARSER_STATE->bindMutualDatatypeTypes(dts, true))));
   }
   ;
 
@@ -2521,7 +2518,7 @@ nonemptyNumeralList[std::vector<uint64_t>& numerals]
 /**
  * Parses a datatype definition
  */
-datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes,
+datatypeDef[bool isCo, std::vector<CVC4::api::DatatypeDecl>& datatypes,
             std::vector< CVC4::api::Sort >& params]
 @init {
   std::string id;
@@ -2532,10 +2529,7 @@ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes,
      * below. */
   : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); }
     {
-      datatypes.push_back(Datatype(SOLVER->getExprManager(),
-                                   id,
-                                   api::sortVectorToTypes(params),
-                                   isCo));
+      datatypes.push_back(SOLVER->mkDatatypeDecl(id, params, isCo));
     }
     ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+
     { PARSER_STATE->popScope(); }
@@ -2544,14 +2538,14 @@ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes,
 /**
  * Parses a constructor defintion for type
  */
-constructorDef[CVC4::Datatype& type]
+constructorDef[CVC4::api::DatatypeDecl& type]
 @init {
   std::string id;
-  CVC4::DatatypeConstructor* ctor = NULL;
+  CVC4::api::DatatypeConstructorDecl* ctor = NULL;
 }
   : symbol[id,CHECK_NONE,SYM_VARIABLE]
     {
-      ctor = new CVC4::DatatypeConstructor(id);
+      ctor = new api::DatatypeConstructorDecl(id);
     }
     ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
     { // make the constructor
@@ -2561,13 +2555,14 @@ constructorDef[CVC4::Datatype& type]
     }
   ;
 
-selector[CVC4::DatatypeConstructor& ctor]
+selector[CVC4::api::DatatypeConstructorDecl& ctor]
 @init {
   std::string id;
   CVC4::api::Sort t, t2;
 }
   : symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t,CHECK_NONE]
-    { ctor.addArg(id, t.getType());
+    { 
+      ctor.addSelector(id, t);
       Debug("parser-idt") << "selector: " << id.c_str()
                           << " of type " << t << std::endl;
     }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index d1fbfe969..c30c44362 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -965,7 +965,7 @@ void Smt2::mkSygusConstantsForType(const api::Sort& type,
 void Smt2::processSygusGTerm(
     CVC4::SygusGTerm& sgt,
     int index,
-    std::vector<CVC4::Datatype>& datatypes,
+    std::vector<api::DatatypeDecl>& datatypes,
     std::vector<api::Sort>& sorts,
     std::vector<std::vector<ParseOp>>& ops,
     std::vector<std::vector<std::string>>& cnames,
@@ -1103,7 +1103,7 @@ void Smt2::processSygusGTerm(
 bool Smt2::pushSygusDatatypeDef(
     api::Sort t,
     std::string& dname,
-    std::vector<CVC4::Datatype>& datatypes,
+    std::vector<api::DatatypeDecl>& datatypes,
     std::vector<api::Sort>& sorts,
     std::vector<std::vector<ParseOp>>& ops,
     std::vector<std::vector<std::string>>& cnames,
@@ -1112,7 +1112,7 @@ bool Smt2::pushSygusDatatypeDef(
     std::vector<std::vector<std::string>>& unresolved_gterm_sym)
 {
   sorts.push_back(t);
-  datatypes.push_back(Datatype(d_solver->getExprManager(), dname));
+  datatypes.push_back(d_solver->mkDatatypeDecl(dname));
   ops.push_back(std::vector<ParseOp>());
   cnames.push_back(std::vector<std::string>());
   cargs.push_back(std::vector<std::vector<api::Sort>>());
@@ -1122,7 +1122,7 @@ bool Smt2::pushSygusDatatypeDef(
 }
 
 bool Smt2::popSygusDatatypeDef(
-    std::vector<CVC4::Datatype>& datatypes,
+    std::vector<api::DatatypeDecl>& datatypes,
     std::vector<api::Sort>& sorts,
     std::vector<std::vector<ParseOp>>& ops,
     std::vector<std::vector<std::string>>& cnames,
@@ -1143,7 +1143,7 @@ bool Smt2::popSygusDatatypeDef(
 api::Sort Smt2::processSygusNestedGTerm(
     int sub_dt_index,
     std::string& sub_dname,
-    std::vector<CVC4::Datatype>& datatypes,
+    std::vector<api::DatatypeDecl>& datatypes,
     std::vector<api::Sort>& sorts,
     std::vector<std::vector<ParseOp>>& ops,
     std::vector<std::vector<std::string>>& cnames,
@@ -1238,12 +1238,12 @@ api::Sort Smt2::processSygusNestedGTerm(
 
 void Smt2::setSygusStartIndex(const std::string& fun,
                               int startIndex,
-                              std::vector<CVC4::Datatype>& datatypes,
+                              std::vector<api::DatatypeDecl>& datatypes,
                               std::vector<api::Sort>& sorts,
                               std::vector<std::vector<ParseOp>>& ops)
 {
   if( startIndex>0 ){
-    CVC4::Datatype tmp_dt = datatypes[0];
+    api::DatatypeDecl tmp_dt = datatypes[0];
     api::Sort tmp_sort = sorts[0];
     std::vector<ParseOp> tmp_ops;
     tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() );
@@ -1262,7 +1262,7 @@ void Smt2::setSygusStartIndex(const std::string& fun,
   }
 }
 
-void Smt2::mkSygusDatatype(CVC4::Datatype& dt,
+void Smt2::mkSygusDatatype(api::DatatypeDecl& dt,
                            std::vector<ParseOp>& ops,
                            std::vector<std::string>& cnames,
                            std::vector<std::vector<api::Sort>>& cargs,
@@ -1388,17 +1388,17 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt,
       // ops[i], or the kind.
       if (!ops[i].d_expr.isNull())
       {
-        dt.addSygusConstructor(ops[i].d_expr.getExpr(),
-                               cnames[i],
-                               api::sortVectorToTypes(cargs[i]),
-                               spc);
+        dt.getDatatype().addSygusConstructor(ops[i].d_expr.getExpr(),
+                                             cnames[i],
+                                             api::sortVectorToTypes(cargs[i]),
+                                             spc);
       }
       else if (ops[i].d_kind != api::NULL_EXPR)
       {
-        dt.addSygusConstructor(extToIntKind(ops[i].d_kind),
-                               cnames[i],
-                               api::sortVectorToTypes(cargs[i]),
-                               spc);
+        dt.getDatatype().addSygusConstructor(extToIntKind(ops[i].d_kind),
+                                             cnames[i],
+                                             api::sortVectorToTypes(cargs[i]),
+                                             spc);
       }
       else
       {
@@ -1423,7 +1423,7 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt,
         if( std::find( types.begin(), types.end(), t )==types.end() ){
           types.push_back( t );
           //identity element
-          api::Sort bt = dt.getSygusType();
+          api::Sort bt = dt.getDatatype().getSygusType();
           Debug("parser-sygus") << ":  make identity function for " << bt << ", argument type " << t << std::endl;
 
           std::stringstream ss;
@@ -1441,10 +1441,10 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt,
           //make the sygus argument list
           std::vector<api::Sort> id_carg;
           id_carg.push_back( t );
-          dt.addSygusConstructor(id_op.getExpr(),
-                                 unresolved_gterm_sym[i],
-                                 api::sortVectorToTypes(id_carg),
-                                 sepc);
+          dt.getDatatype().addSygusConstructor(id_op.getExpr(),
+                                               unresolved_gterm_sym[i],
+                                               api::sortVectorToTypes(id_carg),
+                                               sepc);
 
           //add to operators
           ParseOp idOp;
@@ -1460,7 +1460,7 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt,
   }
 }
 
-api::Term Smt2::makeSygusBoundVarList(CVC4::Datatype& dt,
+api::Term Smt2::makeSygusBoundVarList(api::DatatypeDecl& dt,
                                       unsigned i,
                                       const std::vector<api::Sort>& ltypes,
                                       std::vector<api::Term>& lvars)
@@ -1476,7 +1476,7 @@ api::Term Smt2::makeSygusBoundVarList(CVC4::Datatype& dt,
 }
 
 void Smt2::addSygusConstructorTerm(
-    Datatype& dt,
+    api::DatatypeDecl& dt,
     api::Term term,
     std::map<api::Term, api::Sort>& ntsToUnres) const
 {
@@ -1509,7 +1509,7 @@ void Smt2::addSygusConstructorTerm(
   }
   Trace("parser-sygus2") << "addSygusConstructor:  operator " << op
                          << std::endl;
-  dt.addSygusConstructor(
+  dt.getDatatype().addSygusConstructor(
       op.getExpr(), ssCName.str(), api::sortVectorToTypes(cargs), spc);
 }
 
@@ -1552,7 +1552,7 @@ api::Term Smt2::purifySygusGTerm(api::Term term,
   return nret;
 }
 
-void Smt2::addSygusConstructorVariables(Datatype& dt,
+void Smt2::addSygusConstructorVariables(api::DatatypeDecl& dt,
                                         const std::vector<api::Term>& sygusVars,
                                         api::Sort type) const
 {
@@ -1565,7 +1565,7 @@ void Smt2::addSygusConstructorVariables(Datatype& dt,
       std::stringstream ss;
       ss << v;
       std::vector<api::Sort> cargs;
-      dt.addSygusConstructor(
+      dt.getDatatype().addSygusConstructor(
           v.getExpr(), ss.str(), api::sortVectorToTypes(cargs));
     }
   }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index bf4b231b1..6d3c2e6f6 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -355,7 +355,7 @@ class Smt2 : public Parser
   void processSygusGTerm(
       CVC4::SygusGTerm& sgt,
       int index,
-      std::vector<CVC4::Datatype>& datatypes,
+      std::vector<api::DatatypeDecl>& datatypes,
       std::vector<api::Sort>& sorts,
       std::vector<std::vector<ParseOp>>& ops,
       std::vector<std::vector<std::string>>& cnames,
@@ -371,7 +371,7 @@ class Smt2 : public Parser
   bool pushSygusDatatypeDef(
       api::Sort t,
       std::string& dname,
-      std::vector<CVC4::Datatype>& datatypes,
+      std::vector<api::DatatypeDecl>& datatypes,
       std::vector<api::Sort>& sorts,
       std::vector<std::vector<ParseOp>>& ops,
       std::vector<std::vector<std::string>>& cnames,
@@ -380,7 +380,7 @@ class Smt2 : public Parser
       std::vector<std::vector<std::string>>& unresolved_gterm_sym);
 
   bool popSygusDatatypeDef(
-      std::vector<CVC4::Datatype>& datatypes,
+      std::vector<api::DatatypeDecl>& datatypes,
       std::vector<api::Sort>& sorts,
       std::vector<std::vector<ParseOp>>& ops,
       std::vector<std::vector<std::string>>& cnames,
@@ -390,11 +390,11 @@ class Smt2 : public Parser
 
   void setSygusStartIndex(const std::string& fun,
                           int startIndex,
-                          std::vector<CVC4::Datatype>& datatypes,
+                          std::vector<api::DatatypeDecl>& datatypes,
                           std::vector<api::Sort>& sorts,
                           std::vector<std::vector<ParseOp>>& ops);
 
-  void mkSygusDatatype(CVC4::Datatype& dt,
+  void mkSygusDatatype(api::DatatypeDecl& dt,
                        std::vector<ParseOp>& ops,
                        std::vector<std::string>& cnames,
                        std::vector<std::vector<api::Sort>>& cargs,
@@ -415,7 +415,7 @@ class Smt2 : public Parser
    * via a lambda.
    */
   void addSygusConstructorTerm(
-      Datatype& dt,
+      api::DatatypeDecl& dt,
       api::Term term,
       std::map<api::Term, api::Sort>& ntsToUnres) const;
   /**
@@ -423,7 +423,7 @@ class Smt2 : public Parser
    * type is argument type. This method should be called when the sygus grammar
    * term (Variable type) is encountered.
    */
-  void addSygusConstructorVariables(Datatype& dt,
+  void addSygusConstructorVariables(api::DatatypeDecl& dt,
                                     const std::vector<api::Term>& sygusVars,
                                     api::Sort type) const;
 
@@ -541,7 +541,7 @@ class Smt2 : public Parser
   api::Sort processSygusNestedGTerm(
       int sub_dt_index,
       std::string& sub_dname,
-      std::vector<CVC4::Datatype>& datatypes,
+      std::vector<api::DatatypeDecl>& datatypes,
       std::vector<api::Sort>& sorts,
       std::vector<std::vector<ParseOp>>& ops,
       std::vector<std::vector<std::string>>& cnames,
@@ -560,7 +560,7 @@ class Smt2 : public Parser
    * It appends a bound variable to lvars for each type in ltypes, and returns
    * a bound variable list whose children are lvars.
    */
-  api::Term makeSygusBoundVarList(CVC4::Datatype& dt,
+  api::Term makeSygusBoundVarList(api::DatatypeDecl& dt,
                                   unsigned i,
                                   const std::vector<api::Sort>& ltypes,
                                   std::vector<api::Term>& lvars);