diff options
| -rw-r--r-- | src/parser/smt2/Smt2.g | 25 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 3 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 94 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 35 |
4 files changed, 71 insertions, 86 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 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<Expr>& vars = c->getVars(); Assert(!type.isFunction() || !vars.empty()); - c->getCommandName(); + out << '('; if (type.isFunction()) { // print variable list std::vector<Expr>::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<Type> 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<DatatypeType>(curr).getDatatype().isSygus()); const Datatype& dt = static_cast<DatatypeType>(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<Node> 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 } |