From c4f2ca4c1931f91a9647f0daa032ee9417f1b382 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Mon, 24 Feb 2020 14:30:02 -0600 Subject: 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. --- src/parser/smt2/Smt2.g | 25 ++++------- src/parser/smt2/smt2.cpp | 3 +- src/printer/smt2/smt2_printer.cpp | 94 ++++++++++++++++----------------------- src/smt/smt_engine.cpp | 35 ++++++++++----- 4 files changed, 71 insertions(+), 86 deletions(-) (limited to 'src') 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()); 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 diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a7033b277..7b7e9dd82 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -172,7 +172,8 @@ void Smt2::addStringOperators() { addOperator(kind::STRING_PREFIX, "str.prefixof" ); addOperator(kind::STRING_SUFFIX, "str.suffixof" ); // at the moment, we only use this syntax for smt2.6.1 - if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1) + if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1 + || getLanguage() == language::input::LANG_SYGUS_V2) { addOperator(kind::STRING_ITOS, "str.from_int"); addOperator(kind::STRING_STOI, "str.to_int"); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8153d6856..07422cd8b 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -128,6 +128,7 @@ void Smt2Printer::toStream(std::ostream& out, case REAL_TYPE: out << "Real"; break; case INTEGER_TYPE: out << "Int"; break; case STRING_TYPE: out << "String"; break; + case REGEXP_TYPE: out << "RegLan"; break; case ROUNDINGMODE_TYPE: out << "RoundingMode"; break; default: // fall back on whatever operator<< does on underlying type; we @@ -1206,7 +1207,8 @@ static string smtKindString(Kind k, Variant v) case kind::STRING_CHARAT: return "str.at" ; case kind::STRING_STRIDOF: return "str.indexof" ; case kind::STRING_STRREPL: return "str.replace" ; - case kind::STRING_STRREPLALL: return "str.replaceall"; + case kind::STRING_STRREPLALL: + return v == smt2_6_1_variant ? "str.replace_all" : "str.replaceall"; case kind::STRING_TOLOWER: return "str.tolower"; case kind::STRING_TOUPPER: return "str.toupper"; case kind::STRING_REV: return "str.rev"; @@ -1214,15 +1216,16 @@ static string smtKindString(Kind k, Variant v) case kind::STRING_SUFFIX: return "str.suffixof" ; case kind::STRING_LEQ: return "str.<="; case kind::STRING_LT: return "str.<"; - case kind::STRING_CODE: return "str.code"; + case kind::STRING_CODE: + return v == smt2_6_1_variant ? "str.to_code" : "str.code"; case kind::STRING_ITOS: - return v == smt2_6_1_variant ? "str.from-int" : "int.to.str"; + return v == smt2_6_1_variant ? "str.from_int" : "int.to.str"; case kind::STRING_STOI: - return v == smt2_6_1_variant ? "str.to-int" : "str.to.int"; + return v == smt2_6_1_variant ? "str.to_int" : "str.to.int"; case kind::STRING_IN_REGEXP: - return v == smt2_6_1_variant ? "str.in-re" : "str.in.re"; + return v == smt2_6_1_variant ? "str.in_re" : "str.in.re"; case kind::STRING_TO_REGEXP: - return v == smt2_6_1_variant ? "str.to-re" : "str.to.re"; + return v == smt2_6_1_variant ? "str.to_re" : "str.to.re"; case kind::REGEXP_EMPTY: return "re.nostr"; case kind::REGEXP_SIGMA: return "re.allchar"; case kind::REGEXP_CONCAT: return "re.++"; @@ -2071,25 +2074,23 @@ static void toStream(std::ostream& out, const SynthFunCommand* c) Type type = c->getFunction().getType(); const std::vector& vars = c->getVars(); Assert(!type.isFunction() || !vars.empty()); - c->getCommandName(); + out << '('; if (type.isFunction()) { // print variable list std::vector::const_iterator i = vars.begin(), i_end = vars.end(); Assert(i != i_end); - out << '('; - do + out << '(' << *i << ' ' << i->getType() << ')'; + ++i; + while (i != i_end) { - out << '(' << *i << ' ' << (*i).getType() << ')'; - if (++i != i_end) - { - out << ' '; - } - } while (i != i_end); - out << ')'; + out << " (" << *i << ' ' << i->getType() << ')'; + ++i; + } FunctionType ft = type; type = ft.getRangeType(); } + out << ')'; // if not invariant-to-synthesize, print return type if (!c->isInv()) { @@ -2105,6 +2106,7 @@ static void toStream(std::ostream& out, const SynthFunCommand* c) std::list typesToPrint; grammarTypes.insert(sygusType); typesToPrint.push_back(sygusType); + NodeManager* nm = NodeManager::currentNM(); // for each datatype in grammar // name // sygus type @@ -2118,61 +2120,41 @@ static void toStream(std::ostream& out, const SynthFunCommand* c) Assert(curr.isDatatype() && static_cast(curr).getDatatype().isSygus()); const Datatype& dt = static_cast(curr).getDatatype(); - types_list << "(" << dt.getName() << " " << dt.getSygusType() << "\n("; - types_predecl << "(" << dt.getName() << " " << dt.getSygusType() << ")"; + types_list << '(' << dt.getName() << ' ' << dt.getSygusType() << " ("; + types_predecl << '(' << dt.getName() << ' ' << dt.getSygusType() << ") "; if (dt.getSygusAllowConst()) { types_list << "(Constant " << dt.getSygusType() << ") "; } for (const DatatypeConstructor& cons : dt) { - DatatypeConstructor::const_iterator i = cons.begin(), - i_end = cons.end(); - if (i != i_end) + // make a sygus term + std::vector cchildren; + cchildren.push_back(Node::fromExpr(cons.getConstructor())); + for (const DatatypeConstructorArg& i : cons) { - types_list << "("; - SygusPrintCallback* spc = cons.getSygusPrintCallback().get(); - if (spc != nullptr && options::sygusPrintCallbacks()) + Type argType = i.getRangeType(); + std::stringstream ss; + ss << argType; + Node bv = nm->mkBoundVar(ss.str(), TypeNode::fromType(argType)); + cchildren.push_back(bv); + // if fresh type, store it for later processing + if (grammarTypes.insert(argType).second) { - spc->toStreamSygus(sygus_printer, types_list, cons.getSygusOp()); - } - else - { - types_list << cons.getSygusOp(); - } - do - { - Type argType = (*i).getRangeType(); - // print argument type - types_list << " " << argType; - // if fresh type, store it for later processing - if (grammarTypes.insert(argType).second) - { - typesToPrint.push_back(argType); - } - } while (++i != i_end); - types_list << ")"; - } - else - { - SygusPrintCallback* spc = cons.getSygusPrintCallback().get(); - if (spc != nullptr && options::sygusPrintCallbacks()) - { - spc->toStreamSygus(sygus_printer, types_list, cons.getSygusOp()); - } - else - { - types_list << cons.getSygusOp(); + typesToPrint.push_back(argType); } } - types_list << "\n"; + Node consToPrint = nm->mkNode(kind::APPLY_CONSTRUCTOR, cchildren); + // now, print it + sygus_printer->toStreamSygus(types_list, consToPrint); + types_list << ' '; } types_list << "))\n"; } while (!typesToPrint.empty()); - out << "\n(" << types_predecl.str() << ")\n(" << types_list.str() << ")"; + out << "\n(" << types_predecl.str() << ")\n(" << types_list.str() << ')'; } - out << ")"; + out << ')'; } static void toStream(std::ostream& out, const DeclareSygusFunctionCommand* c) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2dc20cc31..6f40d815f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -963,16 +963,18 @@ void SmtEngine::finishInit() d_assertionList = new(true) AssertionList(d_userContext); } - // dump out a set-logic command - if(Dump.isOn("benchmark")) { - if (Dump.isOn("raw-benchmark")) { - Dump("raw-benchmark") << SetBenchmarkLogicCommand(d_logic.getLogicString()); - } else { + // dump out a set-logic command only when raw-benchmark is disabled to avoid + // dumping the command twice. + if (Dump.isOn("benchmark") && !Dump.isOn("raw-benchmark")) + { LogicInfo everything; everything.lock(); - Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, all-supported logic (below), as some internals might require the use of a logic more general than the input.") - << SetBenchmarkLogicCommand(everything.getLogicString()); - } + Dump("benchmark") << CommentCommand( + "CVC4 always dumps the most general, all-supported logic (below), as " + "some internals might require the use of a logic more general than " + "the input.") + << SetBenchmarkLogicCommand( + everything.getLogicString()); } Trace("smt-debug") << "Dump declaration commands..." << std::endl; @@ -1128,9 +1130,18 @@ void SmtEngine::setLogic(const LogicInfo& logic) void SmtEngine::setLogic(const std::string& s) { SmtScope smts(this); - try { + try + { setLogic(LogicInfo(s)); - } catch(IllegalArgumentException& e) { + // dump out a set-logic command + if (Dump.isOn("raw-benchmark")) + { + Dump("raw-benchmark") + << SetBenchmarkLogicCommand(d_logic.getLogicString()); + } + } + catch (IllegalArgumentException& e) + { throw LogicException(e.what()); } } @@ -3937,7 +3948,6 @@ void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type) { // do nothing (the command is spurious) Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n"; - Dump("raw-benchmark") << DeclareSygusPrimedVarCommand(id, type); // don't need to set that the conjecture is stale } @@ -3947,7 +3957,8 @@ void SmtEngine::declareSygusFunctionVar(const std::string& id, { d_private->d_sygusVars.push_back(Node::fromExpr(var)); Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n"; - Dump("raw-benchmark") << DeclareSygusFunctionCommand(id, var, type); + Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type); + // don't need to set that the conjecture is stale } -- cgit v1.2.3