diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-06 10:18:39 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-06 10:18:39 -0600 |
| commit | f3a773dc772cc3ef0590f01e7ce2ebe0ce87bfd3 (patch) | |
| tree | fdbdbcc5abb5953df9316404db4f4b7674319b03 /src/parser/smt2 | |
| parent | 210e6db5c6a76ee1e554426058ecf3397575f1e3 (diff) | |
Make sygus datatype building independent of parser in sygus v2 (#3923)
The current sygus v2 called the parser's mkMututalDatatypeTypes function, which unecessarily created the datatype and bound its (internally generated) constructor/selector symbols in the symbol tables of the parser. This resolves this dependency.
The same issue also exists in the sygus v1 parser but is harder to resolve; I am leaving this for now since that code will be deleted in the next version of CVC4.
This is work towards the SyGuS API.
Diffstat (limited to 'src/parser/smt2')
| -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]; } |