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, 9 insertions, 9 deletions

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);