From: Andrew Reynolds Date: Wed, 16 May 2018 23:22:35 +0000 (-0500) Subject: Improve the separation resolution scheme in cegis unif (#1931) X-Git-Tag: cvc5-1.0.0~5045 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=13e248f4087347721c731c1f21a6f8b66dc52ed1;p=cvc5.git Improve the separation resolution scheme in cegis unif (#1931) --- diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index ac70a97b2..ab9834254 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -127,6 +127,7 @@ bool CegisUnif::constructCandidates(const std::vector& enums, // values NodeManager* nm = NodeManager::currentNM(); bool addedUnifEnumSymBreakLemma = false; + Node cost_lit = d_u_enum_manager.getCurrentLiteral(); std::map> unif_enums[2]; std::map> unif_values[2]; for (const Node& c : candidates) @@ -157,40 +158,47 @@ bool CegisUnif::constructCandidates(const std::vector& enums, } 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++) + if (index == 0) { - 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) + // 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. + // 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++) { - // 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 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) { - 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; + // 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; + } } } } @@ -206,12 +214,14 @@ bool CegisUnif::constructCandidates(const std::vector& enums, { for (const Node& e : d_cand_to_strat_pt[c]) { - d_sygus_unif.setConditions(e, unif_values[1][e]); + d_sygus_unif.setConditions( + e, cost_lit, unif_enums[1][e], unif_values[1][e]); } } // build solutions (for unif candidates a divide-and-conquer approach is used) std::vector sols; - if (d_sygus_unif.constructSolution(sols)) + std::vector lemmas; + if (d_sygus_unif.constructSolution(sols, lemmas)) { candidate_values.insert(candidate_values.end(), sols.begin(), sols.end()); if (Trace.isOn("cegis-unif")) @@ -226,51 +236,13 @@ bool CegisUnif::constructCandidates(const std::vector& enums, } return true; } - std::map> sepPairs; - if (d_sygus_unif.getSeparationPairs(sepPairs)) + + Assert(!lemmas.empty()); + for (const Node& lem : lemmas) { - // 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 - 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 - 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++) - { - cond_eqs.push_back(itue->second[i].eqNode(ituv->second[i])); - } - 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); - } - } + Trace("cegis-unif") << "CegisUnif::lemma, separation lemma : " << lem + << "\n"; + d_qe->getOutputChannel().lemma(lem); } return false; } @@ -478,7 +450,7 @@ void CegisUnifEnumManager::incrementNumEnumerators() d_qe->getOutputChannel().lemma(sym_break_red_ops); } // symmetry breaking between enumerators - if (!ci.second.d_enums[index].empty()) + if (!ci.second.d_enums[index].empty() && index == 0) { Node e_prev = ci.second.d_enums[index].back(); Node size_e = nm->mkNode(DT_SIZE, e); diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 0afd7a82c..cd011ef44 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -441,7 +441,7 @@ bool CegConjecturePbe::constructCandidates(const std::vector& enums, Node c = candidates[i]; //build decision tree for candidate std::vector sol; - if (d_sygus_unif[c].constructSolution(sol)) + if (d_sygus_unif[c].constructSolution(sol, lems)) { Assert(sol.size() == 1); candidate_values.push_back(sol[0]); diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 15606c9a4..76ca94e05 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -42,7 +42,8 @@ void SygusUnif::initializeCandidate( d_strategy[f].initialize(qe, f, enums); } -bool SygusUnif::constructSolution(std::vector& sols) +bool SygusUnif::constructSolution(std::vector& sols, + std::vector& lemmas) { // initialize a call to construct solution initializeConstructSol(); @@ -52,7 +53,7 @@ bool SygusUnif::constructSolution(std::vector& sols) initializeConstructSolFor(f); // call the virtual construct solution method Node e = d_strategy[f].getRootEnumerator(); - Node sol = constructSol(f, e, role_equal, 1); + Node sol = constructSol(f, e, role_equal, 1, lemmas); if (sol.isNull()) { return false; diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 1c7972978..a19f8e41b 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -80,8 +80,12 @@ class SygusUnif * based on the current set of enumerated values. Returns null if it cannot * for some function (for example, if the set of enumerated values is * insufficient, or if a non-deterministic strategy aborts). + * + * This call may add lemmas to lemmas that should be sent out on an output + * channel by the caller. */ - virtual bool constructSolution(std::vector& sols); + virtual bool constructSolution(std::vector& sols, + std::vector& lemmas); protected: /** reference to quantifier engine */ @@ -150,7 +154,8 @@ class SygusUnif * * ind is the term depth of the context (for debugging). */ - virtual Node constructSol(Node f, Node e, NodeRole nrole, int ind) = 0; + virtual Node constructSol( + Node f, Node e, NodeRole nrole, int ind, std::vector& lemmas) = 0; /** Heuristically choose the best solved term from solved in context x, * currently return the first. */ virtual Node constructBestSolvedTerm(const std::vector& solved); diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 1b43b77ba..f9c597118 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -680,9 +680,10 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) lemmas.push_back(exp_exc); } -bool SygusUnifIo::constructSolution(std::vector& sols) +bool SygusUnifIo::constructSolution(std::vector& sols, + std::vector& lemmas) { - Node sol = constructSolutionNode(); + Node sol = constructSolutionNode(lemmas); if (!sol.isNull()) { sols.push_back(sol); @@ -691,7 +692,7 @@ bool SygusUnifIo::constructSolution(std::vector& sols) return false; } -Node SygusUnifIo::constructSolutionNode() +Node SygusUnifIo::constructSolutionNode(std::vector& lemmas) { Node c = d_candidate; if (!d_solution.isNull()) @@ -716,7 +717,7 @@ Node SygusUnifIo::constructSolutionNode() initializeConstructSolFor(c); // call the virtual construct solution method Node e = d_strategy[c].getRootEnumerator(); - Node vcc = constructSol(c, e, role_equal, 1); + Node vcc = constructSol(c, e, role_equal, 1, lemmas); // if we constructed the solution, and we either did not previously have // a solution, or the new solution is better (smaller). if (!vcc.isNull() @@ -854,7 +855,8 @@ void SygusUnifIo::initializeConstructSolFor(Node f) Assert(d_candidate == f); } -Node SygusUnifIo::constructSol(Node f, Node e, NodeRole nrole, int ind) +Node SygusUnifIo::constructSol( + Node f, Node e, NodeRole nrole, int ind, std::vector& lemmas) { Assert(d_candidate == f); UnifContextIo& x = d_context; @@ -1285,7 +1287,7 @@ Node SygusUnifIo::constructSol(Node f, Node e, NodeRole nrole, int ind) } else { - rec_c = constructSol(f, cenum.first, cenum.second, ind + 2); + rec_c = constructSol(f, cenum.first, cenum.second, ind + 2, lemmas); } // undo update the context diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 9a6c02421..a8e7fc011 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -285,7 +285,8 @@ class SygusUnifIo : public SygusUnif void notifyEnumeration(Node e, Node v, std::vector& lemmas) override; /** Construct solution */ - bool constructSolution(std::vector& sols) override; + bool constructSolution(std::vector& sols, + std::vector& lemmas) override; /** add example * @@ -377,7 +378,7 @@ class SygusUnifIo : public SygusUnif * constructSolution. If this returns a non-null node, then that term is a * solution for the function-to-synthesize in the overall conjecture. */ - Node constructSolutionNode(); + Node constructSolutionNode(std::vector& lemmas); /** domain-specific enumerator exclusion techniques * * Returns true if the value v for e can be excluded based on a @@ -414,7 +415,11 @@ class SygusUnifIo : public SygusUnif /** initialize construct solution for */ void initializeConstructSolFor(Node f) override; /** construct solution */ - Node constructSol(Node f, Node e, NodeRole nrole, int ind) override; + Node constructSol(Node f, + Node e, + NodeRole nrole, + int ind, + std::vector& lemmas) override; }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index f7337a92d..3fbb4b2b7 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -14,6 +14,8 @@ #include "theory/quantifiers/sygus/sygus_unif_rl.h" +#include "options/base_options.h" +#include "printer/printer.h" #include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" @@ -276,9 +278,10 @@ Node SygusUnifRl::addRefLemma(Node lemma, return plem; } -void SygusUnifRl::initializeConstructSol() { d_sepPairs.clear(); } +void SygusUnifRl::initializeConstructSol() {} void SygusUnifRl::initializeConstructSolFor(Node f) {} -bool SygusUnifRl::constructSolution(std::vector& sols) +bool SygusUnifRl::constructSolution(std::vector& sols, + std::vector& lemmas) { initializeConstructSol(); bool successful = true; @@ -291,7 +294,8 @@ bool SygusUnifRl::constructSolution(std::vector& sols) continue; } initializeConstructSolFor(c); - Node v = constructSol(c, d_strategy[c].getRootEnumerator(), role_equal, 0); + Node v = constructSol( + c, d_strategy[c].getRootEnumerator(), role_equal, 0, lemmas); if (v.isNull()) { // we continue trying to build solutions to accumulate potentitial @@ -305,7 +309,8 @@ bool SygusUnifRl::constructSolution(std::vector& sols) return successful; } -Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind) +Node SygusUnifRl::constructSol( + Node f, Node e, NodeRole nrole, int ind, std::vector& lemmas) { indent("sygus-unif-sol", ind); Trace("sygus-unif-sol") << "ConstructSol: SygusRL : " << e << std::endl; @@ -334,23 +339,14 @@ Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind) return d_parent->getModelValue(e); } EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()]; - std::vector toSeparate; - Node sol = itd->second.buildSol(etis->d_cons, toSeparate); + Node sol = itd->second.buildSol(etis->d_cons, lemmas); if (sol.isNull()) { - Assert(!toSeparate.empty()); - d_sepPairs[e] = toSeparate; + Assert(!lemmas.empty()); } return sol; } -bool SygusUnifRl::getSeparationPairs( - std::map>& sepPairs) -{ - sepPairs = d_sepPairs; - return !sepPairs.empty(); -} - bool SygusUnifRl::usingUnif(Node f) const { return d_unif_candidates.find(f) != d_unif_candidates.end(); @@ -363,12 +359,15 @@ Node SygusUnifRl::getConditionForEvaluationPoint(Node e) const return it->second.getConditionEnumerator(); } -void SygusUnifRl::setConditions(Node e, const std::vector& conds) +void SygusUnifRl::setConditions(Node e, + Node guard, + const std::vector& enums, + const std::vector& conds) { std::map::iterator it = d_stratpt_to_dt.find(e); Assert(it != d_stratpt_to_dt.end()); - // Clear previous trie - it->second.resetPointSeparator(conds); + // set the conditions for the appropriate tree + it->second.setConditions(guard, enums, conds); } std::vector SygusUnifRl::getEvalPointHeads(Node c) @@ -487,27 +486,20 @@ void SygusUnifRl::DecisionTreeInfo::initialize(Node cond_enum, d_pt_sep.initialize(this); } -void SygusUnifRl::DecisionTreeInfo::resetPointSeparator( - const std::vector& conds) +void SygusUnifRl::DecisionTreeInfo::setConditions( + Node guard, const std::vector& enums, const std::vector& conds) { - // clear old condition values and trie + Assert(enums.size() == conds.size()); + // set the guard + d_guard = guard; + // clear old condition values + d_enums.clear(); d_conds.clear(); - d_pt_sep.d_trie.clear(); // set new condition values + d_enums.insert(d_enums.end(), enums.begin(), enums.end()); d_conds.insert(d_conds.end(), conds.begin(), conds.end()); } -void SygusUnifRl::DecisionTreeInfo::addPoint(Node f) -{ - d_pt_sep.d_trie.add(f, &d_pt_sep, d_conds.size()); -} - -void SygusUnifRl::DecisionTreeInfo::addCondValue(Node condv) -{ - d_conds.push_back(condv); - d_pt_sep.d_trie.addClassifier(&d_pt_sep, d_conds.size() - 1); -} - unsigned SygusUnifRl::DecisionTreeInfo::getStrategyIndex() const { return d_strategy_index; @@ -516,21 +508,234 @@ unsigned SygusUnifRl::DecisionTreeInfo::getStrategyIndex() const using UNodePair = std::pair; Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, - std::vector& toSeparate) + std::vector& lemmas) { if (!d_template.first.isNull()) { Trace("sygus-unif-sol") << "...templated conditions unsupported\n"; return Node::null(); } - if (!isSeparated(toSeparate)) + Trace("sygus-unif-sol") << "Decision::buildSol with " << d_hds.size() + << " evaluation heads and " << d_conds.size() + << " conditions..." << std::endl; + NodeManager* nm = NodeManager::currentNM(); + // model values for evaluation heads + std::map hd_mv; + // reset the trie + d_pt_sep.d_trie.clear(); + // the current explanation of why there has not yet been a separation conflict + std::vector exp; + // is the above explanation ready to be sent out as a lemma? + bool exp_conflict = false; + // the index of the head we are considering + unsigned hd_counter = 0; + // the index of the condition we are considering + unsigned c_counter = 0; + // do we need to resolve a separation conflict? + bool needs_sep_resolve = false; + // This loop simultaneously builds the solution in terms of a lazy trie + // (LazyTrieMulti), and checks whether a separation conflict exists. We + // enforce that the separation conflicts we encounter while building + // this solution are resolved, in order, by the condition enumerators. + // If not, then we add a (conflict) lemma stating that the current model + // value of the condition enumerator must be different. We also call this + // a "separation lemma". + // + // As a simple example, say we have: + // evalution heads: (eval e1 0 0), (eval e2 1 2) + // conditions: c1 + // where M(e1) = x, M(e2) = y, and M(c1) = x>1. After adding e1 and e2, we are + // in conflict since { e1, e2 } form a separation class, M(e1)!=M(e2), and + // M(c1) does not separate e1 and e2 since: + // (x>1){x->0,y->0} = (x>1){x->1,y->2} = false + // Hence, we would fail to build a solution in this case, and instead send a + // separation lemma of the form: + // ~( e1 != e2 ^ c1 = [x<1] ) + // + // Say we have: + // evalution heads: (eval e1 0 0), (eval e2 1 2), (eval e3 1 3) + // conditions: c1 c2 + // where M(e1) = x, M(e2) = y, M(e3) = x+1, M(c1) = x>0 and M(c2) = x<0. + // After adding e1 and e2, { e1, e2 } form a separation class, M(e1)!=M(e2), + // but M(c1) separates e1 and e2 since + // (x>0){x->0,y->0} = false, and + // (x>1){x->1,y->2} = true + // Hence, we get new separation classes { e1 } and { e2 }, and afterwards + // add e3. We then get { e2, e3 } as a separation class, which is also a + // conflict since M(e2)!=M(e3). We check if M(c2) resolves this conflict. + // It does not, since (x<1){x->0,y->0} = (x<1){x->1,y->2} = false. Hence, + // we get a separation lemma: + // ~( c1 = [x>1] ^ e2 != e3 ^ c2 = [x<1] ) + // + // Say we have: + // evalution heads: (eval e1 0 0), (eval e2 1 2), (eval e3 1 3) + // conditions: c1 + // where M(e1) = x, M(e2) = x, M(e3) = y, M(c1) = x>0. + // After adding e1 and e2, we have separation class { e1, e2 }. This is not a + // conflict since M(e1)=M(e2). We then add e3, obtaining separation class + // { e1, e2, e3 }, which is in conflict since M(e3)!=M(e1), and the condition + // c1 does not separate e3 and the representative of this class, e1. Hence we + // get a separation lemma of the form: + // ~( e1 = e2 ^ e1 != e3 ^ c1 = [x>0] ) + // + // It also may be the case that we exhaust the pool of condition enumerators. + // Say we have: + // evalution heads: (eval e1 0 0), (eval e2 1 2), (eval e3 1 3) + // conditions: c1 + // where M(e1) = x, M(e2) = x, M(e3) = y, M(c1) = y>0. After adding e1, e2, + // and e3, we have a separation class { e1, e2, e3 } that is in conflict + // since M(e3)!=M(e1). We add the condition c1, which separates into new + // equivalence classes { e1 }, { e2, e3 }. We are still in separation conflict + // since M(e3)!=M(e2). However, we do not have any further conditions to use + // to resolve this conflict. Thus, we add the separation lemma: + // ~( e1 = e2 ^ e1 != e3 ^ e2 != e3 ^ c1 = [y>0] ^ G_1 ) + // where G_1 is a guard stating that we use at most 1 condition. + Node e; + Node er; + while (hd_counter < d_hds.size() || needs_sep_resolve) + { + if (!needs_sep_resolve) + { + // add the head to the trie + e = d_hds[hd_counter]; + hd_mv[e] = d_unif->d_parent->getModelValue(e); + if (Trace.isOn("sygus-unif-sol")) + { + std::stringstream ss; + Printer::getPrinter(options::outputLanguage()) + ->toStreamSygus(ss, hd_mv[e]); + Trace("sygus-unif-sol") + << " add evaluation head (" << hd_counter << "/" << d_hds.size() + << "): " << e << " -> " << ss.str() << std::endl; + } + hd_counter++; + // get the representative of the trie + er = d_pt_sep.d_trie.add(e, &d_pt_sep, c_counter); + Trace("sygus-unif-sol") << " ...separation class " << er << std::endl; + // are we in conflict? + if (er == e) + { + // new separation class, no conflict + continue; + } + Assert(hd_mv.find(er) != hd_mv.end()); + if (hd_mv[er] == hd_mv[e]) + { + // merged into separation class with same model value, no conflict + // add to explanation + // this states that it mattered that (er = e) at the time that e was + // added to the trie. Notice that er and e may become separated later, + // but to ensure the overall invariant, this equality must persist in + // the explanation. + exp.push_back(er.eqNode(e)); + Trace("sygus-unif-sol") << " ...equal model values " << std::endl; + Trace("sygus-unif-sol") + << " ...add to explanation " << er.eqNode(e) << std::endl; + continue; + } + } + // must include in the explanation that we hit a conflict at this point in + // the construction + exp.push_back(e.eqNode(er).negate()); + // we are in separation conflict, does the next condition resolve this? + // check whether we have have exhausted our condition pool. If so, we + // are in conflict and this conflict depends on the guard. + if (c_counter >= d_conds.size()) + { + // truncated separation lemma + Assert(!d_guard.isNull()); + exp.push_back(d_guard); + exp_conflict = true; + break; + } + Assert(c_counter < d_conds.size()); + Node ce = d_enums[c_counter]; + Node cv = d_conds[c_counter]; + Assert(ce.getType() == cv.getType()); + if (Trace.isOn("sygus-unif-sol")) + { + std::stringstream ss; + Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, cv); + Trace("sygus-unif-sol") + << " add condition (" << c_counter << "/" << d_conds.size() + << "): " << ce << " -> " << ss.str() << std::endl; + } + // cache the separation class + std::vector prev_sep_c = d_pt_sep.d_trie.d_rep_to_class[er]; + // add new classifier + d_pt_sep.d_trie.addClassifier(&d_pt_sep, c_counter); + c_counter++; + // add to explanation + // c_exp is a conjunction of testers applied to shared selector chains + Node c_exp = d_unif->d_tds->getExplain()->getExplanationForEquality(ce, cv); + exp.push_back(c_exp); + std::map>::iterator itr = + d_pt_sep.d_trie.d_rep_to_class.find(e); + // since e is last in its separation class, if it becomes a representative, + // then it is separated from all values in prev_sep_c + if (itr != d_pt_sep.d_trie.d_rep_to_class.end()) + { + Trace("sygus-unif-sol") + << " ...resolves separation conflict with all" << std::endl; + needs_sep_resolve = false; + continue; + } + itr = d_pt_sep.d_trie.d_rep_to_class.find(er); + // since er is first in its separation class, it remains a representative + Assert(itr != d_pt_sep.d_trie.d_rep_to_class.end()); + // is e still in the separation class of er? + if (std::find(itr->second.begin(), itr->second.end(), e) + != itr->second.end()) + { + Trace("sygus-unif-sol") + << " ...does not resolve separation conflict with current" + << std::endl; + // the condition does not separate e and er + // this violates the invariant that the i^th conditional enumerator + // resolves the i^th separation conflict + exp_conflict = true; + break; + } + Trace("sygus-unif-sol") + << " ...resolves separation conflict with current, but not all" + << std::endl; + // find the new term to resolve a separation + Node new_er = Node::null(); + // scan the previous list and find the representative of the class that e is + // now in + for (unsigned i = 0, size = prev_sep_c.size(); i < size; i++) + { + Node check_er = prev_sep_c[i]; + if (check_er != er && check_er != e) + { + itr = d_pt_sep.d_trie.d_rep_to_class.find(check_er); + if (itr != d_pt_sep.d_trie.d_rep_to_class.end()) + { + if (std::find(itr->second.begin(), itr->second.end(), e) + != itr->second.end()) + { + new_er = check_er; + break; + } + } + } + } + // should find exactly one + Assert(!new_er.isNull()); + er = new_er; + needs_sep_resolve = true; + } + if (exp_conflict) { - Trace("sygus-unif-sol") << "...separation check failed\n"; + Node lemma = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp); + lemma = lemma.negate(); + Trace("sygus-unif-sol") << " ......conflict is " << lemma << std::endl; + lemmas.push_back(lemma); return Node::null(); } + Trace("sygus-unif-sol") << "...ready to build solution from DT\n"; // Traverse trie and build ITE with cons - NodeManager* nm = NodeManager::currentNM(); std::map cache; std::map::iterator it; std::vector visit; @@ -551,8 +756,8 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, // leaf if (trie->d_children.empty()) { - Assert(d_hd_values.find(trie->d_lazy_child) != d_hd_values.end()); - cache[cur] = d_hd_values[trie->d_lazy_child]; + Assert(hd_mv.find(trie->d_lazy_child) != hd_mv.end()); + cache[cur] = hd_mv[trie->d_lazy_child]; Trace("sygus-unif-sol-debug") << "......leaf, build " << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType()) @@ -607,70 +812,6 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, return cache[root]; } -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) - { - Assert(!rep_to_class.second.empty()); - Node v = d_unif->d_parent->getModelValue(rep_to_class.second[0]); - if (Trace.isOn("sygus-unif-rl-dt-debug")) - { - Trace("sygus-unif-rl-dt-debug") << "...class of (" - << rep_to_class.second[0]; - Assert(d_unif->d_hd_to_pt.find(rep_to_class.second[0]) - != d_unif->d_hd_to_pt.end()); - for (const Node& pti : d_unif->d_hd_to_pt[rep_to_class.second[0]]) - { - Trace("sygus-unif-rl-dt-debug") << " " << pti << " "; - } - Trace("sygus-unif-rl-dt-debug") << ") " - << " with hd value " << v << "\n"; - } - d_hd_values[rep_to_class.second[0]] = v; - unsigned i, size = rep_to_class.second.size(); - for (i = 1; i < size; ++i) - { - Node vi = d_unif->d_parent->getModelValue(rep_to_class.second[i]); - Assert(d_hd_values.find(rep_to_class.second[i]) == d_hd_values.end()); - d_hd_values[rep_to_class.second[i]] = vi; - if (Trace.isOn("sygus-unif-rl-dt-debug")) - { - Trace("sygus-unif-rl-dt-debug") << "...class of (" - << rep_to_class.second[i]; - Assert(d_unif->d_hd_to_pt.find(rep_to_class.second[i]) - != d_unif->d_hd_to_pt.end()); - for (const Node& pti : d_unif->d_hd_to_pt[rep_to_class.second[i]]) - { - Trace("sygus-unif-rl-dt-debug") << " " << pti << " "; - } - Trace("sygus-unif-rl-dt-debug") << ") " - << " with hd value " << vi << "\n"; - } - // Heads with different model values - if (v != vi) - { - Trace("sygus-unif-rl-dt") << "...in sep class heads with diff values: " - << rep_to_class.second[0] << " and " - << rep_to_class.second[i] << "\n"; - 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 toSeparate.empty(); -} - void SygusUnifRl::DecisionTreeInfo::PointSeparator::initialize( DecisionTreeInfo* dt) { diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 5bd6cdc1e..8a5230d15 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -59,7 +59,8 @@ class SygusUnifRl : public SygusUnif /** Notify enumeration (unused) */ void notifyEnumeration(Node e, Node v, std::vector& lemmas) override; /** Construct solution */ - bool constructSolution(std::vector& sols) override; + bool constructSolution(std::vector& sols, + std::vector& lemmas) override; /** add refinement lemma * * This adds a lemma to the specification. It returns the purified form @@ -90,29 +91,29 @@ class SygusUnifRl : public SygusUnif /** set conditional enumerators * * This informs this class that the current set of conditions for evaluation - * point e is conds. + * point e are enumerated by "enums" and have values "conds"; "guard" is + * Boolean variable whose semantics correspond to "there is a solution using + * at most enums.size() conditions." */ - void setConditions(Node e, const std::vector& conds); + void setConditions(Node e, + Node guard, + const std::vector& enums, + const std::vector& conds); /** 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; /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */ std::unordered_set d_unif_candidates; /** construct sol */ - Node constructSol(Node f, Node e, NodeRole nrole, int ind) override; + Node constructSol(Node f, + Node e, + NodeRole nrole, + int ind, + std::vector& lemmas) override; /** collects data from refinement lemmas to drive solution construction * * In particular it rebuilds d_app_to_pt whenever d_prev_rlemmas is different @@ -123,12 +124,6 @@ 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 @@ -211,32 +206,39 @@ 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 + * separated indeed are separated by the current set of conditions. * - * 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. + * This method either returns a solution (if all points are separated). + * It it fails, it adds a conflict lemma to lemmas. */ - bool isSeparated(std::vector& toSeparate); + Node buildSol(Node cons, std::vector& lemmas); /** 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 */ + /** enumerated condition values, this is set by setConditions(...). */ 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); + /** set conditions */ + void setConditions(Node guard, + const std::vector& enums, + const std::vector& conds); private: + /** + * Conditional enumerator variables corresponding to the condition values in + * d_conds. These are used for generating separation lemmas during + * buildSol. This is set by setConditions(...). + */ + std::vector d_enums; + /** + * The guard literal whose semantics is "we need at most d_enums.size() + * conditions in our solution. This is set by setConditions(...). + */ + Node d_guard; /** * reference to inferred strategy for the function-to-synthesize this DT is * associated with @@ -254,8 +256,6 @@ class SygusUnifRl : public SygusUnif * decision tree. */ Node d_cond_enum; - /** chache of model values of heads of evaluation points */ - NodePairMap d_hd_values; /** Classifies evaluation points according to enumerated condition values * * Maintains the invariant that points evaluated in the same way in the @@ -284,10 +284,6 @@ 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;