From 3ca59fea3c2ddbe170830a0fc499254605e1d3c4 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 15 May 2018 12:20:13 -0500 Subject: [PATCH] Building and refining solutions with dynamic condition generation in CegisUnif (#1920) --- src/theory/quantifiers/lazy_trie.cpp | 6 ++ src/theory/quantifiers/lazy_trie.h | 3 + src/theory/quantifiers/sygus/cegis_unif.cpp | 94 +++++++++++++++---- src/theory/quantifiers/sygus/cegis_unif.h | 10 +- .../quantifiers/sygus/sygus_unif_rl.cpp | 85 +++++++++++------ src/theory/quantifiers/sygus/sygus_unif_rl.h | 53 +++++++---- 6 files changed, 181 insertions(+), 70 deletions(-) diff --git a/src/theory/quantifiers/lazy_trie.cpp b/src/theory/quantifiers/lazy_trie.cpp index 21a87c792..33d8adaa1 100644 --- a/src/theory/quantifiers/lazy_trie.cpp +++ b/src/theory/quantifiers/lazy_trie.cpp @@ -148,6 +148,12 @@ Node LazyTrieMulti::add(Node f, LazyTrieEvaluator* ev, unsigned ntotal) return res; } +void LazyTrieMulti::clear() +{ + d_trie.clear(); + d_rep_to_class.clear(); +} + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h index 935b9bec1..3585247c6 100644 --- a/src/theory/quantifiers/lazy_trie.h +++ b/src/theory/quantifiers/lazy_trie.h @@ -159,6 +159,9 @@ class LazyTrieMulti * containing only itself. */ Node add(Node f, LazyTrieEvaluator* ev, unsigned ntotal); + /** clear the trie */ + void clear(); + /** A regular lazy trie */ LazyTrie d_trie; }; diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 920b142bb..8db60d373 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -68,8 +68,8 @@ bool CegisUnif::initialize(Node n, { Node cond = d_sygus_unif.getConditionForEvaluationPoint(e); Assert(!cond.isNull()); - Trace("cegis-unif") - << " " << e << " with condition : " << cond << std::endl; + Trace("cegis-unif") << " " << e << " with condition : " << cond + << std::endl; pt_to_cond[e] = cond; } } @@ -123,6 +123,8 @@ bool CegisUnif::constructCandidates(const std::vector& enums, // build the values of the condition enumerators for each strategy point std::map> condition_map; Trace("cegis-unif-enum") << "Register new enumerated values :\n"; + // keep track of the relation between conditional enums and their values + NodePairMap cenum_to_value; for (unsigned i = 0, size = enums.size(); i < size; ++i) { // Non-unif enums (which are the very candidates) should not be notified @@ -144,6 +146,7 @@ bool CegisUnif::constructCandidates(const std::vector& enums, std::map::iterator itc = d_cenum_to_strat_pt.find(e); if (itc != d_cenum_to_strat_pt.end()) { + cenum_to_value[e] = v; Trace("cegis-unif-enum") << " ...this is a condition for " << e << "\n"; // it is the value of a current condition condition_map[itc->second].push_back(v); @@ -160,8 +163,6 @@ bool CegisUnif::constructCandidates(const std::vector& enums, d_sygus_unif.setConditions(cs.first, cs.second); } // TODO : check symmetry breaking for enumerators - // TODO : check separation of evaluation heads wrt condition enumerators and - // add lemmas. // build solutions (for unif candidates a divide-and-conquer approach is used) std::vector sols; if (d_sygus_unif.constructSolution(sols)) @@ -179,6 +180,48 @@ bool CegisUnif::constructCandidates(const std::vector& enums, } return true; } + std::map> sepPairs; + if (d_sygus_unif.getSeparationPairs(sepPairs)) + { + // Build separation lemma based on current size, and for each heads that + // could not be separated, the condition values currently enumerated for its + // decision tree + NodeManager* nm = NodeManager::currentNM(); + Node neg_cost_lit = d_u_enum_manager.getCurrentLiteral().negate(); + std::vector cenums, cond_eqs; + for (std::pair>& np : sepPairs) + { + // Build equalities between condition enumerators associated with the + // strategy point whose decision tree could not separate the given heads + d_u_enum_manager.getCondEnumeratorsForStrategyPt(np.first, cenums); + for (const Node& ce : cenums) + { + Assert(cenum_to_value.find(ce) != cenum_to_value.end()); + cond_eqs.push_back(nm->mkNode(EQUAL, ce, cenum_to_value[ce])); + } + Assert(!cond_eqs.empty()); + Node neg_conds_lit = + cond_eqs.size() > 1 ? nm->mkNode(AND, cond_eqs) : cond_eqs[0]; + neg_conds_lit = neg_conds_lit.negate(); + for (const Node& eq : np.second) + { + // A separation lemma is of the shape + // (cost_n+1 ^ (c_1 = M(c_1) ^ ... ^ M(c_n))) => e_i = e_j + // in which cost_n+1 is the cost function for the size n+1, each c_k is + // a conditional enumerator associated with the respective decision + // tree, each M(c_k) its current model value, and e_i, e_j are two + // distinct heads that could not be separated by these condition values + // + // Such a lemma will force the ground solver, within the restrictions of + // the respective cost function, to make e_i and e_j equal or to come up + // with new values for the conditional enumerators such that we can try + Node sep_lemma = nm->mkNode(OR, neg_cost_lit, neg_conds_lit, eq); + Trace("cegis-unif") + << "CegisUnif::lemma, separation lemma : " << sep_lemma << "\n"; + d_qe->getOutputChannel().lemma(sep_lemma); + } + } + } return false; } @@ -194,7 +237,12 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, // Notify the enumeration manager if there are new evaluation points for (const std::pair>& ep : eval_pts) { - d_u_enum_manager.registerEvalPts(ep.second, ep.first); + Assert(d_cand_to_strat_pt.find(ep.first) != d_cand_to_strat_pt.end()); + // Notify each startegy point of the respective candidate + for (const Node& n : d_cand_to_strat_pt[ep.first]) + { + d_u_enum_manager.registerEvalPts(ep.second, n); + } } // Make the refinement lemma and add it to lems. This lemma is guarded by the // parent's guard, which has the semantics "this conjecture has a solution", @@ -242,8 +290,8 @@ void CegisUnifEnumManager::initialize( std::map::const_iterator itcc = e_to_cond.find(e); Assert(itcc != e_to_cond.end()); Node cond = itcc->second; - Trace("cegis-unif-enum-debug") - << "...its condition strategy point is " << cond << "\n"; + Trace("cegis-unif-enum-debug") << "...its condition strategy point is " + << cond << "\n"; d_ce_info[e].d_ce_type = cond.getType(); // initialize the symmetry breaking lemma templates for (unsigned index = 0; index < 2; index++) @@ -366,9 +414,6 @@ void CegisUnifEnumManager::incrementNumEnumerators() { continue; } - // register the enumerator - ci.second.d_enums[index].push_back(e); - d_tds->registerEnumerator(e, ci.second.d_pt, d_parent); // instantiate template for removing redundant operators if (!ci.second.d_sbt_lemma_tmpl[index].first.isNull()) { @@ -381,21 +426,34 @@ void CegisUnifEnumManager::incrementNumEnumerators() d_qe->getOutputChannel().lemma(sym_break_red_ops); } // symmetry breaking between enumerators - Node e_prev = ci.second.d_enums[index].back(); - Node size_e = nm->mkNode(DT_SIZE, e); - Node size_e_prev = nm->mkNode(DT_SIZE, e_prev); - Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev); - Trace("cegis-unif-enum-lemma") - << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n"; - d_qe->getOutputChannel().lemma(sym_break); + if (!ci.second.d_enums[index].empty()) + { + Node e_prev = ci.second.d_enums[index].back(); + Node size_e = nm->mkNode(DT_SIZE, e); + Node size_e_prev = nm->mkNode(DT_SIZE, e_prev); + Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev); + Trace("cegis-unif-enum-lemma") + << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n"; + d_qe->getOutputChannel().lemma(sym_break); + } + // register the enumerator + ci.second.d_enums[index].push_back(e); + Trace("cegis-unif-enum") << "* Registering new enumerator " << e + << " to strategy point " << ci.second.d_pt + << "\n"; + d_tds->registerEnumerator(e, ci.second.d_pt, d_parent); // if the sygus datatype is interpreted as an infinite type // (this should be the case for almost all examples) TypeNode et = e.getType(); if (!et.isInterpretedFinite()) { // it is disequal from all previous ones - for (const Node ei : ci.second.d_enums[index]) + for (const Node& ei : ci.second.d_enums[index]) { + if (ei == e) + { + continue; + } Node deq = e.eqNode(ei).negate(); Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, enum deq:" << deq << "\n"; diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 445ab5f6c..ce096b127 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -82,6 +82,11 @@ class CegisUnifEnumManager * 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 */ @@ -138,11 +143,6 @@ class CegisUnifEnumManager 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 diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index f59331d68..f7337a92d 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -100,8 +100,8 @@ Node SygusUnifRl::purifyLemma(Node n, else { nv = d_parent->getModelValue(n); - Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << n - << " is " << nv << "\n"; + Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << n + << " is " << nv << "\n"; } Assert(n != nv); } @@ -263,10 +263,11 @@ Node SygusUnifRl::addRefLemma(Node lemma, for (const Node& stratpt : d_cenum_to_stratpt[cenum]) { Assert(d_stratpt_to_dt.find(stratpt) != d_stratpt_to_dt.end()); - Trace("sygus-unif-rl-dt") << "Add point with head " << cp.second[j] - << " to strategy point " << stratpt << "\n"; + Trace("sygus-unif-rl-dt") << "Register point with head " + << cp.second[j] << " to strategy point " + << stratpt << "\n"; // Register new point from new head - d_stratpt_to_dt[stratpt].addPoint(cp.second[j]); + d_stratpt_to_dt[stratpt].d_hds.push_back(cp.second[j]); } } } @@ -275,18 +276,17 @@ Node SygusUnifRl::addRefLemma(Node lemma, return plem; } -void SygusUnifRl::initializeConstructSol() {} +void SygusUnifRl::initializeConstructSol() { d_sepPairs.clear(); } void SygusUnifRl::initializeConstructSolFor(Node f) {} bool SygusUnifRl::constructSolution(std::vector& sols) { initializeConstructSol(); + bool successful = true; for (const Node& c : d_candidates) { if (!usingUnif(c)) { Node v = d_parent->getModelValue(c); - Trace("sygus-unif-rl-sol") << "Adding solution " << v - << " to non-unif candidate " << c << "\n"; sols.push_back(v); continue; } @@ -294,14 +294,15 @@ bool SygusUnifRl::constructSolution(std::vector& sols) Node v = constructSol(c, d_strategy[c].getRootEnumerator(), role_equal, 0); if (v.isNull()) { - return false; + // we continue trying to build solutions to accumulate potentitial + // separation conditions from other decision trees + successful = false; + continue; } - Trace("sygus-unif-rl-sol") << "Adding solution " << v - << " to unif candidate " << c << "\n"; sols.push_back(v); d_cand_to_sol[c] = v; } - return true; + return successful; } Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind) @@ -333,7 +334,21 @@ Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind) return d_parent->getModelValue(e); } EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()]; - return itd->second.buildSol(etis->d_cons); + std::vector toSeparate; + Node sol = itd->second.buildSol(etis->d_cons, toSeparate); + if (sol.isNull()) + { + Assert(!toSeparate.empty()); + d_sepPairs[e] = toSeparate; + } + return sol; +} + +bool SygusUnifRl::getSeparationPairs( + std::map>& sepPairs) +{ + sepPairs = d_sepPairs; + return !sepPairs.empty(); } bool SygusUnifRl::usingUnif(Node f) const @@ -352,13 +367,8 @@ void SygusUnifRl::setConditions(Node e, const std::vector& conds) { std::map::iterator it = d_stratpt_to_dt.find(e); Assert(it != d_stratpt_to_dt.end()); - it->second.clearCondValues(); - /* TODO - for (const Node& c : conds) - { - it->second.addCondValue(c); - } - */ + // Clear previous trie + it->second.resetPointSeparator(conds); } std::vector SygusUnifRl::getEvalPointHeads(Node c) @@ -477,15 +487,19 @@ void SygusUnifRl::DecisionTreeInfo::initialize(Node cond_enum, d_pt_sep.initialize(this); } -void SygusUnifRl::DecisionTreeInfo::addPoint(Node f) +void SygusUnifRl::DecisionTreeInfo::resetPointSeparator( + const std::vector& conds) { - d_pt_sep.d_trie.add(f, &d_pt_sep, d_conds.size()); + // clear old condition values and trie + d_conds.clear(); + d_pt_sep.d_trie.clear(); + // set new condition values + d_conds.insert(d_conds.end(), conds.begin(), conds.end()); } -void SygusUnifRl::DecisionTreeInfo::clearCondValues() +void SygusUnifRl::DecisionTreeInfo::addPoint(Node f) { - // TODO - // d_conds.clear(); + d_pt_sep.d_trie.add(f, &d_pt_sep, d_conds.size()); } void SygusUnifRl::DecisionTreeInfo::addCondValue(Node condv) @@ -501,14 +515,15 @@ unsigned SygusUnifRl::DecisionTreeInfo::getStrategyIndex() const using UNodePair = std::pair; -Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons) +Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, + std::vector& toSeparate) { if (!d_template.first.isNull()) { Trace("sygus-unif-sol") << "...templated conditions unsupported\n"; return Node::null(); } - if (!isSeparated()) + if (!isSeparated(toSeparate)) { Trace("sygus-unif-sol") << "...separation check failed\n"; return Node::null(); @@ -592,9 +607,16 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons) return cache[root]; } -bool SygusUnifRl::DecisionTreeInfo::isSeparated() +bool SygusUnifRl::DecisionTreeInfo::isSeparated(std::vector& toSeparate) { + // build point separator + for (const Node& f : d_hds) + { + addPoint(f); + } + // check separation d_hd_values.clear(); + NodeManager* nm = NodeManager::currentNM(); for (const std::pair>& rep_to_class : d_pt_sep.d_trie.d_rep_to_class) { @@ -639,11 +661,14 @@ bool SygusUnifRl::DecisionTreeInfo::isSeparated() Trace("sygus-unif-rl-dt") << "...in sep class heads with diff values: " << rep_to_class.second[0] << " and " << rep_to_class.second[i] << "\n"; - return false; + toSeparate.push_back( + nm->mkNode(EQUAL, rep_to_class.second[0], rep_to_class.second[i])); + // For non-separation suffices to consider one head pair per sep class + break; } } } - return true; + return toSeparate.empty(); } void SygusUnifRl::DecisionTreeInfo::PointSeparator::initialize( diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index b5609e625..5bd6cdc1e 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -97,6 +97,15 @@ class SygusUnifRl : public SygusUnif /** retrieve the head of evaluation points for candidate c, if any */ std::vector getEvalPointHeads(Node c); + /** + * if a separation condition is necessary after a failed solution + * construction, then sepCond is assigned a pair (e, fi = fj) in which e is + * the strategy point and fi, fj head of evaluation points of a unif + * function-to-synthesize, such that fi could not be separated from fj by the + * current condition values + */ + bool getSeparationPairs(std::map>& sepPairs); + protected: /** reference to the parent conjecture */ CegConjecture* d_parent; @@ -114,6 +123,12 @@ class SygusUnifRl : public SygusUnif void initializeConstructSolFor(Node f) override; /** maps unif functions-to~synhesize to their last built solutions */ std::map d_cand_to_sol; + /** pair of strategy point and equality between evaluation point heads + * + * this pair is set when a unif solution cannot be built because a two + * evaluation point heads cannot be separated + */ + std::map> d_sepPairs; /* -------------------------------------------------------------- Purification @@ -190,12 +205,6 @@ class SygusUnifRl : public SygusUnif SygusUnifRl* unif, SygusUnifStrategy* strategy, unsigned strategy_index); - /** adds the respective evaluation point of the head f */ - void addPoint(Node f); - /** clears the condition values */ - void clearCondValues(); - /** adds a condition value to the pool of condition values */ - void addCondValue(Node condv); /** returns index of strategy information of strategy node for this DT */ unsigned getStrategyIndex() const; /** builds solution stored in DT, if any, using the given constructor @@ -203,22 +212,29 @@ class SygusUnifRl : public SygusUnif * The DT contains a solution when no class contains two heads of evaluation * points with different model values, i.e. when all points that must be * separated indeed are separated. + */ + Node buildSol(Node cons, std::vector& toSeparate); + /** whether all points that must be separated are separated * - * This function tests separation of the points in the above sense and may - * create separation lemmas to enforce guide the synthesis of conditons that - * will separate points not currently separated. + * This function tests separation of the points in the above sense and in + * case two heads cannot be separated, an equality between them is created + * and stored in toSeparate, so that a separation lemma can be generated to + * guide the synthesis search to yield either conditions that will separate + * these heads or equal values to them. */ - Node buildSol(Node cons); - /** whether all points that must be separated are separated **/ - bool isSeparated(); + bool isSeparated(std::vector& toSeparate); /** reference to parent unif util */ SygusUnifRl* d_unif; /** enumerator template (if no templates, nodes in pair are Node::null()) */ NodePair d_template; /** enumerated condition values */ std::vector d_conds; + /** gathered evaluation point heads */ + std::vector d_hds; /** get condition enumerator */ Node getConditionEnumerator() const { return d_cond_enum; } + /** clear trie and registered condition values */ + void resetPointSeparator(const std::vector& conds); private: /** @@ -268,6 +284,10 @@ class SygusUnifRl : public SygusUnif * enumerated condiotion values */ PointSeparator d_pt_sep; + /** adds the respective evaluation point of the head f to d_pt_sep */ + void addPoint(Node f); + /** adds a value to the pool of condition values and to d_pt_sep */ + void addCondValue(Node condv); }; /** maps strategy points in the strategy tree to the above data */ std::map d_stratpt_to_dt; @@ -301,11 +321,10 @@ class SygusUnifRl : public SygusUnif * Registers that cond is a conditional enumerator for building a (recursive) * decision tree at strategy node e within the strategy tree of f. */ - void registerConditionalEnumerator( - Node f, - Node e, - Node cond, - unsigned strategy_index); + void registerConditionalEnumerator(Node f, + Node e, + Node cond, + unsigned strategy_index); }; } /* CVC4::theory::quantifiers namespace */ -- 2.30.2