diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-14 19:27:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-14 19:27:58 -0500 |
commit | b87e44544862043c4cff523134662c10cfbccf0f (patch) | |
tree | 09529edb6824c7a86cd29bab4a3339fd11bd8c1b /src/theory/quantifiers/sygus/cegis_unif.cpp | |
parent | 4e96b1d5e01260acc79bdbb86322e23c7cf9567f (diff) |
Incorporating dynamic condition enumeration into cegis unif (#1916)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 269 |
1 files changed, 148 insertions, 121 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index def21e6cc..920b142bb 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -38,33 +38,44 @@ bool CegisUnif::initialize(Node n, const std::vector<Node>& candidates, std::vector<Node>& lemmas) { - Trace("cegis-unif-debug") << "Initialize CegisUnif : " << n << std::endl; - // Init UNIF util + Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl; + // list of strategy points for unification candidates + std::vector<Node> unif_candidate_pts; + // map from strategy points to their conditions + std::map<Node, Node> pt_to_cond; + // strategy lemmas for each strategy point std::map<Node, std::vector<Node>> strategy_lemmas; - d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, strategy_lemmas); - std::vector<Node> unif_candidates; - // Initialize enumerators for non-unif functions-to-synhesize - for (const Node& c : candidates) + // Initialize strategies for all functions-to-synhesize + for (const Node& f : candidates) { - if (!d_sygus_unif.usingUnif(c)) + // Init UNIF util for this candidate + d_sygus_unif.initializeCandidate( + d_qe, f, d_cand_to_strat_pt[f], strategy_lemmas); + if (!d_sygus_unif.usingUnif(f)) { - Trace("cegis-unif") << "* non-unification candidate : " << c << std::endl; - d_tds->registerEnumerator(c, c, d_parent); + Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl; + d_tds->registerEnumerator(f, f, d_parent); } else { - Trace("cegis-unif") << "* unification candidate : " << c << std::endl; - unif_candidates.push_back(c); + Trace("cegis-unif") << "* unification candidate : " << f + << " with strategy points:" << std::endl; + std::vector<Node>& enums = d_cand_to_strat_pt[f]; + unif_candidate_pts.insert( + unif_candidate_pts.end(), enums.begin(), enums.end()); + // map strategy point to its condition in pt_to_cond + for (const Node& e : enums) + { + Node cond = d_sygus_unif.getConditionForEvaluationPoint(e); + Assert(!cond.isNull()); + Trace("cegis-unif") + << " " << e << " with condition : " << cond << std::endl; + pt_to_cond[e] = cond; + } } } - for (const Node& e : d_cond_enums) - { - Node g = d_tds->getActiveGuardForEnumerator(e); - Assert(!g.isNull()); - d_enum_to_active_guard[e] = g; - } // initialize the enumeration manager - d_u_enum_manager.initialize(unif_candidates, strategy_lemmas); + d_u_enum_manager.initialize(unif_candidate_pts, pt_to_cond, strategy_lemmas); return true; } @@ -79,26 +90,26 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates, enums.push_back(c); continue; } - // Collect heads of candidate + // 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"; 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<bool>()) + // 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]) { - enums.push_back(e); + std::vector<Node> 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()); } } } @@ -109,7 +120,8 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums, std::vector<Node>& candidate_values, std::vector<Node>& lems) { - NodeManager* nm = NodeManager::currentNM(); + // build the values of the condition enumerators for each strategy point + std::map<Node, std::vector<Node>> condition_map; Trace("cegis-unif-enum") << "Register new enumerated values :\n"; for (unsigned i = 0, size = enums.size(); i < size; ++i) { @@ -129,26 +141,27 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums, Trace("cegis-unif-enum") << ss.str() << std::endl; } Node e = enums[i], v = enum_values[i]; - std::vector<Node> enum_lems; - d_sygus_unif.notifyEnumeration(e, v, enum_lems); - // introduce lemmas to exclude this value of a condition enumerator from - // future consideration - std::map<Node, Node>::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) + std::map<Node, Node>::iterator itc = d_cenum_to_strat_pt.find(e); + if (itc != d_cenum_to_strat_pt.end()) { - enum_lems[j] = nm->mkNode(OR, it->second.negate(), enum_lems[j]); + 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); } - lems.insert(lems.end(), enum_lems.begin(), enum_lems.end()); } // 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<const Node, std::vector<Node>> cs : condition_map) + { + d_sygus_unif.setConditions(cs.first, cs.second); + } + // TODO : check symmetry breaking for enumerators + // TODO : check separation of evaluation heads wrt condition enumerators and + // add lemmas. // build solutions (for unif candidates a divide-and-conquer approach is used) std::vector<Node> sols; if (d_sygus_unif.constructSolution(sols)) @@ -208,82 +221,80 @@ CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe, } void CegisUnifEnumManager::initialize( - const std::vector<Node>& cs, + const std::vector<Node>& es, + const std::map<Node, Node>& e_to_cond, const std::map<Node, std::vector<Node>>& strategy_lemmas) { Assert(!d_initialized); d_initialized = true; - if (cs.empty()) + if (es.empty()) { return; } - // process strategy lemmas - std::map<TypeNode, std::pair<Node, std::vector<Node>>> tn_strategy_lemmas; - for (const std::pair<const Node, std::vector<Node>>& p : strategy_lemmas) - { - if (Trace.isOn("cegis-unif-enum-debug")) - { - Trace("cegis-unif-enum-debug") << "...lemmas of strategy pt " << p.first - << ":\n"; - for (const Node& lem : p.second) - { - Trace("cegis-unif-enum-debug") << "\t" << lem << "\n"; - } - } - TypeNode tn = p.first.getType(); - Assert(tn_strategy_lemmas.find(tn) == tn_strategy_lemmas.end()); - tn_strategy_lemmas[tn].first = p.first; - tn_strategy_lemmas[tn].second = p.second; - } // initialize type information for candidates NodeManager* nm = NodeManager::currentNM(); - for (const Node& c : cs) + for (const Node& e : es) { - Trace("cegis-unif-enum-debug") << "...adding candidate " << c << "\n"; + Trace("cegis-unif-enum-debug") << "...adding strategy point " << e << "\n"; // currently, we allocate the same enumerators for candidates of the same // type - TypeNode tn = c.getType(); - d_ce_info[tn].d_candidates.push_back(c); - // retrieve symmetry breaking lemma template for type if not already init - if (!d_ce_info[tn].d_sbt_lemma.isNull()) - { - continue; - } - std::map<const TypeNode, std::pair<Node, std::vector<Node>>>::iterator it = - tn_strategy_lemmas.find(tn); - if (it == tn_strategy_lemmas.end()) + d_ce_info[e].d_pt = e; + std::map<Node, Node>::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"; + d_ce_info[e].d_ce_type = cond.getType(); + // initialize the symmetry breaking lemma templates + for (unsigned index = 0; index < 2; index++) { - continue; + Assert(d_ce_info[e].d_sbt_lemma_tmpl[index].first.isNull()); + Node sp = index == 0 ? e : cond; + std::map<Node, std::vector<Node>>::const_iterator it = + strategy_lemmas.find(sp); + if (it == strategy_lemmas.end()) + { + continue; + } + // collect lemmas for removing redundant ops for this candidate's type + Node d_sbt_lemma = + it->second.size() == 1 ? it->second[0] : nm->mkNode(AND, it->second); + Trace("cegis-unif-enum-debug") + << "...adding lemma template to remove redundant operators for " << sp + << " --> lambda " << sp << ". " << d_sbt_lemma << "\n"; + d_ce_info[e].d_sbt_lemma_tmpl[index] = + std::pair<Node, Node>(d_sbt_lemma, sp); } - // collect lemmas for removing redundant ops for this candidate's type - d_ce_info[tn].d_sbt_lemma = nm->mkNode(AND, it->second.second); - Trace("cegis-unif-enum-debug") - << "...adding lemma template to remove redundant operators for " << c - << " and its type " << tn << " --> " << d_ce_info[tn].d_sbt_lemma - << "\n"; - d_ce_info[tn].d_sbt_arg = it->second.first; } // initialize the current literal incrementNumEnumerators(); } -void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node c) +void CegisUnifEnumManager::getCondEnumeratorsForStrategyPt( + Node e, std::vector<Node>& ces) const +{ + std::map<Node, StrategyPtInfo>::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()); +} + +void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node e) { // candidates of the same type are managed - TypeNode ct = c.getType(); - std::map<TypeNode, TypeInfo>::iterator it = d_ce_info.find(ct); + std::map<Node, StrategyPtInfo>::iterator it = d_ce_info.find(e); Assert(it != d_ce_info.end()); it->second.d_eval_points.insert( it->second.d_eval_points.end(), eis.begin(), eis.end()); // register at all already allocated sizes - for (const std::pair<const unsigned, Node>& p : d_guq_lit) + for (const Node& ei : eis) { - for (const Node& ei : eis) + Assert(ei.getType() == e.getType()); + for (const std::pair<const unsigned, Node>& p : d_guq_lit) { - Assert(ei.getType() == ct); - Trace("cegis-unif-enum") << "...for cand " << c << " adding hd " << ei + Trace("cegis-unif-enum") << "...for cand " << e << " adding hd " << ei << " at size " << p.first << "\n"; - registerEvalPtAtSize(ct, ei, p.second, p.first); + registerEvalPtAtSize(e, ei, p.second, p.first); } } } @@ -335,57 +346,73 @@ void CegisUnifEnumManager::incrementNumEnumerators() d_qe->getOutputChannel().requirePhase(new_lit, true); d_guq_lit[new_size] = new_lit; // allocate an enumerator for each candidate - for (std::pair<const TypeNode, TypeInfo>& ci : d_ce_info) + for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info) { - TypeNode ct = ci.first; + Node c = ci.first; + TypeNode ct = c.getType(); Node eu = nm->mkSkolem("eu", ct); - // instantiate template for removing redundant operators - if (!ci.second.d_sbt_lemma.isNull()) + Node ceu; + if (!ci.second.d_enums[0].empty()) { - Node templ = ci.second.d_sbt_lemma; - TNode templ_var = ci.second.d_sbt_arg; - Node sym_break_red_ops = templ.substitute(templ_var, eu); - Trace("cegis-unif-enum-lemma") - << "CegisUnifEnum::lemma, remove redundant ops of " << eu << " : " - << sym_break_red_ops << "\n"; - d_qe->getOutputChannel().lemma(sym_break_red_ops); + // make a new conditional enumerator as well, starting the + // second type around + ceu = nm->mkSkolem("cu", ci.second.d_ce_type); } - if (!ci.second.d_enums.empty()) + // register the new enumerators + for (unsigned index = 0; index < 2; index++) { - Node eu_prev = ci.second.d_enums.back(); - // symmetry breaking - Node size_eu = nm->mkNode(DT_SIZE, eu); - Node size_eu_prev = nm->mkNode(DT_SIZE, eu_prev); - Node sym_break = nm->mkNode(GEQ, size_eu, size_eu_prev); + Node e = index == 0 ? eu : ceu; + if (e.isNull()) + { + continue; + } + // register the enumerator + ci.second.d_enums[index].push_back(e); + d_tds->registerEnumerator(e, ci.second.d_pt, d_parent); + // 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 + 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); // if the sygus datatype is interpreted as an infinite type // (this should be the case for almost all examples) - if (!ct.isInterpretedFinite()) + TypeNode et = e.getType(); + if (!et.isInterpretedFinite()) { // it is disequal from all previous ones - for (const Node eui : ci.second.d_enums) + for (const Node ei : ci.second.d_enums[index]) { - Node deq = eu.eqNode(eui).negate(); + Node deq = e.eqNode(ei).negate(); Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, enum deq:" << deq << "\n"; d_qe->getOutputChannel().lemma(deq); } } } - ci.second.d_enums.push_back(eu); - d_tds->registerEnumerator(eu, d_null, d_parent); } // register the evaluation points at the new value - for (std::pair<const TypeNode, TypeInfo>& ci : d_ce_info) + for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info) { - TypeNode ct = ci.first; + Node c = 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); + registerEvalPtAtSize(c, ei, new_lit, new_size); } } } @@ -403,20 +430,20 @@ Node CegisUnifEnumManager::getLiteral(unsigned n) const return itc->second; } -void CegisUnifEnumManager::registerEvalPtAtSize(TypeNode ct, +void CegisUnifEnumManager::registerEvalPtAtSize(Node e, Node ei, Node guq_lit, unsigned n) { // must be equal to one of the first n enums - std::map<TypeNode, TypeInfo>::iterator itc = d_ce_info.find(ct); + std::map<Node, StrategyPtInfo>::iterator itc = d_ce_info.find(e); Assert(itc != d_ce_info.end()); - Assert(itc->second.d_enums.size() >= n); + Assert(itc->second.d_enums[0].size() >= n); std::vector<Node> disj; disj.push_back(guq_lit.negate()); for (unsigned i = 0; i < n; i++) { - disj.push_back(ei.eqNode(itc->second.d_enums[i])); + 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 |