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.

3 files changed, 10 insertions, 10 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index c1aa89832..79cc465ac 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -27,6 +27,7 @@
 #include "base/output.h"
 #include "expr/expr_iomanip.h"
 #include "expr/node.h"
+#include "expr/type.h"
 #include "options/options.h"
 #include "options/smt_options.h"
 #include "printer/printer.h"
@@ -2783,21 +2784,19 @@ std::string SetExpressionNameCommand::getCommandName() const
 /* class DatatypeDeclarationCommand                                           */
 /* -------------------------------------------------------------------------- */
 
-DatatypeDeclarationCommand::DatatypeDeclarationCommand(
-    const DatatypeType& datatype)
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(const Type& datatype)
     : d_datatypes()
 {
   d_datatypes.push_back(datatype);
 }
 
 DatatypeDeclarationCommand::DatatypeDeclarationCommand(
-    const std::vector<DatatypeType>& datatypes)
+    const std::vector<Type>& datatypes)
     : d_datatypes(datatypes)
 {
 }
 
-const std::vector<DatatypeType>& DatatypeDeclarationCommand::getDatatypes()
-    const
+const std::vector<Type>& DatatypeDeclarationCommand::getDatatypes() const
 {
   return d_datatypes;
 }
diff --git a/src/smt/command.h b/src/smt/command.h
index 19b858bd6..63f1f0f33 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1301,13 +1301,13 @@ class CVC4_PUBLIC SetExpressionNameCommand : public Command
 class CVC4_PUBLIC DatatypeDeclarationCommand : public Command
 {
  private:
-  std::vector<DatatypeType> d_datatypes;
+  std::vector<Type> d_datatypes;
 
  public:
-  DatatypeDeclarationCommand(const DatatypeType& datatype);
+  DatatypeDeclarationCommand(const Type& datatype);
 
-  DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes);
-  const std::vector<DatatypeType>& getDatatypes() const;
+  DatatypeDeclarationCommand(const std::vector<Type>& datatypes);
+  const std::vector<Type>& getDatatypes() const;
   void invoke(SmtEngine* smtEngine) override;
   Command* exportTo(ExprManager* exprManager,
                     ExprManagerMapCollection& variableMap) override;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 43459dcec..180b33fe0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -683,7 +683,8 @@ class SmtEnginePrivate : public NodeManagerListener {
   {
     if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0)
     {
-      DatatypeDeclarationCommand c(dtts);
+      std::vector<Type> types(dtts.begin(), dtts.end());
+      DatatypeDeclarationCommand c(types);
       d_smt.addToModelCommandAndDump(c);
     }
   }