From 016c3e69a7bf5f89ca4625b41db8571a6849fb68 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 15 May 2018 15:39:27 -0500 Subject: [PATCH] Refactoring get enumerator values in construct candidate for cegis unif (#1926) --- src/theory/quantifiers/sygus/cegis_unif.cpp | 154 ++++++++++++------ src/theory/quantifiers/sygus/cegis_unif.h | 10 +- .../quantifiers/sygus/term_database_sygus.cpp | 2 +- 3 files changed, 112 insertions(+), 54 deletions(-) diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 8db60d373..ac70a97b2 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -97,20 +97,6 @@ void CegisUnif::getTermList(const std::vector& candidates, << hd << "\n"; enums.push_back(hd); } - // for each decision tree strategy allocated for c (these are referenced - // by strategy points in d_cand_to_strat_pt[c]) - for (const Node& e : d_cand_to_strat_pt[c]) - { - std::vector cenums; - // also get the current conditional enumerators - d_u_enum_manager.getCondEnumeratorsForStrategyPt(e, cenums); - for (const Node& ce : cenums) - { - d_cenum_to_strat_pt[ce] = e; - } - // conditional enumerators are also part of list - enums.insert(enums.end(), cenums.begin(), cenums.end()); - } } } @@ -120,49 +106,109 @@ bool CegisUnif::constructCandidates(const std::vector& enums, std::vector& candidate_values, std::vector& lems) { - // 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) + if (Trace.isOn("cegis-unif-enum")) { - // Non-unif enums (which are the very candidates) should not be notified - if (enums[i] == candidates[i] && !d_sygus_unif.usingUnif(enums[i])) + Trace("cegis-unif-enum") << " Evaluation heads :\n"; + for (unsigned i = 0, size = enums.size(); i < size; ++i) { - Trace("cegis-unif-enum") << " Ignoring non-unif candidate " << enums[i] - << std::endl; - continue; - } - if (Trace.isOn("cegis-unif-enum")) - { - Trace("cegis-unif-enum") << " " << enums[i] << " -> "; + Trace("cegis-unif-enum") << " " << enums[i] << " -> "; std::stringstream ss; Printer::getPrinter(options::outputLanguage()) ->toStreamSygus(ss, enum_values[i]); Trace("cegis-unif-enum") << ss.str() << std::endl; } - Node e = enums[i], v = enum_values[i]; - 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); - } } // evaluate on refinement lemmas if (addEvalLemmas(enums, enum_values)) { return false; } - // inform the unif utility that we are using these conditions - for (const std::pair> cs : condition_map) + // the unification enumerators (return values, conditions) and their model + // values + NodeManager* nm = NodeManager::currentNM(); + bool addedUnifEnumSymBreakLemma = false; + std::map> unif_enums[2]; + std::map> unif_values[2]; + for (const Node& c : candidates) + { + // for each decision tree strategy allocated for c (these are referenced + // by strategy points in d_cand_to_strat_pt[c]) + for (const Node& e : d_cand_to_strat_pt[c]) + { + for (unsigned index = 0; index < 2; index++) + { + Trace("cegis-unif-enum") + << " " << (index == 0 ? "Return values" : "Conditions") << " for " + << e << ":\n"; + // get the current unification enumerators + d_u_enum_manager.getEnumeratorsForStrategyPt( + e, unif_enums[index][e], index); + // get the model value of each enumerator + for (const Node& eu : unif_enums[index][e]) + { + Node m_eu = d_parent->getModelValue(eu); + if (Trace.isOn("cegis-unif-enum")) + { + Trace("cegis-unif-enum") << " " << eu << " -> "; + std::stringstream ss; + Printer::getPrinter(options::outputLanguage()) + ->toStreamSygus(ss, m_eu); + Trace("cegis-unif-enum") << ss.str() << std::endl; + } + unif_values[index][e].push_back(m_eu); + } + // inter-enumerator symmetry breaking + // given a pool of unification enumerators eu_1, ..., eu_n, + // CegisUnifEnumManager 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} ) ) + // when applicable. + for (unsigned j = 1, nenum = unif_values[index][e].size(); j < nenum; + j++) + { + Node prev_val = unif_values[index][e][j - 1]; + Node curr_val = unif_values[index][e][j]; + // compare the node values + if (curr_val < prev_val) + { + // must have the same size + unsigned prev_size = d_tds->getSygusTermSize(prev_val); + unsigned curr_size = d_tds->getSygusTermSize(curr_val); + 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(); + Trace("cegis-unif") << "CegisUnif::lemma, inter-unif-enumerator " + "symmetry breaking lemma : " + << slem << "\n"; + d_qe->getOutputChannel().lemma(slem); + addedUnifEnumSymBreakLemma = true; + break; + } + } + } + } + } + } + if (addedUnifEnumSymBreakLemma) + { + return false; + } + // set the conditions + for (const Node& c : candidates) { - d_sygus_unif.setConditions(cs.first, cs.second); + for (const Node& e : d_cand_to_strat_pt[c]) + { + d_sygus_unif.setConditions(e, unif_values[1][e]); + } } - // TODO : check symmetry breaking for enumerators // build solutions (for unif candidates a divide-and-conquer approach is used) std::vector sols; if (d_sygus_unif.constructSolution(sols)) @@ -186,18 +232,22 @@ bool CegisUnif::constructCandidates(const std::vector& enums, // 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) { + Node e = np.first; // 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) + std::vector cond_eqs; + std::map>::iterator itue = unif_enums[1].find(e); + Assert(itue != unif_enums[1].end()); + std::map>::iterator ituv = unif_values[1].find(e); + Assert(ituv != unif_values[1].end()); + Assert(itue->second.size() == ituv->second.size()); + for (unsigned i = 0, size = itue->second.size(); i < size; i++) { - Assert(cenum_to_value.find(ce) != cenum_to_value.end()); - cond_eqs.push_back(nm->mkNode(EQUAL, ce, cenum_to_value[ce])); + cond_eqs.push_back(itue->second[i].eqNode(ituv->second[i])); } Assert(!cond_eqs.empty()); Node neg_conds_lit = @@ -318,13 +368,15 @@ void CegisUnifEnumManager::initialize( incrementNumEnumerators(); } -void CegisUnifEnumManager::getCondEnumeratorsForStrategyPt( - Node e, std::vector& ces) const +void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e, + std::vector& es, + unsigned index) const { std::map::const_iterator itc = d_ce_info.find(e); Assert(itc != d_ce_info.end()); - ces.insert( - ces.end(), itc->second.d_enums[1].begin(), itc->second.d_enums[1].end()); + es.insert(es.end(), + itc->second.d_enums[index].begin(), + itc->second.d_enums[index].end()); } void CegisUnifEnumManager::registerEvalPts(const std::vector& eis, Node e) diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index ce096b127..735477821 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -59,8 +59,14 @@ class CegisUnifEnumManager void initialize(const std::vector& es, const std::map& e_to_cond, const std::map>& strategy_lemmas); - /** get the current set of conditional enumerators for strategy point e */ - void getCondEnumeratorsForStrategyPt(Node e, std::vector& ces) const; + /** get the current set of enumerators for strategy point e + * + * Index 0 adds the set of return value enumerators to es, index 1 adds the + * set of condition enumerators to es. + */ + void getEnumeratorsForStrategyPt(Node e, + std::vector& es, + unsigned index) const; /** register evaluation point for candidate * * This notifies this class that eis is a set of heads of evaluation points diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 774ba2180..3d88cbe5d 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -112,7 +112,7 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c) Assert( TypeNode::fromType( static_cast(tn.toType()).getDatatype().getSygusType()) - == c.getType()); + .isComparableTo(c.getType())); std::map::iterator it = d_proxy_vars[tn].find(c); if (it == d_proxy_vars[tn].end()) -- 2.30.2