From: Andrew Reynolds Date: Mon, 17 Sep 2018 22:32:02 +0000 (-0500) Subject: Decision strategy: incorporate cegis unif (#2482) X-Git-Tag: cvc5-1.0.0~4638 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8d7b71d2a8c02bf26ec3fa1de6abcf2547b3acbf;p=cvc5.git Decision strategy: incorporate cegis unif (#2482) --- diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index dafcab5de..30c0a3ae1 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -615,23 +615,6 @@ Node CegConjecture::getStreamGuardedLemma(Node n) const return n; } -Node CegConjecture::getNextDecisionRequest(unsigned& priority) -{ - // 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(); -} - CegConjecture::SygusStreamDecisionStrategy::SygusStreamDecisionStrategy( context::Context* satContext, Valuation valuation) : DecisionStrategyFmf(satContext, valuation) diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h index 41ec6ab9e..adc75056e 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -50,8 +50,6 @@ public: Node getConjecture() { return d_quant; } /** get deep embedding version of conjecture */ 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 */ diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp index c59195746..d30cccd87 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp @@ -255,17 +255,6 @@ void CegInstantiation::registerQuantifier(Node q) } } -Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) { - if( d_conj->isAssigned() ){ - Node dec_req = d_conj->getNextDecisionRequest( priority ); - if( !dec_req.isNull() ){ - Trace("cegqi-debug") << "CEGQI : Decide next on : " << dec_req << "..." << std::endl; - return dec_req; - } - } - return Node::null(); -} - void CegInstantiation::checkConjecture(CegConjecture* conj) { Node q = conj->getEmbeddedConjecture(); diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/ce_guided_instantiation.h index 9c81b6978..6bf33effb 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.h @@ -60,8 +60,6 @@ public: void check(Theory::Effort e, QEffort quant_e) override; /* Called for new quantifiers */ void registerQuantifier(Node q) override; - /** get the next decision request */ - Node getNextDecisionRequest(unsigned& priority) override; /** Identify this module (for debugging, dynamic configuration, etc..) */ std::string identify() const override { return "CegInstantiation"; } /** print solution for synthesis conjectures */ diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 19b0ad717..56cc40244 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_unif_rl.h" #include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/theory_engine.h" using namespace CVC4::kind; @@ -122,7 +123,7 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, NodeManager* nm = NodeManager::currentNM(); Valuation& valuation = d_qe->getValuation(); bool addedUnifEnumSymBreakLemma = false; - Node cost_lit = d_u_enum_manager.getCurrentLiteral(); + Node cost_lit = d_u_enum_manager.getAssertedLiteral(); std::map> unif_enums[2]; std::map> unif_values[2]; for (const Node& c : d_unif_candidates) @@ -171,7 +172,7 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, if (index == 0) { // given a pool of unification enumerators eu_1, ..., eu_n, - // CegisUnifEnumManager insists that size(eu_1) <= ... <= size(eu_n). + // CegisUnifEnumDecisionStrategy insists that size(eu_1) <= ... <= size(eu_n). // We additionally insist that M(eu_i) < M(eu_{i+1}) when // size(eu_i) = size(eu_{i+1}), where < is pointer comparison. // We enforce this below by adding symmetry breaking lemmas of the @@ -298,23 +299,112 @@ 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, +CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, CegConjecture* parent) - : d_qe(qe), - d_parent(parent), - d_ret_dec(qe->getSatContext(), false), - d_curr_guq_val(qe->getSatContext(), 0) + : DecisionStrategyFmf(qe->getSatContext(), qe->getValuation()), + d_qe(qe), + d_parent(parent) { d_initialized = false; d_tds = d_qe->getTermDatabaseSygus(); } -void CegisUnifEnumManager::initialize( +Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) +{ + NodeManager* nm = NodeManager::currentNM(); + Node new_lit = nm->mkSkolem("G_cost", nm->booleanType()); + unsigned new_size = n + 1; + + // allocate an enumerator for each candidate + for (std::pair& ci : d_ce_info) + { + Node c = ci.first; + TypeNode ct = c.getType(); + Node eu = nm->mkSkolem("eu", ct); + Node ceu; + if (!options::sygusUnifCondIndependent() && !ci.second.d_enums[0].empty()) + { + // make a new conditional enumerator as well, starting the + // second type around + ceu = nm->mkSkolem("cu", ci.second.d_ce_type); + } + // register the new enumerators + for (unsigned index = 0; index < 2; index++) + { + Node e = index == 0 ? eu : ceu; + if (e.isNull()) + { + continue; + } + setUpEnumerator(e, ci.second, index); + } + } + // register the evaluation points at the new value + for (std::pair& ci : d_ce_info) + { + Node c = ci.first; + for (const Node& ei : ci.second.d_eval_points) + { + Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei + << " to new size " << new_size << "\n"; + registerEvalPtAtSize(c, ei, new_lit, new_size); + } + } + // enforce fairness between number of enumerators and enumerator size + if (new_size > 1) + { + // construct the "virtual enumerator" + if (d_virtual_enum.isNull()) + { + // we construct the default integer grammar with no variables, e.g.: + // A -> 0 | 1 | A+A + TypeNode intTn = nm->integerType(); + // use a null variable list + Node bvl; + std::stringstream ss; + ss << "_virtual_enum_grammar"; + std::string virtualEnumName(ss.str()); + std::map> extra_cons; + std::map> exclude_cons; + // do not include "-", which is included by default for integers + exclude_cons[intTn].push_back(nm->operatorOf(MINUS)); + std::unordered_set term_irrelevant; + TypeNode vtn = CegGrammarConstructor::mkSygusDefaultType(intTn, + bvl, + virtualEnumName, + extra_cons, + exclude_cons, + term_irrelevant); + d_virtual_enum = nm->mkSkolem("_ve", vtn); + d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent); + } + // if new_size is a power of two, then isPow2 returns log2(new_size)+1 + // otherwise, this returns 0. In the case it returns 0, we don't care + // since the floor( log2( i ) ) = floor( log2( i - 1 ) ) and we do not + // increase our size bound. + unsigned pow_two = Integer(new_size).isPow2(); + if (pow_two > 0) + { + Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum); + Node fair_lemma = + nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1))); + fair_lemma = nm->mkNode(OR, new_lit, fair_lemma); + Trace("cegis-unif-enum-lemma") + << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n"; + // this lemma relates the number of conditions we enumerate and the + // maximum size of a term that is part of our solution. It is of the + // form: + // G_uq_i => size(ve) >= log_2( i-1 ) + // In other words, if we use i conditions, then we allow terms in our + // solution whose size is at most log_2(i-1). + d_qe->getOutputChannel().lemma(fair_lemma); + } + } + + return new_lit; +} + +void CegisUnifEnumDecisionStrategy::initialize( const std::vector& es, const std::map& e_to_cond, const std::map>& strategy_lemmas) @@ -360,8 +450,11 @@ void CegisUnifEnumManager::initialize( std::pair(d_sbt_lemma, sp); } } - // initialize the current literal - incrementNumEnumerators(); + + // register this strategy + d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy( + DecisionManager::STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS, this); + // create single condition enumerator for each decision tree strategy if (options::sygusUnifCondIndependent()) { @@ -375,13 +468,15 @@ void CegisUnifEnumManager::initialize( } } -void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e, +void CegisUnifEnumDecisionStrategy::getEnumeratorsForStrategyPt(Node e, std::vector& es, unsigned index) const { // the number of active enumerators is related to the current cost value - unsigned num_enums = d_curr_guq_val.get(); - Assert(num_enums > 0); + unsigned num_enums = 0; + bool has_num_enums = getAssertedLiteralIndex(num_enums); + AlwaysAssert(has_num_enums); + num_enums = num_enums + 1; if (index == 1) { // we always use (cost-1) conditions, or 1 if in the indepedent case @@ -398,13 +493,13 @@ void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e, } } -Node CegisUnifEnumManager::getActiveGuardForEnumerator(Node e) +Node CegisUnifEnumDecisionStrategy::getActiveGuardForEnumerator(Node e) { Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); return d_enum_to_active_guard[e]; } -void CegisUnifEnumManager::setUpEnumerator(Node e, +void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, StrategyPtInfo& si, unsigned index) { @@ -439,7 +534,7 @@ void CegisUnifEnumManager::setUpEnumerator(Node e, e, si.d_pt, d_parent, options::sygusUnifCondIndependent() && index == 1); } -void CegisUnifEnumManager::registerEvalPts(const std::vector& eis, Node e) +void CegisUnifEnumDecisionStrategy::registerEvalPts(const std::vector& eis, Node e) { // candidates of the same type are managed std::map::iterator it = d_ce_info.find(e); @@ -450,163 +545,17 @@ void CegisUnifEnumManager::registerEvalPts(const std::vector& eis, Node e) for (const Node& ei : eis) { Assert(ei.getType() == e.getType()); - for (const std::pair& p : d_guq_lit) + for (unsigned j = 0, size = d_literals.size(); j < size; j++) { Trace("cegis-unif-enum") << "...for cand " << e << " adding hd " << ei - << " at size " << p.first << "\n"; - registerEvalPtAtSize(e, ei, p.second, p.first); + << " at size " << j << "\n"; + registerEvalPtAtSize(e, ei, d_literals[j], j + 1); } } } -Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority) -{ - // are we not initialized or have we returned our decision in the current SAT - // context? - if (!d_initialized || d_ret_dec.get()) - { - return Node::null(); - } - 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)) - { - priority = 1; - return lit; - } - else if (!value) - { - // propagated false, increment - incrementNumEnumerators(); - return getNextDecisionRequest(priority); - } - d_ret_dec = true; - return Node::null(); -} - -void CegisUnifEnumManager::incrementNumEnumerators() -{ - unsigned new_size = d_curr_guq_val.get() + 1; - d_curr_guq_val.set(new_size); - // ensure that the literal has been allocated - std::map::iterator itc = d_guq_lit.find(new_size); - if (itc == d_guq_lit.end()) - { - // allocate the new literal - NodeManager* nm = NodeManager::currentNM(); - Node new_lit = Rewriter::rewrite(nm->mkSkolem("G_cost", nm->booleanType())); - new_lit = d_qe->getValuation().ensureLiteral(new_lit); - AlwaysAssert(!new_lit.isNull()); - d_qe->getOutputChannel().requirePhase(new_lit, true); - d_guq_lit[new_size] = new_lit; - // allocate an enumerator for each candidate - for (std::pair& ci : d_ce_info) - { - Node c = ci.first; - TypeNode ct = c.getType(); - Node eu = nm->mkSkolem("eu", ct); - Node ceu; - if (!options::sygusUnifCondIndependent() && !ci.second.d_enums[0].empty()) - { - // make a new conditional enumerator as well, starting the - // second type around - ceu = nm->mkSkolem("cu", ci.second.d_ce_type); - } - // register the new enumerators - for (unsigned index = 0; index < 2; index++) - { - Node e = index == 0 ? eu : ceu; - if (e.isNull()) - { - continue; - } - setUpEnumerator(e, ci.second, index); - } - } - // register the evaluation points at the new value - for (std::pair& ci : d_ce_info) - { - Node c = ci.first; - for (const Node& ei : ci.second.d_eval_points) - { - Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei - << " to new size " << new_size << "\n"; - registerEvalPtAtSize(c, ei, new_lit, new_size); - } - } - // enforce fairness between number of enumerators and enumerator size - if (new_size > 1) - { - // construct the "virtual enumerator" - if (d_virtual_enum.isNull()) - { - // we construct the default integer grammar with no variables, e.g.: - // A -> 0 | 1 | A+A - TypeNode intTn = nm->integerType(); - // use a null variable list - Node bvl; - std::stringstream ss; - ss << "_virtual_enum_grammar"; - std::string virtualEnumName(ss.str()); - std::map> extra_cons; - std::map> exclude_cons; - // do not include "-", which is included by default for integers - exclude_cons[intTn].push_back(nm->operatorOf(MINUS)); - std::unordered_set term_irrelevant; - TypeNode vtn = - CegGrammarConstructor::mkSygusDefaultType(intTn, - bvl, - virtualEnumName, - extra_cons, - exclude_cons, - term_irrelevant); - d_virtual_enum = nm->mkSkolem("_ve", vtn); - d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent); - } - // if new_size is a power of two, then isPow2 returns log2(new_size)+1 - // otherwise, this returns 0. In the case it returns 0, we don't care - // since the floor( log2( i ) ) = floor( log2( i - 1 ) ) and we do not - // increase our size bound. - unsigned pow_two = Integer(new_size).isPow2(); - if (pow_two > 0) - { - Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum); - Node fair_lemma = - nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1))); - fair_lemma = nm->mkNode(OR, new_lit, fair_lemma); - Trace("cegis-unif-enum-lemma") - << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n"; - // this lemma relates the number of conditions we enumerate and the - // maximum size of a term that is part of our solution. It is of the - // form: - // G_uq_i => size(ve) >= log_2( i-1 ) - // In other words, if we use i conditions, then we allow terms in our - // solution whose size is at most log_2(i-1). - d_qe->getOutputChannel().lemma(fair_lemma); - } - } - } -} - -Node CegisUnifEnumManager::getCurrentLiteral() const -{ - return getLiteral(d_curr_guq_val.get()); -} - -Node CegisUnifEnumManager::getLiteral(unsigned n) const -{ - std::map::const_iterator itc = d_guq_lit.find(n); - Assert(itc != d_guq_lit.end()); - return itc->second; -} -void CegisUnifEnumManager::registerEvalPtAtSize(Node e, +void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e, Node ei, Node guq_lit, unsigned n) diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 69d6ee25f..ae2d7964b 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -26,9 +26,9 @@ namespace CVC4 { namespace theory { namespace quantifiers { -/** Cegis Unif Enumeration Manager +/** Cegis Unif Enumerators Decision Strategy * - * This class enforces a decision heuristic that limits the number of + * This class enforces a decision strategy that limits the number of * unique values given to the set of heads of evaluation points and conditions * enumerators for these points, which are variables of sygus datatype type that * are introduced by CegisUnif. @@ -42,12 +42,24 @@ namespace quantifiers { * To enforce this, we introduce sygus enumerator(s) of the same type as the * heads of evaluation points and condition enumerators registered to this class * and add lemmas that enforce that these terms are equal to at least one - * enumerator (see registerEvalPtAtValue). + * enumerator (see registerEvalPtAtSize). */ -class CegisUnifEnumManager +class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf { public: - CegisUnifEnumManager(QuantifiersEngine* qe, CegConjecture* parent); + CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, CegConjecture* parent); + /** Make the n^th literal of this strategy (G_uq_n). + * + * This call may add new lemmas of the form described above + * registerEvalPtAtValue on the output channel of d_qe. + */ + Node mkLiteral(unsigned n) override; + /** identify */ + std::string identify() const override + { + return std::string("cegis_unif_num_enums"); + } + /** initialize candidates * * Notify this class that it will be managing enumerators for the vector @@ -73,29 +85,11 @@ class CegisUnifEnumManager * for strategy point e, where e was passed to initialize in the vector es. * * This may add new lemmas of the form described above - * registerEvalPtAtValue on the output channel of d_qe. + * registerEvalPtAtSize on the output channel of d_qe. */ void registerEvalPts(const std::vector& eis, Node e); /** Retrieves active guard for enumerator */ Node getActiveGuardForEnumerator(Node e); - /** 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); - /** - * 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; - private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; @@ -143,10 +137,6 @@ class CegisUnifEnumManager }; /** map strategy points 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 "virtual" enumerator * * This enumerator is used for enforcing fairness. In particular, we relate @@ -165,11 +155,6 @@ class CegisUnifEnumManager * (0,8), ..., (0,15), (1,8), ..., (1,15), ... [size 3] */ Node d_virtual_enum; - /** - * The minimal n such that G_uq_n is not asserted negatively in the - * current SAT context. - */ - context::CDO d_curr_guq_val; /** Registers an enumerator and adds symmetry breaking lemmas * * The symmetry breaking lemmas are generated according to the stored @@ -179,10 +164,6 @@ class CegisUnifEnumManager * order of size. */ void setUpEnumerator(Node e, StrategyPtInfo& si, unsigned index); - /** increment the number of enumerators */ - void incrementNumEnumerators(); - /** get literal G_uq_n */ - Node getLiteral(unsigned n) const; /** register evaluation point at size * * This sends a lemma of the form: @@ -246,8 +227,6 @@ 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: /** do cegis-implementation-specific initialization for this class */ @@ -288,7 +267,7 @@ class CegisUnif : public Cegis */ SygusUnifRl d_sygus_unif; /** enumerator manager utility */ - CegisUnifEnumManager d_u_enum_manager; + CegisUnifEnumDecisionStrategy d_u_enum_manager; /* The null node */ Node d_null; /** the unification candidates */ diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 52b6aea0a..e2a9fae80 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -114,14 +114,6 @@ 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(); - } /** * Are we trying to repair constants in candidate solutions? * If we return true for usingRepairConst is true, then this module has