From ef1e8fd92dc24fc02754c9573c1dac6c473bf2ca Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 3 Oct 2018 14:48:44 -0500 Subject: [PATCH] Make CegisUnif with condition independent robust to var agnostic (#2565) --- src/theory/quantifiers/sygus/cegis_unif.cpp | 187 ++++++++++++-------- src/theory/quantifiers/sygus/cegis_unif.h | 32 +++- 2 files changed, 144 insertions(+), 75 deletions(-) diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 56edc55c6..d71139eef 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -124,39 +124,23 @@ void CegisUnif::getTermList(const std::vector& candidates, } } -bool CegisUnif::processConstructCandidates(const std::vector& enums, - const std::vector& enum_values, - const std::vector& candidates, - std::vector& candidate_values, - bool satisfiedRl, - std::vector& lems) +bool CegisUnif::getEnumValues(const std::vector& enums, + const std::vector& enum_values, + std::map>& unif_cenums, + std::map>& unif_cvalues, + std::vector& lems) { - if (d_unif_candidates.empty()) - { - Assert(d_non_unif_candidates.size() == candidates.size()); - return Cegis::processConstructCandidates( - enums, enum_values, candidates, candidate_values, satisfiedRl, lems); - } - if (!satisfiedRl) - { - Trace("cegis-unif") - << "..added refinement lemmas\n---CegisUnif Engine---\n"; - // if we didn't satisfy the specification, there is no way to repair - return false; - } + NodeManager* nm = NodeManager::currentNM(); + Node cost_lit = d_u_enum_manager.getAssertedLiteral(); + std::map> unif_renums, unif_rvalues; // build model value map std::map mvMap; for (unsigned i = 0, size = enums.size(); i < size; i++) { mvMap[enums[i]] = enum_values[i]; } - // the unification enumerators (return values, conditions) and their model - // values - NodeManager* nm = NodeManager::currentNM(); bool addedUnifEnumSymBreakLemma = false; - Node cost_lit = d_u_enum_manager.getAssertedLiteral(); - std::map> unif_enums[2]; - std::map> unif_values[2]; + // populate maps between unification enumerators and their model values for (const Node& c : d_unif_candidates) { // for each decision tree strategy allocated for c (these are referenced @@ -165,24 +149,28 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, { for (unsigned index = 0; index < 2; index++) { + std::vector es, vs; Trace("cegis") << " " << (index == 0 ? "Return values" : "Conditions") << " for " << e << ":\n"; // get the current unification enumerators - d_u_enum_manager.getEnumeratorsForStrategyPt( - e, unif_enums[index][e], index); - if (index == 1 && options::sygusUnifCondIndependent()) + d_u_enum_manager.getEnumeratorsForStrategyPt(e, es, index); + // set enums for condition enumerators + if (index == 1) { - Assert(unif_enums[index][e].size() == 1); - Node eu = unif_enums[index][e][0]; - if (mvMap.find(eu) == mvMap.end()) + if (options::sygusUnifCondIndependent()) { - Trace("cegis") << " " << eu << " -> N/A\n"; - unif_enums[index][e].clear(); - continue; + Assert(es.size() == 1); + // whether valueus exhausted + if (mvMap.find(es[0]) == mvMap.end()) + { + Trace("cegis") << " " << es[0] << " -> N/A\n"; + es.clear(); + } } + unif_cenums[e] = es; } // get the model value of each enumerator - for (const Node& eu : unif_enums[index][e]) + for (const Node& eu : es) { Assert(mvMap.find(eu) != mvMap.end()); Node m_eu = mvMap[eu]; @@ -194,14 +182,19 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, ->toStreamSygus(ss, m_eu); Trace("cegis") << ss.str() << std::endl; } - unif_values[index][e].push_back(m_eu); + vs.push_back(m_eu); + } + // set values for condition enumerators of e + if (index == 1) + { + unif_cvalues[e] = vs; } // inter-enumerator symmetry breaking for return values - if (index == 0) + else { // given a pool of unification enumerators eu_1, ..., eu_n, - // CegisUnifEnumDecisionStrategy insists that size(eu_1) <= ... <= size(eu_n). - // We additionally insist that M(eu_i) < M(eu_{i+1}) when + // 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 // form ~( eu_i = M(eu_i) ^ eu_{i+1} = M(eu_{i+1} ) ) @@ -209,11 +202,10 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, // we only do this for return value enumerators, since condition // enumerators cannot be ordered (their order is based on the // seperation resolution scheme during model construction). - for (unsigned j = 1, nenum = unif_values[index][e].size(); j < nenum; - j++) + for (unsigned j = 1, nenum = vs.size(); j < nenum; j++) { - Node prev_val = unif_values[index][e][j - 1]; - Node curr_val = unif_values[index][e][j]; + Node prev_val = vs[j - 1]; + Node curr_val = vs[j]; // compare the node values if (curr_val < prev_val) { @@ -223,12 +215,10 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, Assert(prev_size <= curr_size); if (curr_size == prev_size) { - Node slem = nm->mkNode(AND, - unif_enums[index][e][j - 1].eqNode( - unif_values[index][e][j - 1]), - unif_enums[index][e][j].eqNode( - unif_values[index][e][j])) - .negate(); + Node slem = + nm->mkNode( + AND, es[j - 1].eqNode(vs[j - 1]), es[j].eqNode(vs[j])) + .negate(); Trace("cegis-unif") << "CegisUnif::lemma, inter-unif-enumerator " "symmetry breaking lemma : " @@ -243,36 +233,86 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, } } } - if (addedUnifEnumSymBreakLemma) - { - Trace("cegis-unif") << "..added unif enum symmetry breaking " - "lemma\n---CegisUnif Engine---\n"; - return false; - } + return !addedUnifEnumSymBreakLemma; +} + +void CegisUnif::setConditions( + const std::map>& unif_cenums, + const std::map>& unif_cvalues, + std::vector& lems) +{ + Node cost_lit = d_u_enum_manager.getAssertedLiteral(); + NodeManager* nm = NodeManager::currentNM(); // set the conditions for (const Node& c : d_unif_candidates) { for (const Node& e : d_cand_to_strat_pt[c]) { - d_sygus_unif.setConditions( - e, cost_lit, unif_enums[1][e], unif_values[1][e]); - // if condition enumerator had value, exclude this value - if (options::sygusUnifCondIndependent() && !unif_enums[1][e].empty()) + Assert(unif_cenums.find(e) != unif_cenums.end()); + Assert(unif_cvalues.find(e) != unif_cvalues.end()); + std::map>::const_iterator itc = + unif_cenums.find(e); + std::map>::const_iterator itv = + unif_cvalues.find(e); + d_sygus_unif.setConditions(e, cost_lit, itc->second, itv->second); + // d_sygus_unif.setConditions(e, cost_lit, unif_cenums[e], + // unif_cvalues[e]); if condition enumerator had value and it is being + // passively generated, exclude this value + if (options::sygusUnifCondIndependent() && !itc->second.empty()) { - Node eu = unif_enums[1][e][0]; + Node eu = itc->second[0]; Assert(d_tds->isEnumerator(eu)); + Assert(!itv->second.empty()); if (d_tds->isPassiveEnumerator(eu)) { Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu); - Node exp_exc = - d_tds->getExplain() - ->getExplanationForEquality(eu, unif_values[1][e][0]) - .negate(); + Node exp_exc = d_tds->getExplain() + ->getExplanationForEquality(eu, itv->second[0]) + .negate(); lems.push_back(nm->mkNode(OR, g.negate(), exp_exc)); } } } } +} + +bool CegisUnif::processConstructCandidates(const std::vector& enums, + const std::vector& enum_values, + const std::vector& candidates, + std::vector& candidate_values, + bool satisfiedRl, + std::vector& lems) +{ + if (d_unif_candidates.empty()) + { + Assert(d_non_unif_candidates.size() == candidates.size()); + return Cegis::processConstructCandidates( + enums, enum_values, candidates, candidate_values, satisfiedRl, lems); + } + // the unification enumerators for conditions and their model values + std::map> unif_cenums; + std::map> unif_cvalues; + // we only proceed to solution building if we are not introducing symmetry + // breaking lemmas between return values and if we have not previously + // introduced return values refinement lemmas + if (!getEnumValues(enums, enum_values, unif_cenums, unif_cvalues, lems) + || !satisfiedRl) + { + // if condition values are being indepedently enumerated, they should be + // communicated to the decision tree strategies indepedently of we + // proceeding to attempt solution building + if (options::sygusUnifCondIndependent()) + { + setConditions(unif_cenums, unif_cvalues, lems); + } + Trace("cegis-unif") << (!satisfiedRl + ? "..added refinement lemmas" + : "..added unif enum symmetry breaking") + << "\n---CegisUnif Engine---\n"; + // if we didn't satisfy the specification, there is no way to repair + return false; + } + setConditions(unif_cenums, unif_cvalues, lems); // build solutions (for unif candidates a divide-and-conquer approach is used) std::vector sols; std::vector lemmas; @@ -501,9 +541,8 @@ void CegisUnifEnumDecisionStrategy::initialize( } } -void CegisUnifEnumDecisionStrategy::getEnumeratorsForStrategyPt(Node e, - std::vector& es, - unsigned index) const +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 = 0; @@ -533,8 +572,8 @@ Node CegisUnifEnumDecisionStrategy::getActiveGuardForEnumerator(Node e) } void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, - StrategyPtInfo& si, - unsigned index) + StrategyPtInfo& si, + unsigned index) { NodeManager* nm = NodeManager::currentNM(); // instantiate template for removing redundant operators @@ -567,7 +606,8 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e, e, si.d_pt, d_parent, options::sygusUnifCondIndependent() && index == 1); } -void CegisUnifEnumDecisionStrategy::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); @@ -587,11 +627,10 @@ void CegisUnifEnumDecisionStrategy::registerEvalPts(const std::vector& eis } } - void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e, - Node ei, - Node guq_lit, - unsigned n) + Node ei, + Node guq_lit, + unsigned n) { // must be equal to one of the first n enums std::map::iterator itc = d_ce_info.find(e); diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 00cc5af72..c32a1390c 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -90,6 +90,7 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf void registerEvalPts(const std::vector& eis, Node e); /** Retrieves active guard for enumerator */ Node getActiveGuardForEnumerator(Node e); + private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; @@ -223,7 +224,7 @@ class CegisUnif : public Cegis * example would actually correspond to * eval(d, 0) != c1 v eval(d, c1) != c2 v eval(d, c2) > 1 * in which d is the deep embedding of the function-to-synthesize f - */ + */ void registerRefinementLemma(const std::vector& vars, Node lem, std::vector& lems) override; @@ -261,6 +262,35 @@ class CegisUnif : public Cegis std::vector& candidate_values, bool satisfiedRl, std::vector& lems) override; + /** communicate condition values to solution building utility + * + * for each unification candidate and for each strategy point associated with + * it, set in d_sygus_unif the condition values (unif_cvalues) for respective + * condition enumerators (unif_cenums) + */ + void setConditions(const std::map>& unif_cenums, + const std::map>& unif_cvalues, + std::vector& lems); + /** set values of condition enumerators based on current enumerator assignment + * + * enums and enum_values are the enumerators registered in getTermList and + * their values retrieved by the parent SynthConjecture module, respectively. + * + * unif_cenums and unif_cvalues associate the conditional enumerators of each + * strategy point of each unification candidate with their respective model + * values + * + * This function also generates inter-enumerator symmetry breaking for return + * values, such that their model values are ordered by size + * + * returns true if no symmetry breaking lemmas were generated for the return + * value enumerators, false otherwise + */ + bool getEnumValues(const std::vector& enums, + const std::vector& enum_values, + std::map>& unif_cenums, + std::map>& unif_cvalues, + std::vector& lems); /** * Sygus unif utility. This class implements the core algorithm (e.g. decision * tree learning) that this module relies upon. -- 2.30.2