diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-02-24 14:30:02 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-24 14:30:02 -0600 |
| commit | c4f2ca4c1931f91a9647f0daa032ee9417f1b382 (patch) | |
| tree | a2396581d7de09b033fd44c8f7ad3310280bd5f6 /src/parser/smt2/Smt2.g | |
| parent | 90fe2a057cdcdaea34f0a03f837159d9adb45914 (diff) | |
Fix bugs related to printing Sygus commands (#3804)
With this commit, most Sygus problems should print correctly. The current printing functionality was tested on 158 Sygus regress files (0, 1, and 2) and 153 of them were printed in Sygus2 format and contained "(check-synth)". The printing functionality was tested again on the generated files and gave almost the same results.
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 |