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.

1 files changed, 16 insertions, 12 deletions

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