From: Andrew Reynolds Date: Wed, 4 Sep 2019 21:45:08 +0000 (-0500) Subject: Towards incremental SyGuS in SMT engine (#3195) X-Git-Tag: cvc5-1.0.0~3978 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5b71632328be3d5a0677e12415d28c0d712aac3c;p=cvc5.git Towards incremental SyGuS in SMT engine (#3195) --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 562f2a897..3d469f2b5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -517,15 +517,10 @@ class SmtEnginePrivate : public NodeManagerListener { std::vector d_sygusConstraints; /** functions-to-synthesize */ std::vector d_sygusFunSymbols; - /** maps functions-to-synthesize to their respective input variables lists */ - std::map> d_sygusFunVars; - /** maps functions-to-synthesize to their respective syntactic restrictions - * - * If function has syntactic restrictions, these are encoded as a SyGuS - * datatype type + /** + * Whether we need to reconstruct the sygus conjecture. */ - std::map d_sygusFunSyntax; - + CDO d_sygusConjectureStale; /*------------------- end of sygus utils ------------------*/ private: @@ -575,7 +570,8 @@ class SmtEnginePrivate : public NodeManagerListener { d_simplifyAssertionsDepth(0), // d_needsExpandDefs(true), //TODO? d_exprNames(smt.d_userContext), - d_iteRemover(smt.d_userContext) + d_iteRemover(smt.d_userContext), + d_sygusConjectureStale(smt.d_userContext, true) { d_smt.d_nodeManager->subscribeEvents(this); d_true = NodeManager::currentNM()->mkConst(true); @@ -1980,10 +1976,10 @@ void SmtEngine::setDefaults() { // rewrite rule synthesis implies that sygus stream must be true options::sygusStream.set(true); } - if (options::sygusStream()) + if (options::sygusStream() || options::incrementalSolving()) { - // Streaming is incompatible with techniques that focus the search towards - // finding a single solution. + // Streaming and incremental mode are incompatible with techniques that + // focus the search towards finding a single solution. reqBasicSygus = true; } // Now, disable options for non-basic sygus algorithms, if necessary. @@ -3880,6 +3876,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"; + // don't need to set that the conjecture is stale } void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type) @@ -3888,6 +3885,7 @@ void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type) d_private->d_sygusPrimedVarTypes.push_back(type); #endif Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n"; + // don't need to set that the conjecture is stale } void SmtEngine::declareSygusFunctionVar(const std::string& id, @@ -3896,6 +3894,7 @@ void SmtEngine::declareSygusFunctionVar(const std::string& id, { d_private->d_sygusVars.push_back(Node::fromExpr(var)); Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n"; + // don't need to set that the conjecture is stale } void SmtEngine::declareSynthFun(const std::string& id, @@ -3904,28 +3903,41 @@ void SmtEngine::declareSynthFun(const std::string& id, bool isInv, const std::vector& vars) { + SmtScope smts(this); + finalOptionsAreSet(); + doPendingPops(); Node fn = Node::fromExpr(func); d_private->d_sygusFunSymbols.push_back(fn); - std::vector var_nodes; - for (const Expr& v : vars) + if (!vars.empty()) { - var_nodes.push_back(Node::fromExpr(v)); + Expr bvl = d_exprManager->mkExpr(kind::BOUND_VAR_LIST, vars); + std::vector attr_val_bvl; + attr_val_bvl.push_back(bvl); + setUserAttribute("sygus-synth-fun-var-list", func, attr_val_bvl, ""); } - d_private->d_sygusFunVars[fn] = var_nodes; // whether sygus type encodes syntax restrictions if (sygusType.isDatatype() && static_cast(sygusType).getDatatype().isSygus()) { - d_private->d_sygusFunSyntax[fn] = TypeNode::fromType(sygusType); + TypeNode stn = TypeNode::fromType(sygusType); + Node sym = d_nodeManager->mkBoundVar("sfproxy", stn); + std::vector attr_value; + attr_value.push_back(sym.toExpr()); + setUserAttribute("sygus-synth-grammar", func, attr_value, ""); } Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n"; + // sygus conjecture is now stale + setSygusConjectureStale(); } void SmtEngine::assertSygusConstraint(Expr constraint) { + SmtScope smts(this); d_private->d_sygusConstraints.push_back(constraint); Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n"; + // sygus conjecture is now stale + setSygusConjectureStale(); } void SmtEngine::assertSygusInvConstraint(const Expr& inv, @@ -4016,11 +4028,27 @@ void SmtEngine::assertSygusInvConstraint(const Expr& inv, d_private->d_sygusConstraints.push_back(constraint); Trace("smt") << "SmtEngine::assertSygusInvConstrant: " << constraint << "\n"; + // sygus conjecture is now stale + setSygusConjectureStale(); } Result SmtEngine::checkSynth() { SmtScope smts(this); + + if (options::incrementalSolving()) + { + // TODO (project #7) + throw ModalException( + "Cannot make check-synth commands when incremental solving is enabled"); + } + + if (!d_private->d_sygusConjectureStale) + { + // do not need to reconstruct, we're done + return checkSatisfiability(Expr(), true, false); + } + // build synthesis conjecture from asserted constraints and declared // variables/functions Node sygusVar = @@ -4056,39 +4084,19 @@ Result SmtEngine::checkSynth() // set attribute for synthesis conjecture setUserAttribute("sygus", sygusVar.toExpr(), {}, ""); - // set attributes for functions-to-synthesize - for (const Node& synth_fun : d_private->d_sygusFunSymbols) + Trace("smt") << "Check synthesis conjecture: " << body << std::endl; + + d_private->d_sygusConjectureStale = false; + + if (options::incrementalSolving()) { - // associate var list with function-to-synthesize - Assert(d_private->d_sygusFunVars.find(synth_fun) - != d_private->d_sygusFunVars.end()); - const std::vector& vars = d_private->d_sygusFunVars[synth_fun]; - Node bvl; - if (!vars.empty()) - { - bvl = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, vars); - } - std::vector attr_val_bvl; - attr_val_bvl.push_back(bvl.toExpr()); - setUserAttribute( - "sygus-synth-fun-var-list", synth_fun.toExpr(), attr_val_bvl, ""); - // If the function has syntax restrition, bulid a variable "sfproxy" which - // carries the type, a SyGuS datatype that corresponding to the syntactic - // restrictions. - std::map::const_iterator it = - d_private->d_sygusFunSyntax.find(synth_fun); - if (it != d_private->d_sygusFunSyntax.end()) - { - Node sym = d_nodeManager->mkBoundVar("sfproxy", it->second); - std::vector attr_value; - attr_value.push_back(sym.toExpr()); - setUserAttribute( - "sygus-synth-grammar", synth_fun.toExpr(), attr_value, ""); - } + // we push a context so that this conjecture is removed if we modify it + // later + internalPush(); + assertFormula(body.toExpr(), true); + return checkSatisfiability(body.toExpr(), true, false); } - Trace("smt") << "Check synthesis conjecture: " << body << std::endl; - return checkSatisfiability(body.toExpr(), true, false); } @@ -5649,4 +5657,18 @@ void SmtEngine::setExpressionName(Expr e, const std::string& name) { d_private->setExpressionName(e,name); } +void SmtEngine::setSygusConjectureStale() +{ + if (d_private->d_sygusConjectureStale) + { + // already stale + return; + } + d_private->d_sygusConjectureStale = true; + if (options::incrementalSolving()) + { + internalPop(); + } +} + }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 120c712ea..4f18546ad 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1240,6 +1240,24 @@ class CVC4_PUBLIC SmtEngine /** Container for the lemma input and output channels for this SmtEngine.*/ LemmaChannels* d_channels; + + /*---------------------------- sygus commands ---------------------------*/ + + /** + * Set sygus conjecture is stale. The sygus conjecture is stale if either: + * (1) no sygus conjecture has been added as an assertion to this SMT engine, + * (2) there is a sygus conjecture that has been added as an assertion + * internally to this SMT engine, and there have been further calls such that + * the asserted conjecture is no longer up-to-date. + * + * This method should be called when new sygus constraints are asserted and + * when functions-to-synthesize are declared. This function pops a user + * context if we are in incremental mode and the sygus conjecture was + * previously not stale. + */ + void setSygusConjectureStale(); + + /*------------------------- end of sygus commands ------------------------*/ }; /* class SmtEngine */ /* -------------------------------------------------------------------------- */