From 75502e8c943d747df6c9d10a237238e8443d6c38 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 6 Mar 2020 15:55:21 -0600 Subject: [PATCH] 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. --- src/parser/cvc/Cvc.g | 2 +- src/parser/parser.cpp | 9 ++----- src/parser/parser.h | 2 +- src/parser/smt2/Smt2.g | 10 ++++--- src/printer/ast/ast_printer.cpp | 10 +++---- src/printer/cvc/cvc_printer.cpp | 28 +++++++++++--------- src/printer/smt2/smt2_printer.cpp | 43 ++++++++++++++----------------- src/smt/command.cpp | 9 +++---- src/smt/command.h | 8 +++--- src/smt/smt_engine.cpp | 3 ++- 10 files changed, 60 insertions(+), 64 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* 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 Parser::mkMutualDatatypeTypes( +std::vector Parser::mkMutualDatatypeTypes( std::vector& datatypes, bool doOverload, uint32_t flags) { try { @@ -491,12 +491,7 @@ std::vector Parser::mkMutualDatatypeTypes( throw ParserException(dt.getName() + " is not well-founded"); } } - std::vector 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 mkMutualDatatypeTypes( + std::vector mkMutualDatatypeTypes( std::vector& 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 datatypeTypes = + std::vector 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* 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 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& datatypes = c->getDatatypes(); + const vector& datatypes = c->getDatatypes(); out << "DatatypeDeclarationCommand(["; - for(vector::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& datatypes = c->getDatatypes(); + const vector& 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::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& datatypes = c->getDatatypes(); + const std::vector& 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::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::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::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 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& datatypes) + const std::vector& datatypes) : d_datatypes(datatypes) { } -const std::vector& DatatypeDeclarationCommand::getDatatypes() - const +const std::vector& 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 d_datatypes; + std::vector d_datatypes; public: - DatatypeDeclarationCommand(const DatatypeType& datatype); + DatatypeDeclarationCommand(const Type& datatype); - DatatypeDeclarationCommand(const std::vector& datatypes); - const std::vector& getDatatypes() const; + DatatypeDeclarationCommand(const std::vector& datatypes); + const std::vector& 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 types(dtts.begin(), dtts.end()); + DatatypeDeclarationCommand c(types); d_smt.addToModelCommandAndDump(c); } } -- 2.30.2