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.

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index e3d0e0696694c9b3d5d222a4a1bf8a23ac4f2801..64eb56c74db67a8727a22478f8940bcbb1307445 100644 (file)
--- 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 f4ea6d56cacace6452ababde61f2f9d19d4132c3..87fa93dcc4758c72daf9caeaa9107a867233284f 100644 (file)
--- 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 3237c28937f1799008a56618125cf0290d64f259..c7efcbacb94b46544a2e486b1c8e922fdcb5e5d5 100644 (file)
--- 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 d1544f03cc02cf0cb6c7f000cb0601dc17d4e260..aa62eab5db6608e1b45c14ffb4f04e08fe80036e 100644 (file)
--- 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))));
   }
   ;
 

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 1e6604d24a4153369e9c12067ff8c103dab3ea35..c59d8f32845cf4c1c11fdd3d13324e09cfc8399b 100644 (file)
--- 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 3120fe8f127ba28872516b8ae5ce5e6d93e3aa2c..86dd31da2f4e0d238d7508cb96f032793d022dc2 100644 (file)
--- 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 0334c97b6b54e8e27057b6ac8eff833cdc0b44ef..ed4d3f5dc0f3a2e1e22bffceff634f70d6a9047e 100644 (file)
--- 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 << ")";

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index c1aa89832ef918aa516c731d5bd72bb771db1256..79cc465ac5b76f34b76697478918aa3618d52ce3 100644 (file)
--- 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 19b858bd6a8803a0b286b41c45b2fc7c222826b3..63f1f0f33c083620498530c056b8730e5ddece5d 100644 (file)
--- 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 43459dcec62def23188faa60eae7b14b03e63c08..180b33fe010474775406321515854a24f6158241 100644 (file)
--- 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);
     }
   }