From: Haniel Barbosa Date: Tue, 11 Sep 2018 01:51:03 +0000 (-0500) Subject: Using a single condition enumerator in sygus-unif (#2440) X-Git-Tag: cvc5-1.0.0~4665 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1a695dcbe3036ab0f1922c5655c082ec1f14db97;p=cvc5.git Using a single condition enumerator in sygus-unif (#2440) This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case). In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts: - _main advantage_: can quickly enumerate relevant condition values for solving the problem - _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie. A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif. There is also small improvements for trace messages. --- diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index c9d1aefa1..01cf41518 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -741,7 +741,7 @@ header = "options/quantifiers_options.h" read_only = true help = "optimization, skip instances based on possibly irrelevant portions of quantified formulas" -### Rewrite rules options +### Rewrite rules options [[option]] name = "quantRewriteRules" @@ -761,7 +761,7 @@ header = "options/quantifiers_options.h" read_only = true help = "add one instance of rewrite rule per round" -### Induction options +### Induction options [[option]] name = "quantInduction" @@ -975,6 +975,22 @@ header = "options/quantifiers_options.h" default = "false" help = "Unification-based function synthesis" +[[option]] + name = "sygusUnifCondIndependent" + category = "regular" + long = "sygus-unif-cond-independent" + type = "bool" + default = "false" + help = "Synthesize conditions indepedently from return values (may generate bigger solutions)" + +[[option]] + name = "sygusUnifCondIndNoRepeatSol" + category = "regular" + long = "sygus-unif-cond-indpendent-no-repeat-sol" + type = "bool" + default = "true" + help = "Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis" + [[option]] name = "sygusBoolIteReturnConst" category = "regular" @@ -1164,7 +1180,7 @@ header = "options/quantifiers_options.h" type = "bool" default = "true" help = "Minimize synthesis solutions" - + [[option]] name = "sygusEvalOpt" category = "regular" @@ -1180,7 +1196,7 @@ header = "options/quantifiers_options.h" type = "bool" default = "false" help = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant" - + # Internal uses of sygus [[option]] diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 7319ba73e..204daa49a 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -166,7 +166,17 @@ bool Cegis::constructCandidates(const std::vector& enums, Trace("cegis") << " Enumerators :\n"; for (unsigned i = 0, size = enums.size(); i < size; ++i) { - Trace("cegis") << " " << enums[i] << " -> "; + bool isUnit = false; + for (const Node& hd_unit : d_rl_eval_hds) + { + if (enums[i] == hd_unit[0]) + { + isUnit = true; + break; + } + } + Trace("cegis") << " " << enums[i] + << (options::sygusUnif() && isUnit ? "*" : "") << " -> "; std::stringstream ss; Printer::getPrinter(options::outputLanguage()) ->toStreamSygus(ss, enum_values[i]); diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 89a11eb0c..1245cba1f 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -68,8 +68,8 @@ bool CegisUnif::processInitialize(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; } } @@ -90,8 +90,8 @@ void CegisUnif::getTermList(const std::vector& candidates, // Collect heads of candidates for (const Node& hd : d_sygus_unif.getEvalPointHeads(c)) { - Trace("cegis-unif-enum-debug") << "......cand " << c << " with enum hd " - << hd << "\n"; + Trace("cegis-unif-enum-debug") + << "......cand " << c << " with enum hd " << hd << "\n"; enums.push_back(hd); } } @@ -112,12 +112,15 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, } 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; } // the unification enumerators (return values, conditions) and their model // values NodeManager* nm = NodeManager::currentNM(); + Valuation& valuation = d_qe->getValuation(); bool addedUnifEnumSymBreakLemma = false; Node cost_lit = d_u_enum_manager.getCurrentLiteral(); std::map> unif_enums[2]; @@ -135,6 +138,21 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, // get the current unification enumerators d_u_enum_manager.getEnumeratorsForStrategyPt( e, unif_enums[index][e], index); + if (index == 1 && options::sygusUnifCondIndependent()) + { + Assert(unif_enums[index][e].size() == 1); + Node eu = unif_enums[index][e][0]; + Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu); + // If active guard for this enumerator is not true, there are no more + // values for it, and hence we ignore it + Node gstatus = valuation.getSatValue(g); + if (gstatus.isNull() || !gstatus.getConst()) + { + Trace("cegis") << " " << eu << " -> N/A\n"; + unif_enums[index][e].clear(); + continue; + } + } // get the model value of each enumerator for (const Node& eu : unif_enums[index][e]) { @@ -149,9 +167,9 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, } unif_values[index][e].push_back(m_eu); } + // inter-enumerator symmetry breaking for return values if (index == 0) { - // 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 @@ -198,6 +216,8 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, } if (addedUnifEnumSymBreakLemma) { + Trace("cegis-unif") << "..added unif enum symmetry breaking " + "lemma\n---CegisUnif Engine---\n"; return false; } // set the conditions @@ -207,6 +227,16 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, { 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()) + { + Node eu = unif_enums[1][e][0]; + Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu); + Node exp_exc = d_tds->getExplain() + ->getExplanationForEquality(eu, unif_values[1][e][0]) + .negate(); + lems.push_back(nm->mkNode(OR, g.negate(), exp_exc)); + } } } // build solutions (for unif candidates a divide-and-conquer approach is used) @@ -228,13 +258,15 @@ bool CegisUnif::processConstructCandidates(const std::vector& enums, return true; } - Assert(!lemmas.empty()); + // TODO tie this to the lemma for getting a new condition value + Assert(options::sygusUnifCondIndependent() || !lemmas.empty()); for (const Node& lem : lemmas) { - Trace("cegis-unif") << "CegisUnif::lemma, separation lemma : " << lem - << "\n"; + Trace("cegis-unif-lemma") + << "CegisUnif::lemma, separation lemma : " << lem << "\n"; d_qe->getOutputChannel().lemma(lem); } + Trace("cegis-unif") << "..failed to separate heads\n---CegisUnif Engine---\n"; return false; } @@ -246,12 +278,13 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, std::map> eval_pts; Node plem = d_sygus_unif.addRefLemma(lem, eval_pts); addRefinementLemma(plem); - Trace("cegis-unif-lemma") << "* Refinement lemma:\n" << plem << "\n"; + Trace("cegis-unif-lemma") + << "CegisUnif::lemma, refinement lemma : " << plem << "\n"; // Notify the enumeration manager if there are new evaluation points for (const std::pair>& ep : eval_pts) { Assert(d_cand_to_strat_pt.find(ep.first) != d_cand_to_strat_pt.end()); - // Notify each startegy point of the respective candidate + // Notify each strategy point of the respective candidate for (const Node& n : d_cand_to_strat_pt[ep.first]) { d_u_enum_manager.registerEvalPts(ep.second, n); @@ -303,8 +336,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++) @@ -329,6 +362,17 @@ void CegisUnifEnumManager::initialize( } // initialize the current literal incrementNumEnumerators(); + // create single condition enumerator for each decision tree strategy + if (options::sygusUnifCondIndependent()) + { + // allocate a condition enumerator for each candidate + for (std::pair& ci : d_ce_info) + { + Node ceu = nm->mkSkolem("cu", ci.second.d_ce_type); + setUpEnumerator(ceu, ci.second, 1); + d_enum_to_active_guard[ceu] = d_tds->getActiveGuardForEnumerator(ceu); + } + } } void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e, @@ -340,8 +384,8 @@ void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e, Assert(num_enums > 0); if (index == 1) { - // we always use (cost-1) conditions - num_enums = num_enums - 1; + // we always use (cost-1) conditions, or 1 if in the indepedent case + num_enums = !options::sygusUnifCondIndependent() ? num_enums - 1 : 1; } if (num_enums > 0) { @@ -354,6 +398,46 @@ void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e, } } +Node CegisUnifEnumManager::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, + StrategyPtInfo& si, + unsigned index) +{ + NodeManager* nm = NodeManager::currentNM(); + // instantiate template for removing redundant operators + if (!si.d_sbt_lemma_tmpl[index].first.isNull()) + { + Node templ = si.d_sbt_lemma_tmpl[index].first; + TNode templ_var = si.d_sbt_lemma_tmpl[index].second; + Node sym_break_red_ops = templ.substitute(templ_var, e); + Trace("cegis-unif-enum-lemma") + << "CegisUnifEnum::lemma, remove redundant ops of " << e << " : " + << sym_break_red_ops << "\n"; + d_qe->getOutputChannel().lemma(sym_break_red_ops); + } + // symmetry breaking between enumerators + if (!si.d_enums[index].empty() && index == 0) + { + Node e_prev = si.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 + si.d_enums[index].push_back(e); + Trace("cegis-unif-enum") << "* Registering new enumerator " << e + << " to strategy point " << si.d_pt << "\n"; + d_tds->registerEnumerator(e, si.d_pt, d_parent); +} + void CegisUnifEnumManager::registerEvalPts(const std::vector& eis, Node e) { // candidates of the same type are managed @@ -427,7 +511,7 @@ void CegisUnifEnumManager::incrementNumEnumerators() TypeNode ct = c.getType(); Node eu = nm->mkSkolem("eu", ct); Node ceu; - if (!ci.second.d_enums[0].empty()) + if (!options::sygusUnifCondIndependent() && !ci.second.d_enums[0].empty()) { // make a new conditional enumerator as well, starting the // second type around @@ -441,38 +525,7 @@ void CegisUnifEnumManager::incrementNumEnumerators() { continue; } - // instantiate template for removing redundant operators - if (!ci.second.d_sbt_lemma_tmpl[index].first.isNull()) - { - Node templ = ci.second.d_sbt_lemma_tmpl[index].first; - TNode templ_var = ci.second.d_sbt_lemma_tmpl[index].second; - Node sym_break_red_ops = templ.substitute(templ_var, e); - Trace("cegis-unif-enum-lemma") - << "CegisUnifEnum::lemma, remove redundant ops of " << e << " : " - << sym_break_red_ops << "\n"; - d_qe->getOutputChannel().lemma(sym_break_red_ops); - } - // symmetry breaking between enumerators - 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); - 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); - // TODO symmetry breaking for making - // e distinct from ei : (ci.second.d_enums[index] \ {e}) - // if its respective type has had at least - // ci.second.d_enums[index].size() distinct values enumerated + setUpEnumerator(e, ci.second, index); } } // register the evaluation points at the new value @@ -568,8 +621,8 @@ void CegisUnifEnumManager::registerEvalPtAtSize(Node e, disj.push_back(ei.eqNode(itc->second.d_enums[0][i])); } Node lem = NodeManager::currentNM()->mkNode(OR, disj); - Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, domain:" << lem - << "\n"; + Trace("cegis-unif-enum-lemma") + << "CegisUnifEnum::lemma, domain:" << lem << "\n"; d_qe->getOutputChannel().lemma(lem); } diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 858a83bce..69d6ee25f 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -76,6 +76,8 @@ class CegisUnifEnumManager * registerEvalPtAtValue 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. @@ -105,6 +107,9 @@ class CegisUnifEnumManager bool d_initialized; /** null node */ Node d_null; + /** map from condition enumerators to active guards (in case they are + * enumerated indepedently of the return values) */ + std::map d_enum_to_active_guard; /** information per initialized type */ class StrategyPtInfo { @@ -165,6 +170,15 @@ class CegisUnifEnumManager * 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 + * information from the enumerator's respective strategy point and whether it + * is a condition or return value enumerator. For the latter we add symmetry + * breaking lemmas that force enumerators to consider values in an increasing + * order of size. + */ + void setUpEnumerator(Node e, StrategyPtInfo& si, unsigned index); /** increment the number of enumerators */ void incrementNumEnumerators(); /** get literal G_uq_n */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 183f40b66..51b14f3e1 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -345,10 +345,8 @@ Node SygusUnifRl::constructSol( } EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()]; Node sol = itd->second.buildSol(etis->d_cons, lemmas); - if (sol.isNull()) - { - Assert(!lemmas.empty()); - } + Assert(options::sygusUnifCondIndependent() || !sol.isNull() + || !lemmas.empty()); return sol; } @@ -512,6 +510,23 @@ void SygusUnifRl::DecisionTreeInfo::setConditions( // set new condition values d_enums.insert(d_enums.end(), enums.begin(), enums.end()); d_conds.insert(d_conds.end(), conds.begin(), conds.end()); + // add to condition pool + if (options::sygusUnifCondIndependent()) + { + if (Trace.isOn("sygus-unif-cond-pool")) + { + d_cond_mvs.insert(conds.begin(), conds.end()); + for (const Node& condv : conds) + { + if (d_cond_mvs.find(condv) == d_cond_mvs.end()) + { + Trace("sygus-unif-cond-pool") + << " ...adding to condition pool : " + << d_unif->d_tds->sygusToBuiltin(condv, condv.getType()) << "\n"; + } + } + } + } } unsigned SygusUnifRl::DecisionTreeInfo::getStrategyIndex() const @@ -519,8 +534,6 @@ unsigned SygusUnifRl::DecisionTreeInfo::getStrategyIndex() const return d_strategy_index; } -using UNodePair = std::pair; - Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, std::vector& lemmas) { @@ -532,6 +545,62 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, Trace("sygus-unif-sol") << "Decision::buildSol with " << d_hds.size() << " evaluation heads and " << d_conds.size() << " conditions..." << std::endl; + + return options::sygusUnifCondIndependent() ? buildSolAllCond(cons, lemmas) + : buildSolMinCond(cons, lemmas); +} + +Node SygusUnifRl::DecisionTreeInfo::buildSolAllCond(Node cons, + std::vector& lemmas) +{ + // model values for evaluation heads + std::map hd_mv; + // add conditions + d_conds.clear(); + d_conds.insert(d_conds.end(), d_cond_mvs.begin(), d_cond_mvs.end()); + unsigned num_conds = d_conds.size(); + for (unsigned i = 0; i < num_conds; ++i) + { + d_pt_sep.d_trie.addClassifier(&d_pt_sep, i); + } + // add heads + for (const Node& e : d_hds) + { + Node v = d_unif->d_parent->getModelValue(e); + hd_mv[e] = v; + Node er = d_pt_sep.d_trie.add(e, &d_pt_sep, num_conds); + // are we in conflict? + if (er == e) + { + // new separation class, no conflict + continue; + } + Assert(hd_mv.find(er) != hd_mv.end()); + // merged into separation class with same model value, no conflict + if (hd_mv[e] == hd_mv[er]) + { + continue; + } + // conflict. Explanation? + Trace("sygus-unif-sol") + << " ...can't separate " << e << " from " << er << std::endl; + return Node::null(); + } + Trace("sygus-unif-sol") << "...ready to build solution from DT\n"; + Node sol = d_pt_sep.extractSol(cons, hd_mv); + // repeated solution + if (options::sygusUnifCondIndNoRepeatSol() + && d_sols.find(sol) != d_sols.end()) + { + return Node::null(); + } + d_sols.insert(sol); + return sol; +} + +Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons, + std::vector& lemmas) +{ NodeManager* nm = NodeManager::currentNM(); // model values for evaluation heads std::map hd_mv; @@ -749,13 +818,20 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, } Trace("sygus-unif-sol") << "...ready to build solution from DT\n"; + return d_pt_sep.extractSol(cons, hd_mv); +} + +Node SygusUnifRl::DecisionTreeInfo::PointSeparator::extractSol( + Node cons, std::map& hd_mv) +{ // Traverse trie and build ITE with cons + NodeManager* nm = NodeManager::currentNM(); std::map cache; std::map::iterator it; std::vector visit; unsigned index = 0; LazyTrie* trie; - IndTriePair root = IndTriePair(0, &d_pt_sep.d_trie.d_trie); + IndTriePair root = IndTriePair(0, &d_trie.d_trie); visit.push_back(root); while (!visit.empty()) { @@ -772,10 +848,10 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, { 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()) - << "\n"; + Trace("sygus-unif-sol-debug") << "......leaf, build " + << d_dt->d_unif->d_tds->sygusToBuiltin( + cache[cur], cache[cur].getType()) + << "\n"; continue; } cache[cur] = Node::null(); @@ -791,7 +867,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, Assert(trie->d_children.size() == 1 || trie->d_children.size() == 2); std::vector children(4); children[0] = cons; - children[1] = d_conds[index]; + children[1] = d_dt->d_conds[index]; unsigned i = 0; for (std::pair& p_nt : trie->d_children) { @@ -805,8 +881,12 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, { cache[cur] = children[i]; Trace("sygus-unif-sol-debug") - << "......no cond, build " - << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType()) + << "......no need for cond " + << d_dt->d_unif->d_tds->sygusToBuiltin(d_dt->d_conds[index], + d_dt->d_conds[index].getType()) + << ", build " + << d_dt->d_unif->d_tds->sygusToBuiltin(cache[cur], + cache[cur].getType()) << "\n"; continue; } @@ -814,15 +894,11 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, cache[cur] = nm->mkNode(APPLY_CONSTRUCTOR, children); Trace("sygus-unif-sol-debug") << "......build node " - << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType()) + << d_dt->d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType()) << "\n"; } Assert(cache.find(root) != cache.end()); Assert(!cache.find(root)->second.isNull()); - Trace("sygus-unif-sol") << "...solution is " - << d_unif->d_tds->sygusToBuiltin( - cache[root], cache[root].getType()) - << "\n"; return cache[root]; } diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index c9bdf5691..b2db53aeb 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -205,16 +205,27 @@ class SygusUnifRl : public SygusUnif unsigned strategy_index); /** 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 + /** builds solution, if possible, using the given constructor * - * 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 by the current set of conditions. - * - * This method either returns a solution (if all points are separated). - * It it fails, it adds a conflict lemma to lemmas. + * A solution is possible when all different valued heads can be separated, + * i.e. the current set of conditions separates them in a decision tree */ Node buildSol(Node cons, std::vector& lemmas); + /** bulids a solution by considering all condition values ever enumerated */ + Node buildSolAllCond(Node cons, std::vector& lemmas); + /** builds a solution by incrementally adding points and conditions to DT + * + * Differently from the above method, here a condition is only added to the + * DT when it's necessary for resolving a separation conflict (i.e. heads + * with different values in the same leaf of the DT). Only one value per + * condition enumerated is considered. + * + * If a solution cannot be built, then there are more conflicts to be + * resolved than condition enumerators. A conflict lemma is added to lemmas + * that forces a new assigment in which the conflict is removed (heads are + * made equal) or a new condition is enumerated to try to separate them. + */ + Node buildSolMinCond(Node cons, std::vector& lemmas); /** reference to parent unif util */ SygusUnifRl* d_unif; /** enumerator template (if no templates, nodes in pair are Node::null()) */ @@ -223,6 +234,8 @@ class SygusUnifRl : public SygusUnif std::vector d_conds; /** gathered evaluation point heads */ std::vector d_hds; + /** all enumerated model values for conditions */ + std::unordered_set d_cond_mvs; /** get condition enumerator */ Node getConditionEnumerator() const { return d_cond_enum; } /** set conditions */ @@ -231,6 +244,9 @@ class SygusUnifRl : public SygusUnif const std::vector& conds); private: + /** Accumulates solutions built when considering all enumerated condition + * values (which may generate repeated solutions) */ + std::unordered_set d_sols; /** * Conditional enumerator variables corresponding to the condition values in * d_conds. These are used for generating separation lemmas during @@ -278,6 +294,8 @@ class SygusUnifRl : public SygusUnif /** the lazy trie for building the separation classes */ LazyTrieMulti d_trie; + /** extracts solution from decision tree built */ + Node extractSol(Node cons, std::map& hd_mv); private: /** reference to parent unif util */