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, 4 insertions, 11 deletions

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