Simplify DatatypeDeclarationCommand command (#3928)

The new API does not use inheritence for Sorts. The current DatatypeDeclarationCommand uses DatatypeType, which inherits from Type. This commit simplifies the class DatatypeType -> Type and updates the necessary code (e.g. in the printers). Notice we are not yet converting commands Type -> Sort here.

It also makes the main call for constructing datatypes in the parser from DatatypeType -> api::Sort.

This is in preparation for converting Expr-level Datatype to Term-level DatatypeDecl in the parsers.

4 files changed, 10 insertions, 13 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index e3d0e0696..64eb56c74 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -757,7 +757,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
     END_TOK
     { PARSER_STATE->popScope();
       cmd->reset(new DatatypeDeclarationCommand(
-          PARSER_STATE->mkMutualDatatypeTypes(dts)));
+          api::sortVectorToTypes(PARSER_STATE->mkMutualDatatypeTypes(dts))));
     }
 
   | CONTEXT_TOK
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index f4ea6d56c..87fa93dcc 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -398,7 +398,7 @@ bool Parser::isUnresolvedType(const std::string& name) {
   return d_unresolved.find(getSort(name)) != d_unresolved.end();
 }
 
-std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
+std::vector<api::Sort> Parser::mkMutualDatatypeTypes(
     std::vector<Datatype>& datatypes, bool doOverload, uint32_t flags)
 {
   try {
@@ -491,12 +491,7 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
         throw ParserException(dt.getName() + " is not well-founded");
       }
     }
-    std::vector<DatatypeType> retTypes;
-    for (unsigned i = 0, ntypes = types.size(); i < ntypes; i++)
-    {
-      retTypes.push_back(DatatypeType(types[i].getType()));
-    }
-    return retTypes;
+    return types;
   } catch (IllegalArgumentException& ie) {
     throw ParserException(ie.getMessage());
   }
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 3237c2893..c7efcbacb 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -604,7 +604,7 @@ public:
    * printed out as a definition in models or not
    *   (see enum in expr_manager_template.h).
    */
-  std::vector<DatatypeType> mkMutualDatatypeTypes(
+  std::vector<api::Sort> mkMutualDatatypeTypes(
       std::vector<Datatype>& datatypes,
       bool doOverload = false,
       uint32_t flags = ExprManager::DATATYPE_FLAG_NONE);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d1544f03c..aa62eab5d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -788,7 +788,7 @@ sygusGrammarV1[CVC4::api::Sort & ret,
       Debug("parser-sygus") << "  " << i << " : " << datatypes[i].getName()
                             << std::endl;
     }
-    std::vector<DatatypeType> datatypeTypes =
+    std::vector<api::Sort> datatypeTypes =
         PARSER_STATE->mkMutualDatatypeTypes(
             datatypes, false, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
     ret = datatypeTypes[0];
@@ -1062,7 +1062,7 @@ sygusGrammar[CVC4::api::Sort & ret,
             datatypes, utypes,
             ExprManager::DATATYPE_FLAG_PLACEHOLDER);
     // return is the first datatype
-    ret = datatypeTypes[0];
+    ret = api::Sort(datatypeTypes[0]);
   }
 ;
 
@@ -1461,7 +1461,8 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
   RPAREN_TOK
   LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
   { PARSER_STATE->popScope();
-    cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts, true)));
+    cmd->reset(new DatatypeDeclarationCommand(
+      api::sortVectorToTypes(PARSER_STATE->mkMutualDatatypeTypes(dts, true))));
   }
   ;
 
@@ -1557,7 +1558,8 @@ datatypesDef[bool isCo,
     )+
   {
     PARSER_STATE->popScope();
-    cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts, true)));
+    cmd->reset(new DatatypeDeclarationCommand(
+      api::sortVectorToTypes(PARSER_STATE->mkMutualDatatypeTypes(dts, true))));
   }
   ;