diff options
Diffstat (limited to 'src/parser')
| -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 cd661364d..14396c771 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -943,7 +943,7 @@ sygusGrammar[CVC4::api::Sort & ret, std::string name; CVC4::api::Term e, e2; std::vector<CVC4::Datatype> datatypes; - std::vector<api::Sort> unresTypes; + std::set<api::Sort> unresTypes; std::map<CVC4::api::Term, CVC4::api::Sort> ntsToUnres; unsigned dtProcessed = 0; std::unordered_set<unsigned> allowConst; @@ -964,7 +964,7 @@ sygusGrammar[CVC4::api::Sort & ret, // the datatype PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); api::Sort urt = PARSER_STATE->mkUnresolvedType(dname); - unresTypes.push_back(urt); + unresTypes.insert(urt); // make the non-terminal symbol, which will be parsed as an ordinary // free variable. api::Term nts = PARSER_STATE->bindBoundVar(i.first, i.second); @@ -1056,9 +1056,11 @@ sygusGrammar[CVC4::api::Sort & ret, PARSER_STATE->popScope(); // now, make the sygus datatype Trace("parser-sygus2") << "Make the sygus datatypes..." << std::endl; + std::set<Type> utypes = api::sortSetToTypes(unresTypes); std::vector<DatatypeType> datatypeTypes = - PARSER_STATE->mkMutualDatatypeTypes( - datatypes, false, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + SOLVER->getExprManager()->mkMutualDatatypeTypes( + datatypes, utypes, + ExprManager::DATATYPE_FLAG_PLACEHOLDER); // return is the first datatype ret = datatypeTypes[0]; } |