From: Andrew Reynolds Date: Mon, 17 Sep 2018 14:27:03 +0000 (-0500) Subject: Decision strategy: incorporate sygus feasible and sygus stream feasible (#2462) X-Git-Tag: cvc5-1.0.0~4647 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dd92afc3da5ce3c8db63e462b37031860fd0152b;p=cvc5.git Decision strategy: incorporate sygus feasible and sygus stream feasible (#2462) --- diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index d8329395d..dafcab5de 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -168,6 +168,14 @@ void CegConjecture::assign( Node q ) { d_feasible_guard = Rewriter::rewrite(d_feasible_guard); d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard); AlwaysAssert(!d_feasible_guard.isNull()); + // register the strategy + d_feasible_strategy.reset( + new DecisionStrategySingleton("sygus_feasible", + d_feasible_guard, + d_qe->getSatContext(), + d_qe->getValuation())); + d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy( + DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get()); // this must be called, both to ensure that the feasible guard is // decided on with true polariy, but also to ensure that output channel // has been used on this call to check. @@ -193,6 +201,15 @@ void CegConjecture::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->getTheoryEngine()->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; } @@ -234,24 +251,26 @@ void CegConjecture::doSingleInvCheck(std::vector< Node >& lems) { } } -void CegConjecture::doBasicCheck(std::vector< Node >& lems) { - std::vector< Node > model_terms; - Assert(d_candidates.size() == d_quant[0].getNumChildren()); - getModelValues(d_candidates, model_terms); - if (d_qe->getInstantiate()->addInstantiation(d_quant, model_terms)) - { - //record the instantiation - recordInstantiation( model_terms ); - }else{ - Assert( false ); - } -} - bool CegConjecture::needsRefinement() const { return d_set_ce_sk_vars; } void CegConjecture::doCheck(std::vector& lems) { Assert(d_master != nullptr); + // 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) + { + // we have a new guard, print and continue the stream + printAndContinueStream(); + d_current_stream_guard = currGuard; + return; + } + } + // get the list of terms that the master strategy is interested in std::vector terms; d_master->getTermList(d_candidates, terms); @@ -386,32 +405,37 @@ void CegConjecture::doCheck(std::vector& lems) d_set_ce_sk_vars = true; } - if (!lem.isNull()) + if (lem.isNull()) + { + // no lemma to check + return; + } + + lem = Rewriter::rewrite(lem); + // eagerly unfold applications of evaluation function + Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl; + std::map visited_n; + lem = d_qe->getTermDatabaseSygus()->getEagerUnfold(lem, visited_n); + // 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 { - lem = Rewriter::rewrite( lem ); - //eagerly unfold applications of evaluation function - Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl; - std::map visited_n; - lem = d_qe->getTermDatabaseSygus()->getEagerUnfold(lem, visited_n); - // record the instantiation - // this is used for remembering the solution - recordInstantiation(candidate_values); - Node query = lem; - if (query.isConst() && !query.getConst() && options::sygusStream()) - { - // short circuit the check - // instead, we immediately print the current solution. - // this saves us from introducing a check lemma and a new guard. - printAndContinueStream(); - return; - } // 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); if (options::sygusVerifySubcall()) { - Trace("cegqi-engine") << " *** Direct verify..." << std::endl; + Trace("cegqi-engine") << " *** Verify with subcall..." << std::endl; SmtEngine verifySmt(nm->toExprManager()); verifySmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); verifySmt.assertFormula(query.toExpr()); @@ -446,14 +470,23 @@ void CegConjecture::doCheck(std::vector& lems) // 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; } // In the rare case that the subcall is unknown, we add the verification // lemma in the main solver. This should only happen if the quantifier // free logic is undecidable. } - lem = getStreamGuardedLemma(lem); - lems.push_back(lem); } + if (success && 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(); + return; + } + lem = getStreamGuardedLemma(lem); + lems.push_back(lem); } void CegConjecture::doRefine( std::vector< Node >& lems ){ @@ -556,11 +589,18 @@ void CegConjecture::debugPrint( const char * c ) { } Node CegConjecture::getCurrentStreamGuard() const { - if( d_stream_guards.empty() ){ - return Node::null(); - }else{ - return d_stream_guards.back(); + 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 CegConjecture::getStreamGuardedLemma(Node n) const @@ -575,69 +615,8 @@ Node CegConjecture::getStreamGuardedLemma(Node n) const return n; } -Node CegConjecture::getNextDecisionRequest( unsigned& priority ) { - // first, must try the guard - // which denotes "this conjecture is feasible" - Node feasible_guard = d_feasible_guard; - bool value; - if( !d_qe->getValuation().hasSatValue( feasible_guard, value ) ) { - priority = 0; - return feasible_guard; - } - if (!value) - { - Trace("cegqi-debug") << "getNextDecision : conjecture is infeasible." - << std::endl; - return Node::null(); - } - // the conjecture is feasible - if (options::sygusStream()) - { - Assert(!isSingleInvocation()); - // if we are in sygus streaming mode, then get the "next guard" - // which denotes "we have not yet generated the next solution to the - // conjecture" - Node curr_stream_guard = getCurrentStreamGuard(); - bool needs_new_stream_guard = false; - if (curr_stream_guard.isNull()) - { - needs_new_stream_guard = true; - }else{ - // check the polarity of the guard - if (!d_qe->getValuation().hasSatValue(curr_stream_guard, value)) - { - priority = 0; - return curr_stream_guard; - } - if (!value) - { - Trace("cegqi-debug") << "getNextDecision : we have a new solution " - "since stream guard was propagated false: " - << curr_stream_guard << std::endl; - // need to make the next stream guard - needs_new_stream_guard = true; - // the guard has propagated false, indicating that a verify - // lemma was unsatisfiable. Hence, the previous candidate is - // an actual solution. We print and continue the stream. - printAndContinueStream(); - } - } - if (needs_new_stream_guard) - { - // generate a new stream guard - curr_stream_guard = Rewriter::rewrite(NodeManager::currentNM()->mkSkolem( - "G_Stream", NodeManager::currentNM()->booleanType())); - curr_stream_guard = d_qe->getValuation().ensureLiteral(curr_stream_guard); - AlwaysAssert(!curr_stream_guard.isNull()); - d_qe->getOutputChannel().requirePhase(curr_stream_guard, true); - d_stream_guards.push_back(curr_stream_guard); - Trace("cegqi-debug") << "getNextDecision : allocate new stream guard : " - << curr_stream_guard << std::endl; - // return it as a decision - priority = 0; - return curr_stream_guard; - } - } +Node CegConjecture::getNextDecisionRequest(unsigned& priority) +{ // see if the master module has a decision if (!isSingleInvocation()) { @@ -650,10 +629,22 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) { return mlit; } } - return Node::null(); } +CegConjecture::SygusStreamDecisionStrategy::SygusStreamDecisionStrategy( + context::Context* satContext, Valuation valuation) + : DecisionStrategyFmf(satContext, valuation) +{ +} + +Node CegConjecture::SygusStreamDecisionStrategy::mkLiteral(unsigned i) +{ + NodeManager* nm = NodeManager::currentNM(); + Node curr_stream_guard = nm->mkSkolem("G_Stream", nm->booleanType()); + return curr_stream_guard; +} + void CegConjecture::printAndContinueStream() { Assert(d_master != nullptr); diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h index 88902e721..41ec6ab9e 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -20,6 +20,7 @@ #include +#include "theory/decision_manager.h" #include "theory/quantifiers/expr_miner_manager.h" #include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "theory/quantifiers/sygus/cegis.h" @@ -51,7 +52,6 @@ public: Node getEmbeddedConjecture() { return d_embed_quant; } /** get next decision request */ Node getNextDecisionRequest( unsigned& priority ); - //-------------------------------for counterexample-guided check/refine /** increment the number of times we have successfully done candidate * refinement */ @@ -68,10 +68,6 @@ public: * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015. */ void doCheck(std::vector& lems); - /** do basic check - * This is called for non-SyGuS synthesis conjectures - */ - void doBasicCheck(std::vector< Node >& lems); /** do refinement * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015. */ @@ -136,6 +132,8 @@ private: QuantifiersEngine * d_qe; /** The feasible guard. */ Node d_feasible_guard; + /** the decision strategy for the feasible guard */ + std::unique_ptr d_feasible_strategy; /** single invocation utility */ std::unique_ptr d_ceg_si; /** utility for static preprocessing and analysis of conjectures */ @@ -244,8 +242,23 @@ private: std::vector& status, bool singleInvocation); //-------------------------------- sygus stream - /** the streaming guards for sygus streaming mode */ - std::vector< Node > d_stream_guards; + /** 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