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, 40 insertions, 41 deletions

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 1e6604d24..c59d8f328 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -391,13 +391,11 @@ static void toStream(std::ostream& out, const GetOptionCommand* c)
 
 static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c)
 {
-  const vector<DatatypeType>& datatypes = c->getDatatypes();
+  const vector<Type>& datatypes = c->getDatatypes();
   out << "DatatypeDeclarationCommand([";
-  for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
-        i_end = datatypes.end();
-      i != i_end;
-      ++i) {
-    out << *i << ";" << endl;
+  for (const Type& t : datatypes)
+  {
+    out << t << ";" << endl;
   }
   out << "])";
 }
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 3120fe8f1..86dd31da2 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1465,19 +1465,20 @@ static void toStream(std::ostream& out,
                      const DatatypeDeclarationCommand* c,
                      bool cvc3Mode)
 {
-  const vector<DatatypeType>& datatypes = c->getDatatypes();
+  const vector<Type>& datatypes = c->getDatatypes();
+  Assert(!datatypes.empty() && datatypes[0].isDatatype());
+  const Datatype& dt0 = DatatypeType(datatypes[0]).getDatatype();
   //do not print tuple/datatype internal declarations
-  if( datatypes.size()!=1 || ( !datatypes[0].getDatatype().isTuple() && !datatypes[0].getDatatype().isRecord() ) ){
+  if (datatypes.size() != 1 || (!dt0.isTuple() && !dt0.isRecord()))
+  {
     out << "DATATYPE" << endl;
     bool firstDatatype = true;
-    for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
-          i_end = datatypes.end();
-        i != i_end;
-        ++i) {
+    for (const Type& t : datatypes)
+    {
       if(! firstDatatype) {
         out << ',' << endl;
       }
-      const Datatype& dt = (*i).getDatatype();
+      const Datatype& dt = DatatypeType(t).getDatatype();
       out << "  " << dt.getName();
       if(dt.isParametric()) {
         out << '[';
@@ -1511,12 +1512,15 @@ static void toStream(std::ostream& out,
             }
             firstSelector = false;
             const DatatypeConstructorArg& selector = *k;
-            Type t = SelectorType(selector.getType()).getRangeType();
-            if( t.isDatatype() ){
-              const Datatype & sdt = ((DatatypeType)t).getDatatype();
+            Type tr = SelectorType(selector.getType()).getRangeType();
+            if (tr.isDatatype())
+            {
+              const Datatype& sdt = DatatypeType(tr).getDatatype();
               out << selector.getName() << ": " << sdt.getName();
-            }else{
-              out << selector.getName() << ": " << t;
+            }
+            else
+            {
+              out << selector.getName() << ": " << tr;
             }
           }
           out << ')';
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 0334c97b6..ed4d3f5dc 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1921,16 +1921,19 @@ static void toStream(std::ostream& out,
                      const DatatypeDeclarationCommand* c,
                      Variant v)
 {
-  const vector<DatatypeType>& datatypes = c->getDatatypes();
+  const std::vector<Type>& datatypes = c->getDatatypes();
   Assert(!datatypes.empty());
-  if (datatypes[0].getDatatype().isTuple())
+  Assert(datatypes[0].isDatatype());
+  DatatypeType dt0 = DatatypeType(datatypes[0]);
+  const Datatype& d0 = dt0.getDatatype();
+  if (d0.isTuple())
   {
     // not necessary to print tuples
     Assert(datatypes.size() == 1);
     return;
   }
   out << "(declare-";
-  if (datatypes[0].getDatatype().isCodatatype())
+  if (d0.isCodatatype())
   {
     out << "co";
   }
@@ -1938,22 +1941,18 @@ static void toStream(std::ostream& out,
   if (isVariant_2_6(v))
   {
     out << " (";
-    for (vector<DatatypeType>::const_iterator i = datatypes.begin(),
-                                              i_end = datatypes.end();
-         i != i_end;
-         ++i)
+    for (const Type& t : datatypes)
     {
-      const Datatype& d = i->getDatatype();
+      Assert(t.isDatatype());
+      const Datatype& d = DatatypeType(t).getDatatype();
       out << "(" << CVC4::quoteSymbol(d.getName());
       out << " " << d.getNumParameters() << ")";
     }
     out << ") (";
-    for (vector<DatatypeType>::const_iterator i = datatypes.begin(),
-                                              i_end = datatypes.end();
-         i != i_end;
-         ++i)
+    for (const Type& t : datatypes)
     {
-      const Datatype& d = i->getDatatype();
+      Assert(t.isDatatype());
+      const Datatype& d = DatatypeType(t).getDatatype();
       if (d.isParametric())
       {
         out << "(par (";
@@ -1981,11 +1980,11 @@ static void toStream(std::ostream& out,
     // be impossible to print a datatype block where datatypes were given
     // different parameter lists.
     bool success = true;
-    const Datatype& d = datatypes[0].getDatatype();
-    unsigned nparam = d.getNumParameters();
+    unsigned nparam = d0.getNumParameters();
     for (unsigned j = 1, ndt = datatypes.size(); j < ndt; j++)
     {
-      const Datatype& dj = datatypes[j].getDatatype();
+      Assert(datatypes[j].isDatatype());
+      const Datatype& dj = DatatypeType(datatypes[j]).getDatatype();
       if (dj.getNumParameters() != nparam)
       {
         success = false;
@@ -1995,7 +1994,7 @@ static void toStream(std::ostream& out,
         // must also have identical parameter lists
         for (unsigned k = 0; k < nparam; k++)
         {
-          if (dj.getParameter(k) != d.getParameter(k))
+          if (dj.getParameter(k) != d0.getParameter(k))
           {
             success = false;
             break;
@@ -2011,7 +2010,7 @@ static void toStream(std::ostream& out,
     {
       for (unsigned j = 0; j < nparam; j++)
       {
-        out << (j > 0 ? " " : "") << d.getParameter(j);
+        out << (j > 0 ? " " : "") << d0.getParameter(j);
       }
     }
     else
@@ -2022,12 +2021,10 @@ static void toStream(std::ostream& out,
       out << std::endl;
     }
     out << ") (";
-    for (vector<DatatypeType>::const_iterator i = datatypes.begin(),
-                                              i_end = datatypes.end();
-         i != i_end;
-         ++i)
+    for (const Type& t : datatypes)
     {
-      const Datatype& dt = i->getDatatype();
+      Assert(t.isDatatype());
+      const Datatype& dt = DatatypeType(t).getDatatype();
       out << "(" << CVC4::quoteSymbol(dt.getName()) << " ";
       toStream(out, dt);
       out << ")";