diff options
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 269 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.h | 86 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 6 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.cpp | 20 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.h | 16 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 16 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.h | 11 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.cpp | 124 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.h | 53 |
9 files changed, 320 insertions, 281 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 diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index dd98b20ba..445ab5f6c 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -29,17 +29,20 @@ namespace quantifiers { /** Cegis Unif Enumeration Manager * * This class enforces a decision heuristic that limits the number of - * unique values given to the set of heads of evaluation points, which are - * variables of sygus datatype type that are introduced by CegisUnif. + * unique values given to the set of heads of evaluation points and conditions + * enumerators for these points, which are variables of sygus datatype type that + * are introduced by CegisUnif. * * It maintains a set of guards, call them G_uq_1 ... G_uq_n, where the * semantics of G_uq_i is "for each type, the heads of evaluation points of that * type are interpreted as a value in a set whose cardinality is at most i". + * We also enforce that the number of condition enumerators for evaluation + * points is equal to (n-1). * * To enforce this, we introduce sygus enumerator(s) of the same type as the - * heads of evaluation points registered to this class and add lemmas that - * enforce that these terms are equal to at least one enumerator (see - * registerEvalPtAtValue). + * heads of evaluation points and condition enumerators registered to this class + * and add lemmas that enforce that these terms are equal to at least one + * enumerator (see registerEvalPtAtValue). */ class CegisUnifEnumManager { @@ -48,24 +51,25 @@ class CegisUnifEnumManager /** initialize candidates * * Notify this class that it will be managing enumerators for the vector - * of functions-to-synthesize (candidate variables) in candidates. This - * function should only be called once. + * of strategy points es. This function should only be called once. * - * Each candidate c in cs should be such that we are using a - * synthesis-by-unification approach for c. + * Each strategy point in es should be such that we are using a + * synthesis-by-unification approach for its candidate. */ - void initialize(const std::vector<Node>& cs, + void initialize(const std::vector<Node>& es, + const std::map<Node, Node>& e_to_cond, const std::map<Node, std::vector<Node>>& strategy_lemmas); + /** get the current set of conditional enumerators for strategy point e */ + void getCondEnumeratorsForStrategyPt(Node e, std::vector<Node>& ces) const; /** register evaluation point for candidate * * This notifies this class that eis is a set of heads of evaluation points - * for candidate c, where c should be a candidate that was passed to - * initialize in the vector cs. + * for strategy point e, where e was passed to initialize in the vector es. * * This may add new lemmas of the form described above * registerEvalPtAtValue on the output channel of d_qe. */ - void registerEvalPts(const std::vector<Node>& eis, Node c); + void registerEvalPts(const std::vector<Node>& eis, Node e); /** get next decision request * * This function has the same contract as Theory::getNextDecisionRequest. @@ -91,23 +95,38 @@ class CegisUnifEnumManager /** null node */ Node d_null; /** information per initialized type */ - class TypeInfo + class StrategyPtInfo { public: - TypeInfo() {} - /** candidates for this type */ - std::vector<Node> d_candidates; - /** the set of enumerators we have allocated for this candidate */ - std::vector<Node> d_enums; - /** the set of evaluation points of this type */ + StrategyPtInfo() {} + /** strategy point for this type */ + Node d_pt; + /** the set of enumerators we have allocated for this strategy point + * + * Index 0 stores the return value enumerators, and index 1 stores the + * conditional enumerators. We have that + * d_enums[0].size()==d_enums[1].size()+1. + */ + std::vector<Node> d_enums[2]; + /** the type of conditional enumerators for this strategy point */ + TypeNode d_ce_type; + /** + * The set of evaluation points of this type. In models, we ensure that + * each of these are equal to one of d_enums[0]. + */ std::vector<Node> d_eval_points; - /** symmetry breaking lemma template for this type */ - Node d_sbt_lemma; - /** argument (to be instantiated) of symmetry breaking lemma template */ - Node d_sbt_arg; + /** symmetry breaking lemma template for this strategy point + * + * Each pair stores (the symmetry breaking lemma template, argument (to be + * instantiated) of symmetry breaking lemma template). + * + * Index 0 stores the symmetry breaking lemma template for return values, + * index 1 stores the template for conditions. + */ + std::pair<Node, Node> d_sbt_lemma_tmpl[2]; }; - /** map types to the above info */ - std::map<TypeNode, TypeInfo> d_ce_info; + /** map strategy points to the above info */ + std::map<Node, StrategyPtInfo> d_ce_info; /** literals of the form G_uq_n for each n */ std::map<unsigned, Node> d_guq_lit; /** Have we returned a decision in the current SAT context? */ @@ -131,9 +150,9 @@ class CegisUnifEnumManager * This sends a lemma of the form: * G_uq_n => ei = d1 V ... V ei = dn * on the output channel of d_qe, where d1...dn are sygus enumerators of the - * same type (ct) as ei. + * same type as e and ei, and ei is an evaluation point of strategy point e. */ - void registerEvalPtAtSize(TypeNode ct, Node ei, Node guq_lit, unsigned n); + void registerEvalPtAtSize(Node e, Node ei, Node guq_lit, unsigned n); }; /** Synthesizes functions in a data-driven SyGuS approach @@ -233,15 +252,12 @@ class CegisUnif : public Cegis SygusUnifRl d_sygus_unif; /** enumerator manager utility */ CegisUnifEnumManager d_u_enum_manager; - /** - * list of conditonal enumerators to build solutions for candidates being - * synthesized with unification techniques - */ - std::vector<Node> d_cond_enums; - /** map from enumerators to active guards */ - std::map<Node, Node> d_enum_to_active_guard; /* The null node */ Node d_null; + /** list of strategy points per candidate */ + std::map<Node, std::vector<Node>> d_cand_to_strat_pt; + /** map from conditional enumerators to their strategy point */ + std::map<Node, Node> d_cenum_to_strat_pt; }; /* class CegisUnif */ } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 401ab03ee..0afd7a82c 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -174,11 +174,9 @@ bool CegConjecturePbe::initialize(Node n, Assert(d_examples.find(c) != d_examples.end()); Trace("sygus-pbe") << "Initialize unif utility for " << c << "..." << std::endl; - std::vector<Node> singleton_c; - singleton_c.push_back(c); std::map<Node, std::vector<Node>> strategy_lemmas; - d_sygus_unif[c].initialize( - d_qe, singleton_c, d_candidate_to_enum[c], strategy_lemmas); + d_sygus_unif[c].initializeCandidate( + d_qe, c, d_candidate_to_enum[c], strategy_lemmas); Assert(!d_candidate_to_enum[c].empty()); Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size() << " enumerators for " << c << "..." << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 5cf96e513..15606c9a4 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -28,20 +28,18 @@ namespace quantifiers { SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {} SygusUnif::~SygusUnif() {} -void SygusUnif::initialize(QuantifiersEngine* qe, - const std::vector<Node>& funs, - std::vector<Node>& enums, - std::map<Node, std::vector<Node>>& strategy_lemmas) + +void SygusUnif::initializeCandidate( + QuantifiersEngine* qe, + Node f, + std::vector<Node>& enums, + std::map<Node, std::vector<Node>>& strategy_lemmas) { - Assert(d_candidates.empty()); d_qe = qe; d_tds = qe->getTermDatabaseSygus(); - for (const Node& f : funs) - { - d_candidates.push_back(f); - // initialize the strategy - d_strategy[f].initialize(qe, f, enums); - } + d_candidates.push_back(f); + // initialize the strategy + d_strategy[f].initialize(qe, f, enums); } bool SygusUnif::constructSolution(std::vector<Node>& sols) diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index fe80a3d44..1c7972978 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -46,10 +46,11 @@ class SygusUnif SygusUnif(); virtual ~SygusUnif(); - /** initialize + /** initialize candidate * - * This initializes this class with functions-to-synthesize funs. We also call - * these "candidate variables". + * This initializes this class with functions-to-synthesize f. We also call + * this a "candidate variable". This function can be called more than once + * for different functions-to-synthesize in the same conjecture. * * This call constructs a set of enumerators for the relevant subfields of * the grammar of f and adds them to enums. These enumerators are those that @@ -61,10 +62,11 @@ class SygusUnif * strategy is ITE_strat). The lemmas are associated with a strategy point of * the respective function-to-synthesize. */ - virtual void initialize(QuantifiersEngine* qe, - const std::vector<Node>& funs, - std::vector<Node>& enums, - std::map<Node, std::vector<Node>>& strategy_lemmas); + virtual void initializeCandidate( + QuantifiersEngine* qe, + Node f, + std::vector<Node>& enums, + std::map<Node, std::vector<Node>>& strategy_lemmas); /** * Notify that the value v has been enumerated for enumerator e. This call diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 60a3d70d8..1b43b77ba 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -466,19 +466,19 @@ SygusUnifIo::SygusUnifIo() : d_check_sol(false), d_cond_count(0) } SygusUnifIo::~SygusUnifIo() {} -void SygusUnifIo::initialize(QuantifiersEngine* qe, - const std::vector<Node>& funs, - std::vector<Node>& enums, - std::map<Node, std::vector<Node>>& strategy_lemmas) +void SygusUnifIo::initializeCandidate( + QuantifiersEngine* qe, + Node f, + std::vector<Node>& enums, + std::map<Node, std::vector<Node>>& strategy_lemmas) { - Assert(funs.size() == 1); d_examples.clear(); d_examples_out.clear(); d_ecache.clear(); - d_candidate = funs[0]; - SygusUnif::initialize(qe, funs, enums, strategy_lemmas); + d_candidate = f; + SygusUnif::initializeCandidate(qe, f, enums, strategy_lemmas); // learn redundant operators based on the strategy - d_strategy[d_candidate].staticLearnRedundantOps(strategy_lemmas); + d_strategy[f].staticLearnRedundantOps(strategy_lemmas); } void SygusUnifIo::addExample(const std::vector<Node>& input, Node output) diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 359aa4443..9a6c02421 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -273,13 +273,14 @@ class SygusUnifIo : public SygusUnif /** initialize * - * The vector funs should be of length one, since I/O specifications across + * We only initialize for one function f, since I/O specifications across * multiple functions can be separated. */ - void initialize(QuantifiersEngine* qe, - const std::vector<Node>& funs, - std::vector<Node>& enums, - std::map<Node, std::vector<Node>>& strategy_lemmas) override; + void initializeCandidate( + QuantifiersEngine* qe, + Node f, + std::vector<Node>& enums, + std::map<Node, std::vector<Node>>& strategy_lemmas) override; /** Notify enumeration */ void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override; diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 6f68a9871..f59331d68 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -25,58 +25,32 @@ namespace quantifiers { SygusUnifRl::SygusUnifRl(CegConjecture* p) : d_parent(p) {} SygusUnifRl::~SygusUnifRl() {} -void SygusUnifRl::initialize(QuantifiersEngine* qe, - const std::vector<Node>& funs, - std::vector<Node>& enums, - std::map<Node, std::vector<Node>>& strategy_lemmas) +void SygusUnifRl::initializeCandidate( + QuantifiersEngine* qe, + Node f, + std::vector<Node>& enums, + std::map<Node, std::vector<Node>>& strategy_lemmas) { // initialize std::vector<Node> all_enums; - SygusUnif::initialize(qe, funs, all_enums, strategy_lemmas); + SygusUnif::initializeCandidate(qe, f, all_enums, strategy_lemmas); // based on the strategy inferred for each function, determine if we are // using a unification strategy that is compatible our approach. - for (const Node& f : funs) - { - d_strategy[f].staticLearnRedundantOps(strategy_lemmas); - registerStrategy(f, strategy_lemmas); - } - enums.insert(enums.end(), d_cond_enums.begin(), d_cond_enums.end()); + d_strategy[f].staticLearnRedundantOps(strategy_lemmas); + registerStrategy(f, enums); // Copy candidates and check whether CegisUnif for any of them - for (const Node& c : d_unif_candidates) + if (d_unif_candidates.find(f) != d_unif_candidates.end()) { - d_hd_to_pt[c].clear(); - d_cand_to_eval_hds[c].clear(); - d_cand_to_hd_count[c] = 0; + d_hd_to_pt[f].clear(); + d_cand_to_eval_hds[f].clear(); + d_cand_to_hd_count[f] = 0; } } void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) { - Trace("sygus-unif-rl-notify") << "SyGuSUnifRl: Adding to enum " << e - << " value " << v << "\n"; - // Exclude v from next enumerations for e - Node exc_lemma = - d_tds->getExplain()->getExplanationForEquality(e, v).negate(); - Trace("sygus-unif-rl-notify-debug") - << "SygusUnifRl : enumeration exclude lemma : " << exc_lemma << std::endl; - lemmas.push_back(exc_lemma); - // Update all desicion trees in which this enumerator is a conditional - // enumerator, if any - std::map<Node, std::vector<Node>>::iterator it = d_cenum_to_stratpt.find(e); - if (it == d_cenum_to_stratpt.end()) - { - return; - } - for (const Node& stratpt : it->second) - { - Trace("sygus-unif-rl-dt") - << "...adding value " << v - << " to decision tree of strategy point : " << stratpt << std::endl; - Assert(d_stratpt_to_dt.find(stratpt) != d_stratpt_to_dt.end()); - // Register new condition value - d_stratpt_to_dt[stratpt].addCondValue(v); - Trace("sygus-unif-rl-dt") << "...added\n"; - } + // we do not use notify enumeration + Assert(false); } Node SygusUnifRl::purifyLemma(Node n, @@ -362,11 +336,31 @@ Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind) return itd->second.buildSol(etis->d_cons); } -bool SygusUnifRl::usingUnif(Node f) +bool SygusUnifRl::usingUnif(Node f) const { return d_unif_candidates.find(f) != d_unif_candidates.end(); } +Node SygusUnifRl::getConditionForEvaluationPoint(Node e) const +{ + std::map<Node, DecisionTreeInfo>::const_iterator it = d_stratpt_to_dt.find(e); + Assert(it != d_stratpt_to_dt.end()); + return it->second.getConditionEnumerator(); +} + +void SygusUnifRl::setConditions(Node e, const std::vector<Node>& conds) +{ + std::map<Node, DecisionTreeInfo>::iterator it = d_stratpt_to_dt.find(e); + Assert(it != d_stratpt_to_dt.end()); + it->second.clearCondValues(); + /* TODO + for (const Node& c : conds) + { + it->second.addCondValue(c); + } + */ +} + std::vector<Node> SygusUnifRl::getEvalPointHeads(Node c) { std::map<Node, std::vector<Node>>::iterator it = d_cand_to_eval_hds.find(c); @@ -377,8 +371,7 @@ std::vector<Node> SygusUnifRl::getEvalPointHeads(Node c) return it->second; } -void SygusUnifRl::registerStrategy( - Node f, std::map<Node, std::vector<Node>>& strategy_lemmas) +void SygusUnifRl::registerStrategy(Node f, std::vector<Node>& enums) { if (Trace.isOn("sygus-unif-rl-strat")) { @@ -389,7 +382,7 @@ void SygusUnifRl::registerStrategy( Trace("sygus-unif-rl-strat") << "Register..." << std::endl; Node e = d_strategy[f].getRootEnumerator(); std::map<Node, std::map<NodeRole, bool>> visited; - registerStrategyNode(f, e, role_equal, visited, strategy_lemmas); + registerStrategyNode(f, e, role_equal, visited, enums); } void SygusUnifRl::registerStrategyNode( @@ -397,7 +390,7 @@ void SygusUnifRl::registerStrategyNode( Node e, NodeRole nrole, std::map<Node, std::map<NodeRole, bool>>& visited, - std::map<Node, std::vector<Node>>& strategy_lemmas) + std::vector<Node>& enums) { Trace("sygus-unif-rl-strat") << " register node " << e << std::endl; if (visited[e].find(nrole) != visited[e].end()) @@ -433,20 +426,25 @@ 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, j, strategy_lemmas); + registerConditionalEnumerator(f, e, cond, j); + // we will be using a strategy for e + enums.push_back(e); } } // TODO: recurse? for (std::pair<Node, NodeRole>& cec : etis->d_cenum) } } -void SygusUnifRl::registerConditionalEnumerator( - Node f, - Node e, - Node cond, - unsigned strategy_index, - std::map<Node, std::vector<Node>>& strategy_lemmas) +void SygusUnifRl::registerConditionalEnumerator(Node f, + Node e, + Node cond, + unsigned strategy_index) { + // only allow one decision tree per strategy point + if (d_stratpt_to_dt.find(e) != d_stratpt_to_dt.end()) + { + return; + } // we will do unification for this candidate d_unif_candidates.insert(f); // add to the list of all conditional enumerators @@ -455,23 +453,7 @@ void SygusUnifRl::registerConditionalEnumerator( { d_cond_enums.push_back(cond); d_cand_cenums[f].push_back(cond); - // register the conditional enumerator - d_tds->registerEnumerator(cond, f, d_parent, true); d_cenum_to_stratpt[cond].clear(); - // register lemmas to remove redundant operators from condition enumeration - std::map<const Node, std::vector<Node>>::iterator it = - strategy_lemmas.find(cond); - if (it != strategy_lemmas.end()) - { - for (const Node& lemma : it->second) - { - Trace("cegis-unif-enum-debug") - << "* Registering lemma to remove redundand operators for " << cond - << " --> " << lemma << "\n"; - d_qe->getOutputChannel().lemma(lemma); - } - strategy_lemmas.erase(cond); - } } // register that this strategy node has a decision tree construction d_stratpt_to_dt[e].initialize(cond, this, &d_strategy[f], strategy_index); @@ -500,6 +482,12 @@ void SygusUnifRl::DecisionTreeInfo::addPoint(Node f) d_pt_sep.d_trie.add(f, &d_pt_sep, d_conds.size()); } +void SygusUnifRl::DecisionTreeInfo::clearCondValues() +{ + // TODO + // d_conds.clear(); +} + void SygusUnifRl::DecisionTreeInfo::addCondValue(Node condv) { d_conds.push_back(condv); diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 09a226ae7..b5609e625 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -50,11 +50,13 @@ class SygusUnifRl : public SygusUnif ~SygusUnifRl(); /** initialize */ - void initialize(QuantifiersEngine* qe, - const std::vector<Node>& funs, - std::vector<Node>& enums, - std::map<Node, std::vector<Node>>& strategy_lemmas) override; - /** Notify enumeration */ + void initializeCandidate( + QuantifiersEngine* qe, + Node f, + std::vector<Node>& enums, + std::map<Node, std::vector<Node>>& strategy_lemmas) override; + + /** Notify enumeration (unused) */ void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override; /** Construct solution */ bool constructSolution(std::vector<Node>& sols) override; @@ -78,7 +80,19 @@ class SygusUnifRl : public SygusUnif * checked through wehether f has conditional or point enumerators (we use the * former) */ - bool usingUnif(Node f); + bool usingUnif(Node f) const; + /** get condition for evaluation point + * + * Returns the strategy point corresponding to the condition of the strategy + * point e. + */ + Node getConditionForEvaluationPoint(Node e) const; + /** set conditional enumerators + * + * This informs this class that the current set of conditions for evaluation + * point e is conds. + */ + void setConditions(Node e, const std::vector<Node>& conds); /** retrieve the head of evaluation points for candidate c, if any */ std::vector<Node> getEvalPointHeads(Node c); @@ -178,6 +192,8 @@ class SygusUnifRl : public SygusUnif unsigned strategy_index); /** adds the respective evaluation point of the head f */ void addPoint(Node f); + /** clears the condition values */ + void clearCondValues(); /** 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 */ @@ -201,6 +217,8 @@ class SygusUnifRl : public SygusUnif NodePair d_template; /** enumerated condition values */ std::vector<Node> d_conds; + /** get condition enumerator */ + Node getConditionEnumerator() const { return d_cond_enum; } private: /** @@ -262,41 +280,32 @@ class SygusUnifRl : public SygusUnif /** register strategy * * Initialize the above data for the relevant enumerators in the strategy tree - * of candidate variable f. - * - * Lemmas to remove redundant operators from enumerators of specific strategy - * points, if any, are retrived from strategy_lemmas. + * of candidate variable f. For each strategy point e which there is a + * decision tree strategy, we add e to enums. */ - void registerStrategy(Node f, - std::map<Node, std::vector<Node>>& strategy_lemmas); + void registerStrategy(Node f, std::vector<Node>& enums); /** register strategy node * * Called while traversing the strategy tree of f. The arguments e and nrole * indicate the current node in the tree we are traversing, and visited - * indicates the nodes we have already visited. - * - * Lemmas to remove redundant operators from enumerators of specific strategy - * points, if any, are retrived from strategy_lemmas. + * indicates the nodes we have already visited. If e has a decision tree + * strategy, it is added to enums. */ void registerStrategyNode(Node f, Node e, NodeRole nrole, std::map<Node, std::map<NodeRole, bool>>& visited, - std::map<Node, std::vector<Node>>& strategy_lemmas); + std::vector<Node>& enums); /** register conditional enumerator * * Registers that cond is a conditional enumerator for building a (recursive) * decision tree at strategy node e within the strategy tree of f. - * - * Lemmas to remove redundant operators from enumerators of specific strategy - * points, if any, are retrived from strategy_lemmas. */ void registerConditionalEnumerator( Node f, Node e, Node cond, - unsigned strategy_index, - std::map<Node, std::vector<Node>>& strategy_lemmas); + unsigned strategy_index); }; } /* CVC4::theory::quantifiers namespace */ |