diff options
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)))); } ; |