From ed27cf0f854e014922f9690d967c5ff9aa73693c Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Mon, 17 Feb 2020 08:58:42 -0600 Subject: [PATCH] Support dumping Sygus commands. (#3763) --- src/parser/parser.cpp | 5 +- src/parser/parser.h | 10 +- src/parser/smt2/Smt2.g | 6 +- src/printer/smt2/smt2_printer.cpp | 184 +++++++++++++++++++++++++++++- src/smt/smt_engine.cpp | 41 +++---- 5 files changed, 215 insertions(+), 31 deletions(-) diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index af193c04b..681b2a1c9 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -368,10 +368,11 @@ bool Parser::isUnresolvedType(const std::string& name) { } std::vector Parser::mkMutualDatatypeTypes( - std::vector& datatypes, bool doOverload) { + std::vector& datatypes, bool doOverload, uint32_t flags) +{ try { std::vector types = - getExprManager()->mkMutualDatatypeTypes(datatypes, d_unresolved); + getExprManager()->mkMutualDatatypeTypes(datatypes, d_unresolved, flags); assert(datatypes.size() == types.size()); diff --git a/src/parser/parser.h b/src/parser/parser.h index b0ef2328f..2317835ff 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -602,9 +602,15 @@ public: * For each symbol defined by the datatype, if a symbol with name already exists, * then if doOverload is true, we create overloaded operators. * else if doOverload is false, the existing expression is shadowed by the new expression. + * + * flags specify information about the datatype, e.g. whether it should be + * printed out as a definition in models or not + * (see enum in expr_manager_template.h). */ - std::vector - mkMutualDatatypeTypes(std::vector& datatypes, bool doOverload=false); + std::vector mkMutualDatatypeTypes( + std::vector& datatypes, + bool doOverload = false, + uint32_t flags = ExprManager::DATATYPE_FLAG_NONE); /** make flat function type * diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 90303dd40..3a6b444cc 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -784,7 +784,8 @@ sygusGrammarV1[CVC4::Type & ret, << std::endl; } std::vector datatypeTypes = - PARSER_STATE->mkMutualDatatypeTypes(datatypes); + PARSER_STATE->mkMutualDatatypeTypes( + datatypes, false, ExprManager::DATATYPE_FLAG_PLACEHOLDER); ret = datatypeTypes[0]; }; @@ -1068,7 +1069,8 @@ sygusGrammar[CVC4::Type & ret, // now, make the sygus datatype Trace("parser-sygus2") << "Make the sygus datatypes..." << std::endl; std::vector datatypeTypes = - PARSER_STATE->mkMutualDatatypeTypes(datatypes); + PARSER_STATE->mkMutualDatatypeTypes( + datatypes, false, ExprManager::DATATYPE_FLAG_PLACEHOLDER); // return is the first datatype ret = datatypeTypes[0]; } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 806569b08..bfdaf7852 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1269,8 +1269,7 @@ void Smt2Printer::toStream(std::ostream& out, expr::ExprDag::Scope dagScope(out, dag); if (tryToStream(out, c) || tryToStream(out, c) - || tryToStream(out, c) - || tryToStream(out, c) + || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c, d_variant) || tryToStream(out, c) @@ -1301,7 +1300,14 @@ void Smt2Printer::toStream(std::ostream& out, || tryToStream(out, c, d_variant) || tryToStream(out, c, d_variant) || tryToStream(out, c) - || tryToStream(out, c, d_variant)) + || tryToStream(out, c, d_variant) + || tryToStream(out, c) + || tryToStream(out, c) + || tryToStream(out, c) + || tryToStream(out, c) + || tryToStream(out, c) + || tryToStream(out, c) + || tryToStream(out, c)) { return; } @@ -2057,6 +2063,178 @@ static void toStream(std::ostream& out, const EchoCommand* c, Variant v) out << "(echo \"" << s << "\")"; } +/* + -------------------------------------------------------------------------- + Handling SyGuS commands + -------------------------------------------------------------------------- +*/ + +static void toStream(std::ostream& out, const SynthFunCommand* c) +{ + out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol()) + << ' '; + Type type = c->getFunction().getType(); + const std::vector& vars = c->getVars(); + Assert(!type.isFunction() || !vars.empty()); + c->getCommandName(); + 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() << ')'; + if (++i != i_end) + { + out << ' '; + } + } while (i != i_end); + out << ')'; + FunctionType ft = type; + type = ft.getRangeType(); + } + // if not invariant-to-synthesize, print return type + if (!c->isInv()) + { + out << ' ' << type; + } + // print grammar, if any + Type sygusType = c->getSygusType(); + if (sygusType.isDatatype() + && static_cast(sygusType).getDatatype().isSygus()) + { + std::stringstream types_predecl, types_list; + std::set grammarTypes; + std::list typesToPrint; + grammarTypes.insert(sygusType); + typesToPrint.push_back(sygusType); + // for each datatype in grammar + // name + // sygus type + // constructors in order + Printer* sygus_printer = + Printer::getPrinter(language::output::LANG_SYGUS_V2); + do + { + Type curr = typesToPrint.front(); + typesToPrint.pop_front(); + 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() << ")"; + 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) + { + types_list << "("; + SygusPrintCallback* spc = cons.getSygusPrintCallback().get(); + if (spc != nullptr && options::sygusPrintCallbacks()) + { + 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(); + } + } + types_list << "\n"; + } + types_list << "))\n"; + } while (!typesToPrint.empty()); + + out << "\n(" << types_predecl.str() << ")\n(" << types_list.str() << ")"; + } + out << ")"; +} + +static void toStream(std::ostream& out, const DeclareSygusFunctionCommand* c) +{ + out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol()); + + FunctionType ft = c->getType(); + stringstream ss; + + for (const Type& i : ft.getArgTypes()) + { + ss << i << ' '; + } + + string argTypes = ss.str(); + argTypes.pop_back(); + + out << " (" << argTypes << ") " << ft.getRangeType() << ')'; +} + +static void toStream(std::ostream& out, const DeclareSygusPrimedVarCommand* c) +{ + out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol()) + << ' ' << c->getType() << ')'; +} + +static void toStream(std::ostream& out, const DeclareSygusVarCommand* c) +{ + out << '(' << c->getCommandName() << ' ' << c->getVar() << ' ' << c->getType() + << ')'; +} + +static void toStream(std::ostream& out, const SygusConstraintCommand* c) +{ + out << '(' << c->getCommandName() << ' ' << c->getExpr() << ')'; +} + +static void toStream(std::ostream& out, const SygusInvConstraintCommand* c) +{ + out << '(' << c->getCommandName() << ' '; + copy(c->getPredicates().cbegin(), + c->getPredicates().cend(), + std::ostream_iterator(out, " ")); + out << ')'; +} + +static void toStream(std::ostream& out, const CheckSynthCommand* c) +{ + out << '(' << c->getCommandName() << ')'; +} + +/* + -------------------------------------------------------------------------- + End of Handling SyGuS commands + -------------------------------------------------------------------------- +*/ + template static bool tryToStream(std::ostream& out, const Command* c) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1d96fc207..f1d602bc6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3652,16 +3652,27 @@ void SmtEngine::ensureBoolean(const Expr& e) Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore) { + Dump("benchmark") << CheckSatCommand(assumption); return checkSatisfiability(assumption, inUnsatCore, false); } Result SmtEngine::checkSat(const vector& assumptions, bool inUnsatCore) { + if (assumptions.empty()) + { + Dump("benchmark") << CheckSatCommand(); + } + else + { + Dump("benchmark") << CheckSatAssumingCommand(assumptions); + } + return checkSatisfiability(assumptions, inUnsatCore, false); } Result SmtEngine::query(const Expr& assumption, bool inUnsatCore) { + Dump("benchmark") << QueryCommand(assumption, inUnsatCore); return checkSatisfiability(assumption.isNull() ? std::vector() : std::vector{assumption}, @@ -3789,25 +3800,6 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, d_needPostsolve = true; - // Dump the query if requested - if (Dump.isOn("benchmark")) - { - size_t size = assumptions.size(); - // the expr already got dumped out if assertion-dumping is on - if (isQuery && size == 1) - { - Dump("benchmark") << QueryCommand(assumptions[0]); - } - else if (size == 0) - { - Dump("benchmark") << CheckSatCommand(); - } - else - { - Dump("benchmark") << CheckSatAssumingCommand(d_assumptions); - } - } - // Pop the context if (didInternalPush) { @@ -3936,6 +3928,7 @@ void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type) { d_private->d_sygusVars.push_back(Node::fromExpr(var)); Trace("smt") << "SmtEngine::declareSygusVar: " << var << "\n"; + Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type); // don't need to set that the conjecture is stale } @@ -3943,6 +3936,7 @@ 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 } @@ -3952,6 +3946,7 @@ 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); // don't need to set that the conjecture is stale } @@ -3984,6 +3979,7 @@ void SmtEngine::declareSynthFun(const std::string& id, setUserAttribute("sygus-synth-grammar", func, attr_value, ""); } Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n"; + Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars); // sygus conjecture is now stale setSygusConjectureStale(); } @@ -3994,6 +3990,7 @@ void SmtEngine::assertSygusConstraint(Expr constraint) d_private->d_sygusConstraints.push_back(constraint); Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n"; + Dump("raw-benchmark") << SygusConstraintCommand(constraint); // sygus conjecture is now stale setSygusConjectureStale(); } @@ -4065,6 +4062,7 @@ void SmtEngine::assertSygusInvConstraint(const Expr& inv, d_private->d_sygusConstraints.push_back(constraint); Trace("smt") << "SmtEngine::assertSygusInvConstrant: " << constraint << "\n"; + Dump("raw-benchmark") << SygusInvConstraintCommand(inv, pre, trans, post); // sygus conjecture is now stale setSygusConjectureStale(); } @@ -4118,6 +4116,7 @@ Result SmtEngine::checkSynth() setUserAttribute("sygus", sygusVar.toExpr(), {}, ""); Trace("smt") << "Check synthesis conjecture: " << body << std::endl; + Dump("raw-benchmark") << CheckSynthCommand(); d_private->d_sygusConjectureStale = false; @@ -4195,9 +4194,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) // Ensure expr is type-checked at this point. e.getType(true); } - if(Dump.isOn("benchmark")) { - Dump("benchmark") << ExpandDefinitionsCommand(e); - } + unordered_map cache; Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true); n = postprocess(n, TypeNode::fromType(e.getType())); -- 2.30.2