From: Andrew Reynolds Date: Thu, 3 May 2018 16:30:09 +0000 (-0500) Subject: Link cegis unif with the enumeration manager (#1859) X-Git-Tag: cvc5-1.0.0~5098 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4251c330cc2e9e87ffaaf4dd2c1bc9db6f1046a5;p=cvc5.git Link cegis unif with the enumeration manager (#1859) --- diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index db641a82e..d5a430229 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -479,51 +479,74 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) { if( !d_qe->getValuation().hasSatValue( feasible_guard, value ) ) { priority = 0; return feasible_guard; - }else{ - if( value ){ - // 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; - }else{ - 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; - } - } + } + 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{ - Trace("cegqi-debug") << "getNextDecision : conjecture is infeasible." << std::endl; - } + // 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; + } } + // see if the master module has a decision + if (!isSingleInvocation()) + { + Assert(d_master != nullptr); + Node mlit = d_master->getNextDecisionRequest(priority); + if (!mlit.isNull()) + { + Trace("cegqi-debug") << "getNextDecision : master module returned : " + << mlit << std::endl; + return mlit; + } + } + return Node::null(); } diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 14a5bedf5..ee8fb6f12 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -26,7 +26,7 @@ namespace theory { namespace quantifiers { CegisUnif::CegisUnif(QuantifiersEngine* qe, CegConjecture* p) - : Cegis(qe, p), d_sygus_unif(p) + : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p) { d_tds = d_qe->getTermDatabaseSygus(); } @@ -39,16 +39,24 @@ bool CegisUnif::initialize(Node n, Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl; /* Init UNIF util */ d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, lemmas); - /* TODO initialize unif enumerators */ Trace("cegis-unif") << "Initializing enums for pure Cegis case\n"; + std::vector unif_candidates; /* Initialize enumerators for non-unif functions-to-synhesize */ for (const Node& c : candidates) { if (!d_sygus_unif.usingUnif(c)) { + Trace("cegis-unif") << "* non-unification candidate : " << c << std::endl; d_tds->registerEnumerator(c, c, d_parent); } + else + { + Trace("cegis-unif") << "* unification candidate : " << c << std::endl; + unif_candidates.push_back(c); + } } + // initialize the enumeration manager + d_u_enum_manager.initialize(unif_candidates); return true; } @@ -158,15 +166,27 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, OR, d_parent->getGuard().negate(), plem)); } +Node CegisUnif::getNextDecisionRequest(unsigned& priority) +{ + return d_u_enum_manager.getNextDecisionRequest(priority); +} + CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe, CegConjecture* parent) - : d_qe(qe), d_parent(parent), d_curr_guq_val(qe->getSatContext(), 0) + : d_qe(qe), + d_parent(parent), + d_ret_dec(qe->getSatContext(), false), + d_curr_guq_val(qe->getSatContext(), 0) { d_tds = d_qe->getTermDatabaseSygus(); } void CegisUnifEnumManager::initialize(std::vector& cs) { + if (cs.empty()) + { + return; + } for (const Node& c : cs) { // currently, we allocate the same enumerators for candidates of the same @@ -199,10 +219,23 @@ void CegisUnifEnumManager::registerEvalPts(std::vector& eis, Node c) Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority) { + // have we returned our decision in the current SAT context? + if (d_ret_dec.get()) + { + return Node::null(); + } + // only call this after initialization + if (d_ce_info.empty()) + { + // if no enumerators, the decision is null + d_ret_dec = true; + return Node::null(); + } Node lit = getCurrentLiteral(); bool value; if (!d_qe->getValuation().hasSatValue(lit, value)) { + d_ret_dec = true; priority = 0; return lit; } diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index ab2192ff8..2b1f1584a 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -26,6 +26,108 @@ namespace CVC4 { namespace theory { namespace quantifiers { +/** Cegis Unif Enumeration Manager + * + * This class enforces a decision heuristic that limits the number of + * unique values given to the set of "evaluation points", which are variables + * of sygus datatype type that are introduced by CegisUnif. + * + * It maintains a set of guards, call them G_uq_1 ... G_uq_n, where the + * semantics of G_uq_i is "for each type, the evaluation points of that type + * are interpreted as a value in a set whose cardinality is at most i". + * + * To enforce this, we introduce sygus enumerator(s) of the same type as the + * evaluation points registered to this class and add lemmas that enforce that + * points are equal to at least one enumerator (see registerEvalPtAtValue). + */ +class CegisUnifEnumManager +{ + public: + CegisUnifEnumManager(QuantifiersEngine* qe, CegConjecture* parent); + /** initialize candidates + * + * Notify this class that it will be managing enumerators for the vector + * of functions-to-synthesize (candidate variables) in candidates. This + * function should only be called once. + * + * Each candidate c in cs should be such that we are using a + * synthesis-by-unification approach for c. + */ + void initialize(std::vector& cs); + /** register evaluation point for candidate + * + * This notifies this class that eis is a set of evaluation points for + * candidate c, where c should be a candidate that was passed to initialize + * in the vector cs. + * + * This may add new lemmas of the form described above + * registerEvalPtAtValue on the output channel of d_qe. + */ + void registerEvalPts(std::vector& eis, Node c); + /** get next decision request + * + * This function has the same contract as Theory::getNextDecisionRequest. + * + * If no guard G_uq_* is asserted positively, then this method returns the + * minimal G_uq_i that is not asserted negatively. It allocates this guard + * if necessary. + * + * This call may add new lemmas of the form described above + * registerEvalPtAtValue on the output channel of d_qe. + */ + Node getNextDecisionRequest(unsigned& priority); + + private: + /** reference to quantifier engine */ + QuantifiersEngine* d_qe; + /** sygus term database of d_qe */ + TermDbSygus* d_tds; + /** reference to the parent conjecture */ + CegConjecture* d_parent; + /** null node */ + Node d_null; + /** information per initialized type */ + class TypeInfo + { + public: + TypeInfo() {} + /** candidates for this type */ + std::vector d_candidates; + /** the set of enumerators we have allocated for this candidate */ + std::vector d_enums; + /** the set of evaluation points of this type */ + std::vector d_eval_points; + }; + /** map types to the above info */ + std::map d_ce_info; + /** literals of the form G_uq_n for each n */ + std::map d_guq_lit; + /** Have we returned a decision in the current SAT context? */ + context::CDO d_ret_dec; + /** + * The minimal n such that G_uq_n is not asserted negatively in the + * current SAT context. + */ + context::CDO d_curr_guq_val; + /** increment the number of enumerators */ + void incrementNumEnumerators(); + /** + * Get the "current" literal G_uq_n, where n is the minimal n such that G_uq_n + * is not asserted negatively in the current SAT context. + */ + Node getCurrentLiteral() const; + /** get literal G_uq_n */ + Node getLiteral(unsigned n) const; + /** register evaluation point at size + * + * This sends a lemma of the form: + * G_uq_n => ei = d1 V ... V ei = dn + * on the output channel of d_qe, where d1...dn are sygus enumerators of the + * same type (ct) as ei. + */ + void registerEvalPtAtSize(TypeNode ct, Node ei, Node guq_lit, unsigned n); +}; + /** Synthesizes functions in a data-driven SyGuS approach * * Data is derived from refinement lemmas generated through the regular CEGIS @@ -110,6 +212,8 @@ class CegisUnif : public Cegis void registerRefinementLemma(const std::vector& vars, Node lem, std::vector& lems) override; + /** get next decision request */ + Node getNextDecisionRequest(unsigned& priority) override; private: /** sygus term database of d_qe */ @@ -119,6 +223,8 @@ class CegisUnif : public Cegis * tree learning) that this module relies upon. */ SygusUnifRl d_sygus_unif; + /** enumerator manager utility */ + CegisUnifEnumManager d_u_enum_manager; /** * list of conditonal enumerators to build solutions for candidates being * synthesized with unification techniques @@ -130,106 +236,6 @@ class CegisUnif : public Cegis Node d_null; }; /* class CegisUnif */ -/** Cegis Unif Enumeration Manager - * - * This class enforces a decision heuristic that limits the number of - * unique values given to the set of "evaluation points", which are variables - * of sygus datatype type that are introduced by CegisUnif. - * - * It maintains a set of guards, call them G_uq_1 ... G_uq_n, where the - * semantics of G_uq_i is "for each type, the evaluation points of that type - * are interpreted as a value in a set whose cardinality is at most i". - * - * To enforce this, we introduce sygus enumerator(s) of the same type as the - * evaluation points registered to this class and add lemmas that enforce that - * points are equal to at least one enumerator (see registerEvalPtAtValue). - */ -class CegisUnifEnumManager -{ - public: - CegisUnifEnumManager(QuantifiersEngine* qe, CegConjecture* parent); - /** initialize candidates - * - * Notify this class that it will be managing enumerators for the vector - * of functions-to-synthesize (candidate variables) in candidates. This - * function should only be called once. - * - * Each candidate c in cs should be such that we are using a - * synthesis-by-unification approach for c. - */ - void initialize(std::vector& cs); - /** register evaluation point for candidate - * - * This notifies this class that eis is a set of evaluation points for - * candidate c, where c should be a candidate that was passed to initialize - * in the vector cs. - * - * This may add new lemmas of the form described above - * registerEvalPtAtValue on the output channel of d_qe. - */ - void registerEvalPts(std::vector& eis, Node c); - /** get next decision request - * - * This function has the same contract as Theory::getNextDecisionRequest. - * - * If no guard G_uq_* is asserted positively, then this method returns the - * minimal G_uq_i that is not asserted negatively. It allocates this guard - * if necessary. - * - * This call may add new lemmas of the form described above - * registerEvalPtAtValue on the output channel of d_qe. - */ - Node getNextDecisionRequest(unsigned& priority); - - private: - /** reference to quantifier engine */ - QuantifiersEngine* d_qe; - /** sygus term database of d_qe */ - TermDbSygus* d_tds; - /** reference to the parent conjecture */ - CegConjecture* d_parent; - /** null node */ - Node d_null; - /** information per initialized type */ - class TypeInfo - { - public: - TypeInfo() {} - /** candidates for this type */ - std::vector d_candidates; - /** the set of enumerators we have allocated for this candidate */ - std::vector d_enums; - /** the set of evaluation points of this type */ - std::vector d_eval_points; - }; - /** map types to the above info */ - std::map d_ce_info; - /** literals of the form G_uq_n for each n */ - std::map d_guq_lit; - /** - * The minimal n such that G_uq_n is not asserted negatively in the - * current SAT context. - */ - context::CDO d_curr_guq_val; - /** increment the number of enumerators */ - void incrementNumEnumerators(); - /** - * Get the "current" literal G_uq_n, where n is the minimal n such that G_uq_n - * is not asserted negatively in the current SAT context. - */ - Node getCurrentLiteral() const; - /** get literal G_uq_n */ - Node getLiteral(unsigned n) const; - /** register evaluation point at size - * - * This sends a lemma of the form: - * G_uq_n => ei = d1 V ... V ei = dn - * on the output channel of d_qe, where d1...dn are sygus enumerators of the - * same type (ct) as ei. - */ - void registerEvalPtAtSize(TypeNode ct, Node ei, Node guq_lit, unsigned n); -}; - } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 0a3fa9995..07f5aec9d 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -114,6 +114,14 @@ class SygusModule std::vector& lems) { } + /** get next decision request + * + * This has the same contract as Theory::getNextDecisionRequest. + */ + virtual Node getNextDecisionRequest(unsigned& priority) + { + return Node::null(); + } protected: /** reference to quantifier engine */