diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 10 |
1 files changed, 6 insertions, 4 deletions
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)))); } ; |