diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 25 |
1 files changed, 8 insertions, 17 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 6a045797a..e1f8031da 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -673,17 +673,14 @@ sygusGrammarV1[CVC4::Type & ret, : LPAREN_TOK { PARSER_STATE->pushScope(); } (LPAREN_TOK symbol[name, CHECK_NONE, SYM_VARIABLE] sortSymbol[t, CHECK_DECLARED] { - std::stringstream ss; - ss << fun << "_" << name; if (name == "Start") { startIndex = datatypes.size(); } - std::string dname = ss.str(); sgts.push_back(std::vector<CVC4::SygusGTerm>()); sgts.back().push_back(CVC4::SygusGTerm()); PARSER_STATE->pushSygusDatatypeDef(t, - dname, + name, datatypes, sorts, ops, @@ -692,18 +689,18 @@ sygusGrammarV1[CVC4::Type & ret, allow_const, unresolved_gterm_sym); Type unres_t; - if (!PARSER_STATE->isUnresolvedType(dname)) + if (!PARSER_STATE->isUnresolvedType(name)) { // if not unresolved, must be undeclared - Debug("parser-sygus") << "Make unresolved type : " << dname + Debug("parser-sygus") << "Make unresolved type : " << name << std::endl; - PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); - unres_t = PARSER_STATE->mkUnresolvedType(dname); + PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT); + unres_t = PARSER_STATE->mkUnresolvedType(name); } else { - Debug("parser-sygus") << "Get sort : " << dname << std::endl; - unres_t = PARSER_STATE->getSort(dname); + Debug("parser-sygus") << "Get sort : " << name << std::endl; + unres_t = PARSER_STATE->getSort(name); } sygus_to_builtin[unres_t] = t; Debug("parser-sygus") << "--- Read sygus grammar " << name @@ -899,10 +896,6 @@ sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun] sgt.d_name = name; sgt.d_gterm_type = SygusGTerm::gterm_op; }else{ - //prepend function name to base sorts when reading an operator - std::stringstream ss; - ss << fun << "_" << name; - name = ss.str(); if( PARSER_STATE->isDeclared(name, SYM_SORT) ){ Debug("parser-sygus") << "Sygus grammar " << fun << " : nested sort " << name << std::endl; @@ -957,9 +950,7 @@ sygusGrammar[CVC4::Type & ret, { Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl; // make the datatype, which encodes terms generated by this non-terminal - std::stringstream ss; - ss << "dt_" << fun << "_" << i.first; - std::string dname = ss.str(); + std::string dname = i.first; datatypes.push_back(Datatype(EXPR_MANAGER, dname)); // make its unresolved type, used for referencing the final version of // the datatype |