From: Haniel Barbosa Date: Wed, 9 May 2018 21:45:43 +0000 (-0500) Subject: Piecing solutions together in CegisUnif (#1894) X-Git-Tag: cvc5-1.0.0~5070 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a7393ad4724476d7544483996f65877876698348;p=cvc5.git Piecing solutions together in CegisUnif (#1894) --- diff --git a/src/theory/quantifiers/lazy_trie.cpp b/src/theory/quantifiers/lazy_trie.cpp index 9e910b43a..21a87c792 100644 --- a/src/theory/quantifiers/lazy_trie.cpp +++ b/src/theory/quantifiers/lazy_trie.cpp @@ -59,8 +59,6 @@ Node LazyTrie::add(Node n, return Node::null(); } -using IndTriePair = std::pair; - void LazyTrieMulti::addClassifier(LazyTrieEvaluator* ev, unsigned ntotal) { Trace("lazy-trie-multi") << "LazyTrieM: Adding classifier " << ntotal + 1 diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h index 2da76d6ef..935b9bec1 100644 --- a/src/theory/quantifiers/lazy_trie.h +++ b/src/theory/quantifiers/lazy_trie.h @@ -94,6 +94,8 @@ class LazyTrie bool forceKeep); }; +using IndTriePair = std::pair; + /** Lazy trie with multiple elements per leaf * * As the above trie, but allows multiple elements per leaf. This is done by @@ -157,7 +159,6 @@ class LazyTrieMulti * containing only itself. */ Node add(Node f, LazyTrieEvaluator* ev, unsigned ntotal); - private: /** 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 06b552276..a99e726b6 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -73,25 +73,32 @@ void CegisUnif::getTermList(const std::vector& candidates, { for (const Node& c : candidates) { + // Non-unif candidate are themselves the enumerators if (!d_sygus_unif.usingUnif(c)) { enums.push_back(c); continue; } - Valuation& valuation = d_qe->getValuation(); - for (const Node& e : d_cond_enums) + // Collect heads of candidate + for (const Node& hd : d_sygus_unif.getEvalPointHeads(c)) { - Trace("cegis-unif-debug") << "Check conditional enumerator : " << e - << std::endl; - Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); - Node g = d_enum_to_active_guard[e]; - // Get whether the active guard for this enumerator is set. If so, then - // there may exist more values for it, and hence we add it to enums. - Node gstatus = valuation.getSatValue(g); - if (!gstatus.isNull() && gstatus.getConst()) - { - enums.push_back(e); - } + Trace("cegis-unif-enum-debug") << "......cand " << c << " with enum hd " + << hd << "\n"; + enums.push_back(hd); + } + } + // Collect condition enumerators + Valuation& valuation = d_qe->getValuation(); + for (const Node& e : d_cond_enums) + { + Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); + Node g = d_enum_to_active_guard[e]; + // Get whether the active guard for this enumerator is set. If so, then + // there may exist more values for it, and hence we add it to enums. + Node gstatus = valuation.getSatValue(g); + if (!gstatus.isNull() && gstatus.getConst()) + { + enums.push_back(e); } } } @@ -102,21 +109,15 @@ bool CegisUnif::constructCandidates(const std::vector& enums, std::vector& candidate_values, std::vector& lems) { - if (addEvalLemmas(enums, enum_values)) - { - Trace("cegis-unif-lemma") << "Added eval lemmas\n"; - return false; - } - unsigned min_term_size = 0; - std::vector enum_consider; NodeManager* nm = NodeManager::currentNM(); Trace("cegis-unif-enum") << "Register new enumerated values :\n"; for (unsigned i = 0, size = enums.size(); i < size; ++i) { - // Only conditional enumerators will be notified to unif utility - if (std::find(d_cond_enums.begin(), d_cond_enums.end(), enums[i]) - == d_cond_enums.end()) + // 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") << " Ignoring non-unif candidate " << enums[i] + << std::endl; continue; } if (Trace.isOn("cegis-unif-enum")) @@ -127,41 +128,43 @@ bool CegisUnif::constructCandidates(const std::vector& enums, ->toStreamSygus(ss, enum_values[i]); Trace("cegis-unif-enum") << ss.str() << std::endl; } - unsigned sz = d_tds->getSygusTermSize(enum_values[i]); - if (i == 0 || sz < min_term_size) - { - enum_consider.clear(); - min_term_size = sz; - enum_consider.push_back(i); - } - else if (sz == min_term_size) - { - enum_consider.push_back(i); - } - } - // only consider the enumerators that are at minimum size (for fairness) - Trace("cegis-unif-enum") << "...register " << enum_consider.size() << " / " - << enums.size() << std::endl; - for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; ++i) - { - unsigned j = enum_consider[i]; - Node e = enums[j], v = enum_values[j]; + Node e = enums[i], v = enum_values[i]; std::vector enum_lems; d_sygus_unif.notifyEnumeration(e, v, enum_lems); - // the lemmas must be guarded by the active guard of the enumerator - Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); - Node g = d_enum_to_active_guard[e]; + // introduce lemmas to exclude this value of a condition enumerator from + // future consideration + std::map::iterator it = d_enum_to_active_guard.find(e); + if (it == d_enum_to_active_guard.end()) + { + continue; + } for (unsigned j = 0, size = enum_lems.size(); j < size; ++j) { - enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]); + enum_lems[j] = nm->mkNode(OR, it->second.negate(), enum_lems[j]); } lems.insert(lems.end(), enum_lems.begin(), enum_lems.end()); } - // divide-and-conquer solution bulding for candidates using unif util + // evaluate on refinement lemmas + if (addEvalLemmas(enums, enum_values)) + { + Trace("cegis-unif-lemma") << "Added eval lemmas\n"; + return false; + } + // build solutions (for unif candidates a divide-and-conquer approach is used) std::vector sols; if (d_sygus_unif.constructSolution(sols)) { candidate_values.insert(candidate_values.end(), sols.begin(), sols.end()); + if (Trace.isOn("cegis-unif")) + { + Trace("cegis-unif") << "* Candidate solutions are:\n"; + for (const Node& sol : sols) + { + Trace("cegis-unif") + << "... " << d_tds->sygusToBuiltin(sol, sol.getType()) << "\n"; + } + Trace("cegis-unif") << "---CegisUnif Engine---\n"; + } return true; } return false; @@ -175,6 +178,7 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, std::map > eval_pts; Node plem = d_sygus_unif.addRefLemma(lem, eval_pts); d_refinement_lemmas.push_back(plem); + Trace("cegis-unif") << "* Refinement lemma:\n" << plem << "\n"; // Notify the enumeration manager if there are new evaluation points for (const std::pair >& ep : eval_pts) { @@ -200,11 +204,14 @@ CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe, d_ret_dec(qe->getSatContext(), false), d_curr_guq_val(qe->getSatContext(), 0) { + d_initialized = false; d_tds = d_qe->getTermDatabaseSygus(); } void CegisUnifEnumManager::initialize(const std::vector& cs) { + Assert(!d_initialized); + d_initialized = true; if (cs.empty()) { return; @@ -234,6 +241,8 @@ void CegisUnifEnumManager::registerEvalPts(const std::vector& eis, Node c) for (const Node& ei : eis) { Assert(ei.getType() == ct); + Trace("cegis-unif-enum") << "...for cand " << c << " adding hd " << ei + << " at size " << p.first << "\n"; registerEvalPtAtSize(ct, ei, p.second, p.first); } } @@ -241,12 +250,12 @@ void CegisUnifEnumManager::registerEvalPts(const std::vector& eis, Node c) Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority) { - // have we returned our decision in the current SAT context? - if (d_ret_dec.get()) + // are we not initialized or have we returned our decision in the current SAT + // context? + if (!d_initialized || d_ret_dec.get()) { return Node::null(); } - // only call this after initialization if (d_ce_info.empty()) { // if no enumerators, the decision is null @@ -257,7 +266,6 @@ Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority) bool value; if (!d_qe->getValuation().hasSatValue(lit, value)) { - d_ret_dec = true; priority = 0; return lit; } @@ -267,6 +275,7 @@ Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority) incrementNumEnumerators(); return getNextDecisionRequest(priority); } + d_ret_dec = true; return Node::null(); } @@ -308,6 +317,8 @@ void CegisUnifEnumManager::incrementNumEnumerators() TypeNode ct = ci.first; for (const Node& ei : ci.second.d_eval_points) { + Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei + << " to new size " << new_size << "\n"; registerEvalPtAtSize(ct, ei, new_lit, new_size); } } @@ -342,6 +353,7 @@ void CegisUnifEnumManager::registerEvalPtAtSize(TypeNode ct, disj.push_back(ei.eqNode(itc->second.d_enums[i])); } Node lem = NodeManager::currentNM()->mkNode(OR, disj); + Trace("cegis-unif-enum") << "Adding lemma " << 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 4ea6a887a..ed38c9268 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -85,6 +85,8 @@ class CegisUnifEnumManager TermDbSygus* d_tds; /** reference to the parent conjecture */ CegConjecture* d_parent; + /** whether this module has been initialized */ + bool d_initialized; /** null node */ Node d_null; /** information per initialized type */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 1260c62af..a2299f834 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -174,7 +174,10 @@ Node SygusUnifRl::purifyLemma(Node n, // Build purified head with fresh skolem and recreate node std::stringstream ss; ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++; - Node new_f = nm->mkSkolem(ss.str(), nb[0].getType()); + Node new_f = nm->mkSkolem(ss.str(), + nb[0].getType(), + "head of unif evaluation point", + NodeManager::SKOLEM_EXACT_NAME); // Adds new enumerator to map from candidate Trace("sygus-unif-rl-purify") << "...new enum " << new_f << " for candidate " << nb[0] << "\n"; @@ -317,25 +320,32 @@ Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind) { indent("sygus-unif-sol", ind); Trace("sygus-unif-sol") << "ConstructSol: SygusRL : " << e << std::endl; + // retrieve strategy information + TypeNode etn = e.getType(); + EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn); + StrategyNode& snode = tinfo.getStrategyNode(nrole); + if (nrole != role_equal) + { + return Node::null(); + } // is there a decision tree strategy? - if (nrole == role_equal) + std::map::iterator itd = d_stratpt_to_dt.find(e); + // for now only considering simple case of sole "ITE(cond, e, e)" strategy + if (itd == d_stratpt_to_dt.end()) { - std::map::iterator itd = d_stratpt_to_dt.find(e); - if (itd != d_stratpt_to_dt.end()) - { - indent("sygus-unif-sol", ind); - Trace("sygus-unif-sol") << "...it has a decision tree strategy.\n"; - if (itd->second.isSeparated()) - { - Trace("sygus-unif-sol") - << "...... points are separated and I have for root enum the value " - << d_parent->getModelValue(e) << "\n"; - return d_parent->getModelValue(e); - } - } + return Node::null(); } - - return Node::null(); + indent("sygus-unif-sol", ind); + Trace("sygus-unif-sol") << "...it has a decision tree strategy.\n"; + // whether empty set of points + if (d_cand_to_eval_hds[f].empty()) + { + Trace("sygus-unif-sol") << "...... no points, return root enum value " + << d_parent->getModelValue(e) << "\n"; + return d_parent->getModelValue(e); + } + EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()]; + return itd->second.buildSol(etis->d_cons); } bool SygusUnifRl::usingUnif(Node f) @@ -343,6 +353,16 @@ bool SygusUnifRl::usingUnif(Node f) return d_unif_candidates.find(f) != d_unif_candidates.end(); } +std::vector SygusUnifRl::getEvalPointHeads(Node c) +{ + std::map>::iterator it = d_cand_to_eval_hds.find(c); + if (it == d_cand_to_eval_hds.end()) + { + return std::vector(); + } + return it->second; +} + void SygusUnifRl::registerStrategy(Node f) { if (Trace.isOn("sygus-unif-rl-strat")) @@ -397,14 +417,17 @@ void SygusUnifRl::registerStrategyNode( << " ...detected recursive ITE strategy, condition enumerator : " << cond << std::endl; // indicate that we will be enumerating values for cond - registerConditionalEnumerator(f, e, cond); + registerConditionalEnumerator(f, e, cond, j); } } // TODO: recurse? for (std::pair& cec : etis->d_cenum) } } -void SygusUnifRl::registerConditionalEnumerator(Node f, Node e, Node cond) +void SygusUnifRl::registerConditionalEnumerator(Node f, + Node e, + Node cond, + unsigned strategy_index) { // we will do unification for this candidate d_unif_candidates.insert(f); @@ -419,18 +442,20 @@ void SygusUnifRl::registerConditionalEnumerator(Node f, Node e, Node cond) d_cenum_to_stratpt[cond].clear(); } // register that this strategy node has a decision tree construction - d_stratpt_to_dt[e].initialize(cond, this, &d_strategy[f]); + d_stratpt_to_dt[e].initialize(cond, this, &d_strategy[f], strategy_index); // associate conditional enumerator with strategy node d_cenum_to_stratpt[cond].push_back(e); } void SygusUnifRl::DecisionTreeInfo::initialize(Node cond_enum, SygusUnifRl* unif, - SygusUnifStrategy* strategy) + SygusUnifStrategy* strategy, + unsigned strategy_index) { d_cond_enum = cond_enum; d_unif = unif; d_strategy = strategy; + d_strategy_index = strategy_index; // Retrieve template EnumInfo& eiv = d_strategy->getEnumInfo(d_cond_enum); d_template = NodePair(eiv.d_template, eiv.d_template_arg); @@ -449,30 +474,154 @@ void SygusUnifRl::DecisionTreeInfo::addCondValue(Node condv) d_pt_sep.d_trie.addClassifier(&d_pt_sep, d_conds.size() - 1); } +unsigned SygusUnifRl::DecisionTreeInfo::getStrategyIndex() const +{ + return d_strategy_index; +} + +using UNodePair = std::pair; + +Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons) +{ + if (!d_template.first.isNull()) + { + Trace("sygus-unif-sol") << "...templated conditions unsupported\n"; + return Node::null(); + } + if (!isSeparated()) + { + Trace("sygus-unif-sol") << "...separation check failed\n"; + 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; + unsigned index = 0; + LazyTrie* trie; + IndTriePair root = IndTriePair(0, &d_pt_sep.d_trie.d_trie); + visit.push_back(root); + while (!visit.empty()) + { + index = visit.back().first; + trie = visit.back().second; + visit.pop_back(); + IndTriePair cur = IndTriePair(index, trie); + it = cache.find(cur); + // traverse children so results are saved to build node for parent + if (it == cache.end()) + { + // 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]; + Trace("sygus-unif-sol-debug") + << "......leaf, build " + << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType()) + << "\n"; + continue; + } + cache[cur] = Node::null(); + visit.push_back(cur); + for (std::pair& p_nt : trie->d_children) + { + visit.push_back(IndTriePair(index + 1, &p_nt.second)); + } + continue; + } + // retrieve terms of children and build result + Assert(it->second.isNull()); + Assert(trie->d_children.size() == 1 || trie->d_children.size() == 2); + std::vector children(4); + children[0] = cons; + children[1] = d_conds[index]; + unsigned i = 0; + for (std::pair& p_nt : trie->d_children) + { + i = p_nt.first.getConst() ? 2 : 3; + Assert(cache.find(IndTriePair(index + 1, &p_nt.second)) != cache.end()); + children[i] = cache[IndTriePair(index + 1, &p_nt.second)]; + Assert(!children[i].isNull()); + } + // condition is useless or result children are equal, no no need for ITE + if (trie->d_children.size() == 1 || children[2] == children[3]) + { + cache[cur] = children[i]; + Trace("sygus-unif-sol-debug") + << "......no cond, build " + << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType()) + << "\n"; + continue; + } + Assert(trie->d_children.size() == 2); + cache[cur] = nm->mkNode(APPLY_CONSTRUCTOR, children); + Trace("sygus-unif-sol-debug") + << "......build node " + << 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]; +} + bool SygusUnifRl::DecisionTreeInfo::isSeparated() { + d_hd_values.clear(); for (const std::pair>& rep_to_class : d_pt_sep.d_trie.d_rep_to_class) { Assert(!rep_to_class.second.empty()); - Node v = rep_to_class.second[0]; + 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"; - break; + return false; } } - // Heads with different model values - if (i != size) - { - return false; - } } return true; } diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index d618876da..58cf9011e 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -32,6 +32,7 @@ using BoolNodePairHashFunction = PairHashFunction; using BoolNodePairMap = std::unordered_map; +using NodePairMap = std::unordered_map; using NodePair = std::pair; class CegConjecture; @@ -79,6 +80,9 @@ class SygusUnifRl : public SygusUnif */ bool usingUnif(Node f); + /** retrieve the head of evaluation points for candidate c, if any */ + std::vector getEvalPointHeads(Node c); + protected: /** reference to the parent conjecture */ CegConjecture* d_parent; @@ -168,11 +172,25 @@ class SygusUnifRl : public SygusUnif /** initializes this class */ void initialize(Node cond_enum, SygusUnifRl* unif, - SygusUnifStrategy* strategy); + SygusUnifStrategy* strategy, + unsigned strategy_index); /** adds the respective evaluation point of the head f */ void addPoint(Node f); /** 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 + * + * 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. + * + * 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. + */ + Node buildSol(Node cons); /** whether all points that must be separated are separated **/ bool isSeparated(); /** reference to parent unif util */ @@ -184,15 +202,24 @@ class SygusUnifRl : public SygusUnif private: /** - * reference to infered strategy for the function-to-synthesize this DT is + * reference to inferred strategy for the function-to-synthesize this DT is * associated with */ SygusUnifStrategy* d_strategy; + /** index of strategy information of strategy node this DT is based on + * + * this is the index of the strategy (d_strats[index]) in the strategy node + * to which this decision tree corresponds, which can be accessed through + * the above strategy reference + */ + unsigned d_strategy_index; /** * The enumerator in the strategy tree that stores conditions of the * 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 @@ -251,7 +278,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); + void registerConditionalEnumerator(Node f, + Node e, + Node cond, + unsigned strategy_index); }; } /* CVC4::theory::quantifiers namespace */