diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-06 15:55:21 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-06 15:55:21 -0600 |
commit | 75502e8c943d747df6c9d10a237238e8443d6c38 (patch) | |
tree | 75cccccebb1819680f43cc5a9c16194e511a4ac4 /src/parser | |
parent | 89337334236176bff2d561c42b9b55ab9d91bd62 (diff) |
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.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 2 | ||||
-rw-r--r-- | src/parser/parser.cpp | 9 | ||||
-rw-r--r-- | src/parser/parser.h | 2 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 10 |
4 files changed, 10 insertions, 13 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<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 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<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 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<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 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<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)))); } ; |