From: Andrew Reynolds Date: Thu, 12 Nov 2020 23:34:22 +0000 (-0600) Subject: Simplify sygus solver and sygus stream (#5389) X-Git-Tag: cvc5-1.0.0~2603 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cf7c2ce97615990388bb6c37b151c0e2b2fe8f9a;p=cvc5.git Simplify sygus solver and sygus stream (#5389) This simplifies the sygus solver based on the fact that verification lemmas are always processed in a separate subsolver. In particular, this means that the implementation of --sygus-stream can be simplified signficantly. --- diff --git a/src/theory/decision_manager.h b/src/theory/decision_manager.h index e372ab353..8ee9a22fd 100644 --- a/src/theory/decision_manager.h +++ b/src/theory/decision_manager.h @@ -61,7 +61,6 @@ class DecisionManager // "sat" for problems that are unsat. STRAT_QUANT_CEGQI_FEASIBLE, STRAT_QUANT_SYGUS_FEASIBLE, - STRAT_QUANT_SYGUS_STREAM_FEASIBLE, // placeholder for last model-sound required strategy STRAT_LAST_M_SOUND, diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 8dd9a455a..b8700f7f6 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -43,10 +43,8 @@ namespace theory { namespace quantifiers { SynthConjecture::SynthConjecture(QuantifiersEngine* qe, - SynthEngine* p, SygusStatistics& s) : d_qe(qe), - d_parent(p), d_stats(s), d_tds(qe->getTermDatabaseSygus()), d_hasSolution(false), @@ -255,15 +253,6 @@ void SynthConjecture::assign(Node q) d_qe->getOutputChannel().lemma(lem); } - if (options::sygusStream()) - { - d_stream_strategy.reset(new SygusStreamDecisionStrategy( - d_qe->getSatContext(), d_qe->getValuation())); - d_qe->getDecisionManager()->registerStrategy( - DecisionManager::STRAT_QUANT_SYGUS_STREAM_FEASIBLE, - d_stream_strategy.get()); - d_current_stream_guard = d_stream_strategy->getLiteral(0); - } Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl; } @@ -314,9 +303,7 @@ bool SynthConjecture::doCheck(std::vector& lems) { d_hasSolution = true; // the conjecture has a solution, so its negation holds - Node lem = d_quant.negate(); - lem = getStreamGuardedLemma(lem); - lems.push_back(lem); + lems.push_back(d_quant.negate()); } return true; } @@ -327,24 +314,6 @@ bool SynthConjecture::doCheck(std::vector& lems) std::vector terms; d_master->getTermList(d_candidates, terms); - // process the sygus streaming guard - if (options::sygusStream()) - { - Assert(!isSingleInvocation()); - // it may be the case that we have a new solution now - Node currGuard = getCurrentStreamGuard(); - if (currGuard != d_current_stream_guard) - { - std::vector vals; - std::vector status; - getSynthSolutionsInternal(vals, status); - // we have a new guard, print and continue the stream - printAndContinueStream(terms, vals); - d_current_stream_guard = currGuard; - return true; - } - } - Assert(!d_candidates.empty()); Trace("cegqi-check") << "CegConjuncture : check, build candidates..." @@ -530,17 +499,14 @@ bool SynthConjecture::doCheck(std::vector& lems) // we have that the current candidate passed a sample test // since we trust sampling in this mode, we assert there is no // counterexample to the conjecture here. - Node lem = nm->mkNode(OR, d_quant.negate(), nm->mkConst(false)); - lem = getStreamGuardedLemma(lem); - lems.push_back(lem); - recordInstantiation(candidate_values); - d_hasSolution = true; + lems.push_back(d_quant.negate()); + recordSolution(candidate_values); return true; } Assert(!d_set_ce_sk_vars); // immediately skolemize inner existentials - Node lem; + Node query; // introduce the skolem variables std::vector sks; std::vector vars; @@ -571,49 +537,36 @@ bool SynthConjecture::doCheck(std::vector& lems) Trace("cegqi-check-debug") << " introduce skolem " << sk << " for " << v << "\n"; } - lem = inst[0][1].substitute( + query = inst[0][1].substitute( vars.begin(), vars.end(), sks.begin(), sks.end()); - lem = lem.negate(); + query = query.negate(); } else { // use the instance itself - lem = inst; + query = inst; } } d_ce_sk_vars.insert(d_ce_sk_vars.end(), sks.begin(), sks.end()); d_set_ce_sk_vars = true; - if (lem.isNull()) + if (query.isNull()) { // no lemma to check return false; } // simplify the lemma based on the term database sygus utility - lem = d_tds->rewriteNode(lem); + query = d_tds->rewriteNode(query); // eagerly unfold applications of evaluation function - Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl; - // record the instantiation - // this is used for remembering the solution - recordInstantiation(candidate_values); - - Node query = lem; - bool success = false; - if (query.isConst() && !query.getConst()) - { - // short circuit the check - lem = d_quant.negate(); - success = true; - } - else + Trace("cegqi-debug") << "pre-unfold counterexample : " << query << std::endl; + // Record the solution, which may be falsified below. We require recording + // here since the result of the satisfiability test may be unknown. + recordSolution(candidate_values); + + if (!query.isConst() || query.getConst()) { - // This is the "verification lemma", which states - // either this conjecture does not have a solution, or candidate_values - // is a solution for this conjecture. - lem = nm->mkNode(OR, d_quant.negate(), query); Trace("sygus-engine") << " *** Verify with subcall..." << std::endl; - Result r = checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs); Trace("sygus-engine") << " ...got " << r << std::endl; @@ -644,15 +597,7 @@ bool SynthConjecture::doCheck(std::vector& lems) } return false; } - else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - // if the result in the subcall was unsatisfiable, we avoid - // rechecking, hence we drop "query" from the verification lemma - lem = d_quant.negate(); - // we can short circuit adding the lemma (for sygus stream) - success = true; - } - else + else if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) { // In the rare case that the subcall is unknown, we simply exclude the // solution, without adding a counterexample point. This should only @@ -664,22 +609,21 @@ bool SynthConjecture::doCheck(std::vector& lems) d_qe->getOutputChannel().setIncomplete(); return false; } + // otherwise we are unsat, and we will process the solution below } - if (success) + // now mark that we have a solution + d_hasSolution = true; + if (options::sygusStream()) { - d_hasSolution = true; - if (options::sygusStream()) - { - // if we were successful, we immediately print the current solution. - // this saves us from introducing a verification lemma and a new guard. - printAndContinueStream(terms, candidate_values); - // streaming means now we immediately are looking for a new solution - d_hasSolution = false; - return false; - } + // immediately print the current solution + printAndContinueStream(terms, candidate_values); + // streaming means now we immediately are looking for a new solution + d_hasSolution = false; + return false; } - lem = getStreamGuardedLemma(lem); - lems.push_back(lem); + // Use lemma to terminate with "unsat", this is justified by the verification + // check above, which confirms the synthesis conjecture is solved. + lems.push_back(d_quant.negate()); return true; } @@ -1027,47 +971,6 @@ void SynthConjecture::debugPrint(const char* c) Trace(c) << " * Counterexample skolems : " << d_ce_sk_vars << std::endl; } -Node SynthConjecture::getCurrentStreamGuard() const -{ - if (d_stream_strategy != nullptr) - { - // the stream guard is the current asserted literal of the stream strategy - Node lit = d_stream_strategy->getAssertedLiteral(); - if (lit.isNull()) - { - // if none exist, get the first - lit = d_stream_strategy->getLiteral(0); - } - return lit; - } - return Node::null(); -} - -Node SynthConjecture::getStreamGuardedLemma(Node n) const -{ - if (options::sygusStream()) - { - // if we are in streaming mode, we guard with the current stream guard - Node csg = getCurrentStreamGuard(); - Assert(!csg.isNull()); - return NodeManager::currentNM()->mkNode(kind::OR, csg.negate(), n); - } - return n; -} - -SynthConjecture::SygusStreamDecisionStrategy::SygusStreamDecisionStrategy( - context::Context* satContext, Valuation valuation) - : DecisionStrategyFmf(satContext, valuation) -{ -} - -Node SynthConjecture::SygusStreamDecisionStrategy::mkLiteral(unsigned i) -{ - NodeManager* nm = NodeManager::currentNM(); - Node curr_stream_guard = nm->mkSkolem("G_Stream", nm->booleanType()); - return curr_stream_guard; -} - void SynthConjecture::printAndContinueStream(const std::vector& enums, const std::vector& values) { @@ -1299,6 +1202,16 @@ bool SynthConjecture::getSynthSolutions( return true; } +void SynthConjecture::recordSolution(std::vector& vs) +{ + Assert(vs.size() == d_candidates.size()); + d_cinfo.clear(); + for (unsigned i = 0; i < vs.size(); i++) + { + d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]); + } +} + bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, std::vector& statuses) { @@ -1327,7 +1240,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector& sols, } else { - Node cprog = getCandidate(i); + Node cprog = d_candidates[i]; if (!d_cinfo[cprog].d_inst.empty()) { // the solution is just the last instantiated term diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 7f499b1b3..7786f57ad 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -39,7 +39,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class SynthEngine; class SygusStatistics; /** @@ -83,7 +82,7 @@ class EnumValGenerator class SynthConjecture { public: - SynthConjecture(QuantifiersEngine* qe, SynthEngine* p, SygusStatistics& s); + SynthConjecture(QuantifiersEngine* qe, SygusStatistics& s); ~SynthConjecture(); /** presolve */ void presolve(); @@ -200,8 +199,6 @@ class SynthConjecture private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; - /** pointer to the synth engine that owns this */ - SynthEngine* d_parent; /** reference to the statistics of parent */ SygusStatistics& d_stats; /** term database sygus of d_qe */ @@ -360,17 +357,8 @@ class SynthConjecture unsigned d_repair_index; /** number of times we have called doRefine */ unsigned d_refine_count; - /** get candidadate */ - Node getCandidate(unsigned int i) { return d_candidates[i]; } - /** record instantiation (this is used to construct solutions later) */ - void recordInstantiation(std::vector& vs) - { - Assert(vs.size() == d_candidates.size()); - for (unsigned i = 0; i < vs.size(); i++) - { - d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]); - } - } + /** record solution (this is used to construct solutions later) */ + void recordSolution(std::vector& vs); /** get synth solutions internal * * This function constructs the body of solutions for all @@ -392,31 +380,6 @@ class SynthConjecture bool getSynthSolutionsInternal(std::vector& sols, std::vector& status); //-------------------------------- sygus stream - /** current stream guard */ - Node d_current_stream_guard; - /** the decision strategy for streaming solutions */ - class SygusStreamDecisionStrategy : public DecisionStrategyFmf - { - public: - SygusStreamDecisionStrategy(context::Context* satContext, - Valuation valuation); - /** make literal */ - Node mkLiteral(unsigned i) override; - /** identify */ - std::string identify() const override - { - return std::string("sygus_stream"); - } - }; - std::unique_ptr d_stream_strategy; - /** get current stream guard */ - Node getCurrentStreamGuard() const; - /** get stream guarded lemma - * - * If sygusStream is enabled, this returns ( G V n ) where G is the guard - * returned by getCurrentStreamGuard, otherwise this returns n. - */ - Node getStreamGuardedLemma(Node n) const; /** * Prints the current synthesis solution to the output stream indicated by * the Options object, send a lemma blocking the current solution to the diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index ba11490b5..3e40d6654 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -37,7 +37,7 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c) d_sqp(qe) { d_conjs.push_back(std::unique_ptr( - new SynthConjecture(d_quantEngine, this, d_statistics))); + new SynthConjecture(d_quantEngine, d_statistics))); d_conj = d_conjs.back().get(); } @@ -159,7 +159,7 @@ void SynthEngine::assignConjecture(Node q) if (d_conjs.back()->isAssigned()) { d_conjs.push_back(std::unique_ptr( - new SynthConjecture(d_quantEngine, this, d_statistics))); + new SynthConjecture(d_quantEngine, d_statistics))); } d_conjs.back()->assign(q); }