From: Andrew Reynolds Date: Mon, 2 Apr 2018 22:50:31 +0000 (-0500) Subject: Make sygus unif utility use sygus unif strategies (#1732) X-Git-Tag: cvc5-1.0.0~5189 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bc6cb232c11d65f763844c2c9274444446aee26e;p=cvc5.git Make sygus unif utility use sygus unif strategies (#1732) --- diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index fb353a102..b45b602ec 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -70,9 +70,8 @@ class CegConjecture; * * (4) During search, the extension of quantifier-free datatypes procedure for * SyGuS datatypes may ask this class whether current candidates can be -* discarded based on -* inferring when two candidate solutions are equivalent up to examples. -* For example, the candidate solutions: +* discarded based on inferring when two candidate solutions are equivalent +* up to examples. For example, the candidate solutions: * f = \x ite( x < 0, x+1, x ) and f = \x x * are equivalent up to examples on the above conjecture, since they have the * same value on the points x = 0,5,6. Hence, we need only consider one of @@ -85,12 +84,11 @@ class CegConjecture; * CegConjecturePbe::getCandidateList(...), where this class returns the list * of active enumerators. * (6) The parent class subsequently calls -* CegConjecturePbe::constructValues(...), which -* informs this class that new values have been enumerated for active -* enumerators, as indicated by the current model. This call also requests -* that based on these +* CegConjecturePbe::constructValues(...), which informs this class that new +* values have been enumerated for active enumerators, as indicated by the +* current model. This call also requests that based on these * newly enumerated values, whether this class is now able to construct a -* solution based on the high-level strategy (stored in d_c_info). +* solution based on the high-level strategy (stored in d_sygus_unif). * * This class is not designed to work in incremental mode, since there is no way * to specify incremental problems in SyguS. @@ -248,18 +246,36 @@ class CegConjecturePbe : public SygusModule void collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol ); //--------------------------------- PBE search values - /** this class is an index of candidate solutions for PBE synthesis */ + /** + * This class is an index of candidate solutions for PBE synthesis and their + * (concrete) evaluation on the set of input examples. For example, if the + * set of input examples for (x,y) is (0,1), (1,3), then: + * term x is indexed by 0,1 + * term x+y is indexed by 1,4 + * term 0 is indexed by 0,0. + */ class PbeTrie { public: PbeTrie() {} ~PbeTrie() {} + /** the data for this node in the trie */ Node d_lazy_child; + /** the children for this node in the trie */ std::map d_children; + /** clear this trie */ void clear() { d_children.clear(); } + /** + * Add term b as a value enumerated for enumerator e to the trie. + * + * cpbe : reference to the parent pbe utility which stores the examples, + * index : the index of the example we are processing, + * ntotal : the total of the examples for enumerator e. + */ Node addPbeExample(TypeNode etn, Node e, Node b, CegConjecturePbe* cpbe, unsigned index, unsigned ntotal); private: + /** Helper function for above, called when we get the current example ex. */ Node addPbeExampleEval(TypeNode etn, Node e, Node b, std::vector& ex, CegConjecturePbe* cpbe, unsigned index, unsigned ntotal); diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 00658b6c4..27568fcce 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -479,15 +479,7 @@ void SygusUnif::initialize(QuantifiersEngine* qe, d_qe = qe; d_tds = qe->getTermDatabaseSygus(); - TypeNode tn = f.getType(); - d_cinfo.initialize(f); - // collect the enumerator types and form the strategy - collectEnumeratorTypes(tn, role_equal); - // add the enumerators - enums.insert( - enums.end(), d_cinfo.d_esym_list.begin(), d_cinfo.d_esym_list.end()); - // learn redundant ops - staticLearnRedundantOps(lemmas); + d_strategy.initialize(qe, f, enums, lemmas); } void SygusUnif::resetExamples() @@ -509,11 +501,8 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector& lemmas) Node c = d_candidate; Assert(!d_examples.empty()); Assert(d_examples.size() == d_examples_out.size()); - std::map::iterator it = d_einfo.find(e); - Assert(it != d_einfo.end()); - Assert( - std::find(it->second.d_enum_vals.begin(), it->second.d_enum_vals.end(), v) - == it->second.d_enum_vals.end()); + + EnumInfo& ei = d_strategy.getEnumInfo(e); // The explanation for why the current value should be excluded in future // iterations. Node exp_exc; @@ -531,8 +520,7 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector& lemmas) } // is it excluded for domain-specific reason? std::vector exp_exc_vec; - if (getExplanationForEnumeratorExclude( - e, v, base_results, it->second, exp_exc_vec)) + if (getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec)) { Assert(!exp_exc_vec.empty()); exp_exc = exp_exc_vec.size() == 1 @@ -544,19 +532,22 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector& lemmas) else { // notify all slaves - Assert(!it->second.d_enum_slave.empty()); + Assert(!ei.d_enum_slave.empty()); // explanation for why this value should be excluded - for (unsigned s = 0; s < it->second.d_enum_slave.size(); s++) + for (unsigned s = 0; s < ei.d_enum_slave.size(); s++) { - Node xs = it->second.d_enum_slave[s]; - std::map::iterator itv = d_einfo.find(xs); - Assert(itv != d_einfo.end()); + Node xs = ei.d_enum_slave[s]; + + EnumInfo& eiv = d_strategy.getEnumInfo(xs); + + EnumCache& ecv = d_ecache[xs]; + Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl; // bool prevIsCover = false; - if (itv->second.getRole() == enum_io) + if (eiv.getRole() == enum_io) { Trace("sygus-pbe-enum") << " IO-Eval of "; - // prevIsCover = itv->second.isFeasible(); + // prevIsCover = eiv.isFeasible(); } else { @@ -565,8 +556,8 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector& lemmas) Trace("sygus-pbe-enum") << xs << " : "; // evaluate all input/output examples std::vector results; - Node templ = itv->second.d_template; - TNode templ_var = itv->second.d_template_arg; + Node templ = eiv.d_template; + TNode templ_var = eiv.d_template_arg; std::map cond_vals; for (unsigned j = 0, size = base_results.size(); j < size; j++) { @@ -580,7 +571,7 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector& lemmas) Assert(res.isConst()); } Node resb; - if (itv->second.getRole() == enum_io) + if (eiv.getRole() == enum_io) { Node out = d_examples_out[j]; Assert(out.isConst()); @@ -605,7 +596,7 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector& lemmas) } } bool keep = false; - if (itv->second.getRole() == enum_io) + if (eiv.getRole() == enum_io) { // latter is the degenerate case of no examples if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty()) @@ -618,28 +609,25 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector& lemmas) Trace("sygus-pbe-enum") << " ...success, full solution added to PBE pool : " << d_tds->sygusToBuiltin(v) << std::endl; - if (!itv->second.isSolved()) + if (!ecv.isSolved()) { - itv->second.setSolved(v); + ecv.setSolved(v); // it subsumes everything - itv->second.d_term_trie.clear(); - itv->second.d_term_trie.addTerm(v, results, true, subsume); + ecv.d_term_trie.clear(); + ecv.d_term_trie.addTerm(v, results, true, subsume); } keep = true; } else { - Node val = - itv->second.d_term_trie.addTerm(v, results, true, subsume); + Node val = ecv.d_term_trie.addTerm(v, results, true, subsume); if (val == v) { Trace("sygus-pbe-enum") << " ...success"; if (!subsume.empty()) { - itv->second.d_enum_subsume.insert( - itv->second.d_enum_subsume.end(), - subsume.begin(), - subsume.end()); + ecv.d_enum_subsume.insert( + ecv.d_enum_subsume.end(), subsume.begin(), subsume.end()); Trace("sygus-pbe-enum") << " and subsumed " << subsume.size() << " terms"; } @@ -664,7 +652,7 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector& lemmas) else { // must be unique up to examples - Node val = itv->second.d_term_trie.addCond(v, results, true); + Node val = ecv.d_term_trie.addCond(v, results, true); if (val == v) { Trace("sygus-pbe-enum") << " ...success! add to PBE pool : " @@ -676,13 +664,13 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector& lemmas) Trace("sygus-pbe-enum") << " ...fail : term is not unique" << std::endl; } - d_cinfo.d_cond_count++; + d_cond_count++; } if (keep) { - // notify the parent to retry the build of PBE - d_cinfo.d_check_sol = true; - itv->second.addEnumValue(this, v, results); + // notify to retry the build of solution + d_check_sol = true; + ecv.addEnumValue(v, results); } } } @@ -702,27 +690,27 @@ void SygusUnif::notifyEnumeration(Node e, Node v, std::vector& lemmas) Node SygusUnif::constructSolution() { Node c = d_candidate; - if (!d_cinfo.d_solution.isNull()) + if (!d_solution.isNull()) { // already has a solution - return d_cinfo.d_solution; + return d_solution; } else { // only check if an enumerator updated - if (d_cinfo.d_check_sol) + if (d_check_sol) { - Trace("sygus-pbe") << "Construct solution, #iterations = " - << d_cinfo.d_cond_count << std::endl; - d_cinfo.d_check_sol = false; + Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count + << std::endl; + d_check_sol = false; // try multiple times if we have done multiple conditions, due to // non-determinism Node vc; - for (unsigned i = 0; i <= d_cinfo.d_cond_count; i++) + for (unsigned i = 0; i <= d_cond_count; i++) { Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl; - Node e = d_cinfo.getRootEnumerator(); + Node e = d_strategy.getRootEnumerator(); UnifContext x; x.initialize(this); Node vcc = constructSolution(e, role_equal, x, 1); @@ -741,7 +729,7 @@ Node SygusUnif::constructSolution() } if (!vc.isNull()) { - d_cinfo.d_solution = vc; + d_solution = vc; return vc; } Trace("sygus-pbe") << "...failed to solve." << std::endl; @@ -750,780 +738,54 @@ Node SygusUnif::constructSolution() } } -// ----------------------------- establishing enumeration types - -void SygusUnif::registerEnumerator(Node et, - TypeNode tn, - EnumRole enum_role, - bool inSearch) -{ - if (d_einfo.find(et) == d_einfo.end()) - { - Trace("sygus-unif-debug") - << "...register " << et << " for " - << static_cast(tn.toType()).getDatatype().getName(); - Trace("sygus-unif-debug") << ", role = " << enum_role - << ", in search = " << inSearch << std::endl; - d_einfo[et].initialize(enum_role); - // if we are actually enumerating this (could be a compound node in the - // strategy) - if (inSearch) - { - std::map::iterator itn = d_cinfo.d_search_enum.find(tn); - if (itn == d_cinfo.d_search_enum.end()) - { - // use this for the search - d_cinfo.d_search_enum[tn] = et; - d_cinfo.d_esym_list.push_back(et); - d_einfo[et].d_enum_slave.push_back(et); - } - else - { - Trace("sygus-unif-debug") - << "Make " << et << " a slave of " << itn->second << std::endl; - d_einfo[itn->second].d_enum_slave.push_back(et); - } - } - } -} - -void SygusUnif::collectEnumeratorTypes(TypeNode tn, NodeRole nrole) -{ - NodeManager* nm = NodeManager::currentNM(); - if (d_cinfo.d_tinfo.find(tn) == d_cinfo.d_tinfo.end()) - { - // register type - Trace("sygus-unif") << "Register enumerating type : " << tn << std::endl; - d_cinfo.initializeType(tn); - } - EnumTypeInfo& eti = d_cinfo.d_tinfo[tn]; - std::map::iterator itsn = eti.d_snodes.find(nrole); - if (itsn != eti.d_snodes.end()) - { - // already initialized - return; - } - StrategyNode& snode = eti.d_snodes[nrole]; - - // get the enumerator for this - EnumRole erole = getEnumeratorRoleForNodeRole(nrole); - - Node ee; - std::map::iterator iten = eti.d_enum.find(erole); - if (iten == eti.d_enum.end()) - { - ee = nm->mkSkolem("ee", tn); - eti.d_enum[erole] = ee; - Trace("sygus-unif-debug") - << "...enumerator " << ee << " for " - << static_cast(tn.toType()).getDatatype().getName() - << ", role = " << erole << std::endl; - } - else - { - ee = iten->second; - } - - // roles that we do not recurse on - if (nrole == role_ite_condition) - { - Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl; - registerEnumerator(ee, tn, erole, true); - return; - } - - // look at information on how we will construct solutions for this type - Assert(tn.isDatatype()); - const Datatype& dt = static_cast(tn.toType()).getDatatype(); - Assert(dt.isSygus()); - - std::map > cop_to_strat; - std::map cop_to_cindex; - std::map > cop_to_child_templ; - std::map > cop_to_child_templ_arg; - std::map > cop_to_carg_list; - std::map > cop_to_child_types; - std::map > cop_to_sks; - - // whether we will enumerate the current type - bool search_this = false; - for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) - { - Node cop = Node::fromExpr(dt[j].getConstructor()); - Node op = Node::fromExpr(dt[j].getSygusOp()); - Trace("sygus-unif-debug") << "--- Infer strategy from " << cop - << " with sygus op " << op << "..." << std::endl; - - // expand the evaluation to see if this constuctor induces a strategy - std::vector utchildren; - utchildren.push_back(cop); - std::vector sks; - std::vector sktns; - for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++) - { - Type t = dt[j][k].getRangeType(); - TypeNode ttn = TypeNode::fromType(t); - Node kv = nm->mkSkolem("ut", ttn); - sks.push_back(kv); - cop_to_sks[cop].push_back(kv); - sktns.push_back(ttn); - utchildren.push_back(kv); - } - Node ut = nm->mkNode(APPLY_CONSTRUCTOR, utchildren); - std::vector echildren; - echildren.push_back(Node::fromExpr(dt.getSygusEvaluationFunc())); - echildren.push_back(ut); - Node sbvl = Node::fromExpr(dt.getSygusVarList()); - for (const Node& sbv : sbvl) - { - echildren.push_back(sbv); - } - Node eut = nm->mkNode(APPLY_UF, echildren); - Trace("sygus-unif-debug2") - << " Test evaluation of " << eut << "..." << std::endl; - eut = d_qe->getTermDatabaseSygus()->unfold(eut); - Trace("sygus-unif-debug2") << " ...got " << eut; - Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl; - - // candidate strategy - if (eut.getKind() == ITE) - { - cop_to_strat[cop].push_back(strat_ITE); - } - else if (eut.getKind() == STRING_CONCAT) - { - if (nrole != role_string_suffix) - { - cop_to_strat[cop].push_back(strat_CONCAT_PREFIX); - } - if (nrole != role_string_prefix) - { - cop_to_strat[cop].push_back(strat_CONCAT_SUFFIX); - } - } - else if (dt[j].isSygusIdFunc()) - { - cop_to_strat[cop].push_back(strat_ID); - } - - // the kinds for which there is a strategy - if (cop_to_strat.find(cop) != cop_to_strat.end()) - { - // infer an injection from the arguments of the datatype - std::map templ_injection; - std::vector vs; - std::vector ss; - std::map templ_var_index; - for (unsigned k = 0, sksize = sks.size(); k < sksize; k++) - { - Assert(sks[k].getType().isDatatype()); - const Datatype& cdt = - static_cast(sks[k].getType().toType()).getDatatype(); - echildren[0] = Node::fromExpr(cdt.getSygusEvaluationFunc()); - echildren[1] = sks[k]; - Trace("sygus-unif-debug2") - << "...set eval dt to " << sks[k] << std::endl; - Node esk = nm->mkNode(APPLY_UF, echildren); - vs.push_back(esk); - Node tvar = nm->mkSkolem("templ", esk.getType()); - templ_var_index[tvar] = k; - Trace("sygus-unif-debug2") << "* template inference : looking for " - << tvar << " for arg " << k << std::endl; - ss.push_back(tvar); - Trace("sygus-unif-debug2") - << "* substitute : " << esk << " -> " << tvar << std::endl; - } - eut = eut.substitute(vs.begin(), vs.end(), ss.begin(), ss.end()); - Trace("sygus-unif-debug2") - << "Constructor " << j << ", base term is " << eut << std::endl; - std::map test_args; - if (dt[j].isSygusIdFunc()) - { - test_args[0] = eut; - } - else - { - for (unsigned k = 0, size = eut.getNumChildren(); k < size; k++) - { - test_args[k] = eut[k]; - } - } - - // TODO : prefix grouping prefix/suffix - bool isAssoc = TermUtil::isAssoc(eut.getKind()); - Trace("sygus-unif-debug2") - << eut.getKind() << " isAssoc = " << isAssoc << std::endl; - std::map > assoc_combine; - std::vector assoc_waiting; - int assoc_last_valid_index = -1; - for (std::pair& ta : test_args) - { - unsigned k = ta.first; - Node eut_c = ta.second; - // success if we can find a injection from args to sygus args - if (!inferTemplate(k, eut_c, templ_var_index, templ_injection)) - { - Trace("sygus-unif-debug") - << "...fail: could not find injection (range)." << std::endl; - cop_to_strat.erase(cop); - break; - } - std::map::iterator itti = templ_injection.find(k); - if (itti != templ_injection.end()) - { - // if associative, combine arguments if it is the same variable - if (isAssoc && assoc_last_valid_index >= 0 - && itti->second == templ_injection[assoc_last_valid_index]) - { - templ_injection.erase(k); - assoc_combine[assoc_last_valid_index].push_back(k); - } - else - { - assoc_last_valid_index = (int)k; - if (!assoc_waiting.empty()) - { - assoc_combine[k].insert(assoc_combine[k].end(), - assoc_waiting.begin(), - assoc_waiting.end()); - assoc_waiting.clear(); - } - assoc_combine[k].push_back(k); - } - } - else - { - // a ground argument - if (!isAssoc) - { - Trace("sygus-unif-debug") - << "...fail: could not find injection (functional)." - << std::endl; - cop_to_strat.erase(cop); - break; - } - else - { - if (assoc_last_valid_index >= 0) - { - assoc_combine[assoc_last_valid_index].push_back(k); - } - else - { - assoc_waiting.push_back(k); - } - } - } - } - if (cop_to_strat.find(cop) != cop_to_strat.end()) - { - // construct the templates - if (!assoc_waiting.empty()) - { - // could not find a way to fit some arguments into injection - cop_to_strat.erase(cop); - } - else - { - for (std::pair& ta : test_args) - { - unsigned k = ta.first; - Trace("sygus-unif-debug2") - << "- processing argument " << k << "..." << std::endl; - if (templ_injection.find(k) != templ_injection.end()) - { - unsigned sk_index = templ_injection[k]; - if (std::find(cop_to_carg_list[cop].begin(), - cop_to_carg_list[cop].end(), - sk_index) - == cop_to_carg_list[cop].end()) - { - cop_to_carg_list[cop].push_back(sk_index); - } - else - { - Trace("sygus-unif-debug") - << "...fail: duplicate argument used" << std::endl; - cop_to_strat.erase(cop); - break; - } - // also store the template information, if necessary - Node teut; - if (isAssoc) - { - std::vector& ac = assoc_combine[k]; - Assert(!ac.empty()); - std::vector children; - for (unsigned ack = 0, size_ac = ac.size(); ack < size_ac; - ack++) - { - children.push_back(eut[ac[ack]]); - } - teut = children.size() == 1 - ? children[0] - : nm->mkNode(eut.getKind(), children); - teut = Rewriter::rewrite(teut); - } - else - { - teut = ta.second; - } - - if (!teut.isVar()) - { - cop_to_child_templ[cop][k] = teut; - cop_to_child_templ_arg[cop][k] = ss[sk_index]; - Trace("sygus-unif-debug") - << " Arg " << k << " (template : " << teut << " arg " - << ss[sk_index] << "), index " << sk_index << std::endl; - } - else - { - Trace("sygus-unif-debug") - << " Arg " << k << ", index " << sk_index << std::endl; - Assert(teut == ss[sk_index]); - } - } - else - { - Assert(isAssoc); - } - } - } - } - } - if (cop_to_strat.find(cop) == cop_to_strat.end()) - { - Trace("sygus-unif") << "...constructor " << cop - << " does not correspond to a strategy." << std::endl; - search_this = true; - } - else - { - Trace("sygus-unif") << "-> constructor " << cop - << " matches strategy for " << eut.getKind() << "..." - << std::endl; - // collect children types - for (unsigned k = 0, size = cop_to_carg_list[cop].size(); k < size; k++) - { - TypeNode tn = sktns[cop_to_carg_list[cop][k]]; - Trace("sygus-unif-debug") - << " Child type " << k << " : " - << static_cast(tn.toType()).getDatatype().getName() - << std::endl; - cop_to_child_types[cop].push_back(tn); - } - } - } - - // check whether we should also enumerate the current type - Trace("sygus-unif-debug2") << " register this enumerator..." << std::endl; - registerEnumerator(ee, tn, erole, search_this); - - if (cop_to_strat.empty()) - { - Trace("sygus-unif") << "...consider " << dt.getName() << " a basic type" - << std::endl; - } - else - { - for (std::pair >& cstr : cop_to_strat) - { - Node cop = cstr.first; - Trace("sygus-unif-debug") - << "Constructor " << cop << " has " << cstr.second.size() - << " strategies..." << std::endl; - for (unsigned s = 0, ssize = cstr.second.size(); s < ssize; s++) - { - EnumTypeInfoStrat* cons_strat = new EnumTypeInfoStrat; - StrategyType strat = cstr.second[s]; - - cons_strat->d_this = strat; - cons_strat->d_cons = cop; - Trace("sygus-unif-debug") - << "Process strategy #" << s << " for operator : " << cop << " : " - << strat << std::endl; - Assert(cop_to_child_types.find(cop) != cop_to_child_types.end()); - std::vector& childTypes = cop_to_child_types[cop]; - Assert(cop_to_carg_list.find(cop) != cop_to_carg_list.end()); - std::vector& cargList = cop_to_carg_list[cop]; - - std::vector sol_templ_children; - sol_templ_children.resize(cop_to_sks[cop].size()); - - for (unsigned j = 0, csize = childTypes.size(); j < csize; j++) - { - // calculate if we should allocate a new enumerator : should be true - // if we have a new role - NodeRole nrole_c = nrole; - if (strat == strat_ITE) - { - if (j == 0) - { - nrole_c = role_ite_condition; - } - } - else if (strat == strat_CONCAT_PREFIX) - { - if ((j + 1) < childTypes.size()) - { - nrole_c = role_string_prefix; - } - } - else if (strat == strat_CONCAT_SUFFIX) - { - if (j > 0) - { - nrole_c = role_string_suffix; - } - } - // in all other cases, role is same as parent - - // register the child type - TypeNode ct = childTypes[j]; - Node csk = cop_to_sks[cop][cargList[j]]; - cons_strat->d_sol_templ_args.push_back(csk); - sol_templ_children[cargList[j]] = csk; - - EnumRole erole_c = getEnumeratorRoleForNodeRole(nrole_c); - // make the enumerator - Node et; - if (cop_to_child_templ[cop].find(j) != cop_to_child_templ[cop].end()) - { - // it is templated, allocate a fresh variable - et = nm->mkSkolem("et", ct); - Trace("sygus-unif-debug") - << "...enumerate " << et << " of type " - << ((DatatypeType)ct.toType()).getDatatype().getName(); - Trace("sygus-unif-debug") << " for arg " << j << " of " - << static_cast(tn.toType()) - .getDatatype() - .getName() - << std::endl; - registerEnumerator(et, ct, erole_c, true); - d_einfo[et].d_template = cop_to_child_templ[cop][j]; - d_einfo[et].d_template_arg = cop_to_child_templ_arg[cop][j]; - Assert(!d_einfo[et].d_template.isNull()); - Assert(!d_einfo[et].d_template_arg.isNull()); - } - else - { - Trace("sygus-unif-debug") - << "...child type enumerate " - << ((DatatypeType)ct.toType()).getDatatype().getName() - << ", node role = " << nrole_c << std::endl; - collectEnumeratorTypes(ct, nrole_c); - // otherwise use the previous - Assert(d_cinfo.d_tinfo[ct].d_enum.find(erole_c) - != d_cinfo.d_tinfo[ct].d_enum.end()); - et = d_cinfo.d_tinfo[ct].d_enum[erole_c]; - } - Trace("sygus-unif-debug") - << "Register child enumerator " << et << ", arg " << j << " of " - << cop << ", role = " << erole_c << std::endl; - Assert(!et.isNull()); - cons_strat->d_cenum.push_back(std::pair(et, nrole_c)); - } - // children that are unused in the strategy can be arbitrary - for (unsigned j = 0, stsize = sol_templ_children.size(); j < stsize; - j++) - { - if (sol_templ_children[j].isNull()) - { - sol_templ_children[j] = cop_to_sks[cop][j].getType().mkGroundTerm(); - } - } - sol_templ_children.insert(sol_templ_children.begin(), cop); - cons_strat->d_sol_templ = - nm->mkNode(APPLY_CONSTRUCTOR, sol_templ_children); - if (strat == strat_CONCAT_SUFFIX) - { - std::reverse(cons_strat->d_cenum.begin(), cons_strat->d_cenum.end()); - std::reverse(cons_strat->d_sol_templ_args.begin(), - cons_strat->d_sol_templ_args.end()); - } - if (Trace.isOn("sygus-unif")) - { - Trace("sygus-unif") << "Initialized strategy " << strat; - Trace("sygus-unif") - << " for " - << static_cast(tn.toType()).getDatatype().getName() - << ", operator " << cop; - Trace("sygus-unif") << ", #children = " << cons_strat->d_cenum.size() - << ", solution template = (lambda ( "; - for (const Node& targ : cons_strat->d_sol_templ_args) - { - Trace("sygus-unif") << targ << " "; - } - Trace("sygus-unif") << ") " << cons_strat->d_sol_templ << ")"; - Trace("sygus-unif") << std::endl; - } - // make the strategy - snode.d_strats.push_back(cons_strat); - } - } - } -} - -bool SygusUnif::inferTemplate(unsigned k, - Node n, - std::map& templ_var_index, - std::map& templ_injection) -{ - if (n.getNumChildren() == 0) - { - std::map::iterator itt = templ_var_index.find(n); - if (itt != templ_var_index.end()) - { - unsigned kk = itt->second; - std::map::iterator itti = templ_injection.find(k); - if (itti == templ_injection.end()) - { - Trace("sygus-unif-debug") - << "...set template injection " << k << " -> " << kk << std::endl; - templ_injection[k] = kk; - } - else if (itti->second != kk) - { - // two distinct variables in this term, we fail - return false; - } - } - return true; - } - else - { - for (unsigned i = 0; i < n.getNumChildren(); i++) - { - if (!inferTemplate(k, n[i], templ_var_index, templ_injection)) - { - return false; - } - } - } - return true; -} - -void SygusUnif::staticLearnRedundantOps(std::vector& lemmas) -{ - for (unsigned i = 0; i < d_cinfo.d_esym_list.size(); i++) - { - Node e = d_cinfo.d_esym_list[i]; - std::map::iterator itn = d_einfo.find(e); - Assert(itn != d_einfo.end()); - // see if there is anything we can eliminate - Trace("sygus-unif") - << "* Search enumerator #" << i << " : type " - << ((DatatypeType)e.getType().toType()).getDatatype().getName() - << " : "; - Trace("sygus-unif") << e << " has " << itn->second.d_enum_slave.size() - << " slaves:" << std::endl; - for (unsigned j = 0; j < itn->second.d_enum_slave.size(); j++) - { - Node es = itn->second.d_enum_slave[j]; - std::map::iterator itns = d_einfo.find(es); - Assert(itns != d_einfo.end()); - Trace("sygus-unif") << " " << es << ", role = " << itns->second.getRole() - << std::endl; - } - } - Trace("sygus-unif") << std::endl; - Trace("sygus-unif") << "Strategy for candidate " << d_candidate - << " is : " << std::endl; - std::map > visited; - std::map > needs_cons; - staticLearnRedundantOps( - d_cinfo.getRootEnumerator(), role_equal, visited, needs_cons, 0, false); - // now, check the needs_cons map - for (std::pair >& nce : needs_cons) - { - Node em = nce.first; - const Datatype& dt = - static_cast(em.getType().toType()).getDatatype(); - for (std::pair& nc : nce.second) - { - Assert(nc.first < dt.getNumConstructors()); - if (!nc.second) - { - Node tst = - datatypes::DatatypesRewriter::mkTester(em, nc.first, dt).negate(); - if (std::find(lemmas.begin(), lemmas.end(), tst) == lemmas.end()) - { - Trace("sygus-unif") - << "...can exclude based on : " << tst << std::endl; - lemmas.push_back(tst); - } - } - } - } -} - -void SygusUnif::staticLearnRedundantOps( - Node e, - NodeRole nrole, - std::map >& visited, - std::map >& needs_cons, - int ind, - bool isCond) -{ - std::map::iterator itn = d_einfo.find(e); - Assert(itn != d_einfo.end()); - - if (visited[e].find(nrole) == visited[e].end() - || (isCond && !itn->second.isConditional())) - { - visited[e][nrole] = true; - // if conditional - if (isCond) - { - itn->second.setConditional(); - } - indent("sygus-unif", ind); - Trace("sygus-unif") << e << " :: node role : " << nrole; - Trace("sygus-unif") - << ", type : " - << ((DatatypeType)e.getType().toType()).getDatatype().getName(); - if (isCond) - { - Trace("sygus-unif") << ", conditional"; - } - Trace("sygus-unif") << ", enum role : " << itn->second.getRole(); - - if (itn->second.isTemplated()) - { - Trace("sygus-unif") << ", templated : (lambda " - << itn->second.d_template_arg << " " - << itn->second.d_template << ")" << std::endl; - } - else - { - Trace("sygus-unif") << std::endl; - TypeNode etn = e.getType(); - - // enumerator type info - std::map::iterator itt = - d_cinfo.d_tinfo.find(etn); - Assert(itt != d_cinfo.d_tinfo.end()); - EnumTypeInfo& tinfo = itt->second; - - // strategy info - std::map::iterator itsn = - tinfo.d_snodes.find(nrole); - Assert(itsn != tinfo.d_snodes.end()); - StrategyNode& snode = itsn->second; - - if (snode.d_strats.empty()) - { - return; - } - std::map needs_cons_curr; - // various strategies - for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) - { - EnumTypeInfoStrat* etis = snode.d_strats[j]; - StrategyType strat = etis->d_this; - bool newIsCond = isCond || strat == strat_ITE; - indent("sygus-unif", ind + 1); - Trace("sygus-unif") << "Strategy : " << strat - << ", from cons : " << etis->d_cons << std::endl; - int cindex = Datatype::indexOf(etis->d_cons.toExpr()); - Assert(cindex != -1); - needs_cons_curr[static_cast(cindex)] = false; - for (std::pair& cec : etis->d_cenum) - { - // recurse - staticLearnRedundantOps( - cec.first, cec.second, visited, needs_cons, ind + 2, newIsCond); - } - } - // get the master enumerator for the type of this enumerator - std::map::iterator itse = d_cinfo.d_search_enum.find(etn); - if (itse == d_cinfo.d_search_enum.end()) - { - return; - } - Node em = itse->second; - Assert(!em.isNull()); - // get the current datatype - const Datatype& dt = - static_cast(etn.toType()).getDatatype(); - // all constructors that are not a part of a strategy are needed - for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) - { - if (needs_cons_curr.find(j) == needs_cons_curr.end()) - { - needs_cons_curr[j] = true; - } - } - // update the constructors that the master enumerator needs - if (needs_cons.find(em) == needs_cons.end()) - { - needs_cons[em] = needs_cons_curr; - } - else - { - for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) - { - needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j]; - } - } - } - } - else - { - indent("sygus-unif", ind); - Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl; - } -} - // ------------------------------------ solution construction from enumeration -bool SygusUnif::useStrContainsEnumeratorExclude(Node x, EnumInfo& ei) +bool SygusUnif::useStrContainsEnumeratorExclude(Node e) { - TypeNode xbt = d_tds->sygusToBuiltinType(x.getType()); + TypeNode xbt = d_tds->sygusToBuiltinType(e.getType()); if (xbt.isString()) { - std::map::iterator itx = d_use_str_contains_eexc.find(x); + std::map::iterator itx = d_use_str_contains_eexc.find(e); if (itx != d_use_str_contains_eexc.end()) { return itx->second; } - Trace("sygus-pbe-enum-debug") - << "Is " << x << " is str.contains exclusion?" << std::endl; - d_use_str_contains_eexc[x] = true; + Trace("sygus-pbe-enum-debug") << "Is " << e << " is str.contains exclusion?" + << std::endl; + d_use_str_contains_eexc[e] = true; + EnumInfo& ei = d_strategy.getEnumInfo(e); for (const Node& sn : ei.d_enum_slave) { - std::map::iterator itv = d_einfo.find(sn); - EnumRole er = itv->second.getRole(); + EnumInfo& eis = d_strategy.getEnumInfo(sn); + EnumRole er = eis.getRole(); if (er != enum_io && er != enum_concat_term) { Trace("sygus-pbe-enum-debug") << " incompatible slave : " << sn << ", role = " << er << std::endl; - d_use_str_contains_eexc[x] = false; + d_use_str_contains_eexc[e] = false; return false; } - if (itv->second.isConditional()) + if (eis.isConditional()) { Trace("sygus-pbe-enum-debug") << " conditional slave : " << sn << std::endl; - d_use_str_contains_eexc[x] = false; + d_use_str_contains_eexc[e] = false; return false; } } Trace("sygus-pbe-enum-debug") << "...can use str.contains exclusion." << std::endl; - return d_use_str_contains_eexc[x]; + return d_use_str_contains_eexc[e]; } return false; } -bool SygusUnif::getExplanationForEnumeratorExclude(Node x, +bool SygusUnif::getExplanationForEnumeratorExclude(Node e, Node v, std::vector& results, - EnumInfo& ei, std::vector& exp) { - if (useStrContainsEnumeratorExclude(x, ei)) + if (useStrContainsEnumeratorExclude(e)) { NodeManager* nm = NodeManager::currentNM(); // This check whether the example evaluates to something that is larger than @@ -1536,9 +798,9 @@ bool SygusUnif::getExplanationForEnumeratorExclude(Node x, } // check if all examples had longer length that the output Assert(d_examples_out.size() == results.size()); - Trace("sygus-pbe-cterm-debug") - << "Check enumerator exclusion for " << x << " -> " - << d_tds->sygusToBuiltin(v) << " based on str.contains." << std::endl; + Trace("sygus-pbe-cterm-debug") << "Check enumerator exclusion for " << e + << " -> " << d_tds->sygusToBuiltin(v) + << " based on str.contains." << std::endl; std::vector cmp_indices; for (unsigned i = 0, size = results.size(); i < size; i++) { @@ -1562,9 +824,9 @@ bool SygusUnif::getExplanationForEnumeratorExclude(Node x, { // we check invariance with respect to a negative contains test NegContainsSygusInvarianceTest ncset; - ncset.init(x, d_examples, d_examples_out, cmp_indices); + ncset.init(e, d_examples, d_examples_out, cmp_indices); // construct the generalized explanation - d_tds->getExplain()->getExplanationFor(x, v, exp, ncset); + d_tds->getExplain()->getExplanationFor(e, v, exp, ncset); Trace("sygus-pbe-cterm") << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin(v) << " due to negative containment." << std::endl; @@ -1574,9 +836,7 @@ bool SygusUnif::getExplanationForEnumeratorExclude(Node x, return false; } -void SygusUnif::EnumInfo::addEnumValue(SygusUnif* pbe, - Node v, - std::vector& results) +void SygusUnif::EnumCache::addEnumValue(Node v, std::vector& results) { // should not have been enumerated before Assert(d_enum_val_to_index.find(v) == d_enum_val_to_index.end()); @@ -1585,29 +845,6 @@ void SygusUnif::EnumInfo::addEnumValue(SygusUnif* pbe, d_enum_vals_res.push_back(results); } -void SygusUnif::EnumInfo::initialize(EnumRole role) { d_role = role; } - -void SygusUnif::EnumInfo::setSolved(Node slv) { d_enum_solved = slv; } - -void SygusUnif::CandidateInfo::initialize(Node c) -{ - d_this_candidate = c; - d_root = c.getType(); -} - -void SygusUnif::CandidateInfo::initializeType(TypeNode tn) -{ - d_tinfo[tn].d_this_type = tn; - d_tinfo[tn].d_parent = this; -} - -Node SygusUnif::CandidateInfo::getRootEnumerator() -{ - std::map::iterator it = d_tinfo[d_root].d_enum.find(enum_io); - Assert(it != d_tinfo[d_root].d_enum.end()); - return it->second; -} - Node SygusUnif::constructBestSolvedTerm(std::vector& solved, UnifContext& x) { @@ -1685,24 +922,22 @@ Node SygusUnif::constructSolution(Node e, Trace("sygus-pbe-dt-debug") << std::endl; } // enumerator type info - std::map::iterator itt = d_cinfo.d_tinfo.find(etn); - Assert(itt != d_cinfo.d_tinfo.end()); - EnumTypeInfo& tinfo = itt->second; + EnumTypeInfo& tinfo = d_strategy.getEnumTypeInfo(etn); // get the enumerator information - std::map::iterator itn = d_einfo.find(e); - Assert(itn != d_einfo.end()); - EnumInfo& einfo = itn->second; + EnumInfo& einfo = d_strategy.getEnumInfo(e); + + EnumCache& ecache = d_ecache[e]; Node ret_dt; if (nrole == role_equal) { if (!x.isReturnValueModified()) { - if (einfo.isSolved()) + if (ecache.isSolved()) { // this type has a complete solution - ret_dt = einfo.getSolved(); + ret_dt = ecache.getSolved(); indent("sygus-pbe-dt", ind); Trace("sygus-pbe-dt") << "return PBE: success : solved " << d_tds->sygusToBuiltin(ret_dt) << std::endl; @@ -1712,7 +947,7 @@ Node SygusUnif::constructSolution(Node e, { // could be conditionally solved std::vector subsumed_by; - einfo.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by); + ecache.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by); if (!subsumed_by.empty()) { ret_dt = constructBestSolvedTerm(subsumed_by, x); @@ -1734,37 +969,25 @@ Node SygusUnif::constructSolution(Node e, { // check if a current value that closes all examples // get the term enumerator for this type - bool success = true; - std::map::iterator itet; std::map::iterator itnt = tinfo.d_enum.find(enum_concat_term); - if (itnt != itt->second.d_enum.end()) + if (itnt != tinfo.d_enum.end()) { Node et = itnt->second; - itet = d_einfo.find(et); - Assert(itet != d_einfo.end()); - } - else - { - success = false; - } - if (success) - { + + EnumCache& ecachet = d_ecache[et]; // get the current examples std::vector ex_vals; x.getCurrentStrings(this, d_examples_out, ex_vals); - Assert(itn->second.d_enum_vals.size() - == itn->second.d_enum_vals_res.size()); + Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size()); // test each example in the term enumerator for the type std::vector str_solved; - for (unsigned i = 0, size = itet->second.d_enum_vals.size(); i < size; - i++) + for (unsigned i = 0, size = ecachet.d_enum_vals.size(); i < size; i++) { - if (x.isStringSolved( - this, ex_vals, itet->second.d_enum_vals_res[i])) + if (x.isStringSolved(this, ex_vals, ecachet.d_enum_vals_res[i])) { - str_solved.push_back(itet->second.d_enum_vals[i]); + str_solved.push_back(ecachet.d_enum_vals[i]); } } if (!str_solved.empty()) @@ -1809,21 +1032,21 @@ Node SygusUnif::constructSolution(Node e, // check if there is a value for which is a prefix/suffix of all active // examples - Assert(einfo.d_enum_vals.size() == einfo.d_enum_vals_res.size()); + Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size()); - for (unsigned i = 0, size = einfo.d_enum_vals.size(); i < size; i++) + for (unsigned i = 0, size = ecache.d_enum_vals.size(); i < size; i++) { - Node val_t = einfo.d_enum_vals[i]; + Node val_t = ecache.d_enum_vals[i]; Assert(incr.find(val_t) == incr.end()); indent("sygus-pbe-dt-debug", ind); Trace("sygus-pbe-dt-debug") << "increment string values : " << val_t << " : "; - Assert(einfo.d_enum_vals_res[i].size() == d_examples_out.size()); + Assert(ecache.d_enum_vals_res[i].size() == d_examples_out.size()); unsigned tot = 0; bool exsuccess = x.getStringIncrement(this, isPrefix, ex_vals, - einfo.d_enum_vals_res[i], + ecache.d_enum_vals_res[i], incr[val_t], tot); if (!exsuccess) @@ -1890,7 +1113,7 @@ Node SygusUnif::constructSolution(Node e, // get an eligible strategy index unsigned sindex = 0; while (sindex < snode.d_strats.size() - && !snode.d_strats[sindex]->isValid(this, x)) + && !snode.d_strats[sindex]->isValid(&x)) { sindex++; } @@ -1940,16 +1163,14 @@ Node SygusUnif::constructSolution(Node e, std::vector prev; if (strat == strat_ITE && sc > 0) { - std::map::iterator itnc = - d_einfo.find(split_cond_enum); - Assert(itnc != d_einfo.end()); + EnumCache& ecache_cond = d_ecache[split_cond_enum]; Assert(split_cond_res_index >= 0); Assert(split_cond_res_index - < (int)itnc->second.d_enum_vals_res.size()); + < (int)ecache_cond.d_enum_vals_res.size()); prev = x.d_vals; bool ret = x.updateContext( this, - itnc->second.d_enum_vals_res[split_cond_res_index], + ecache_cond.d_enum_vals_res[split_cond_res_index], sc == 1); AlwaysAssert(ret); } @@ -1959,10 +1180,7 @@ Node SygusUnif::constructSolution(Node e, { Node ce = cenum.first; - // register the condition enumerator - std::map::iterator itnc = d_einfo.find(ce); - Assert(itnc != d_einfo.end()); - EnumInfo& einfo_child = itnc->second; + EnumCache& ecache_child = d_ecache[ce]; // only used if the return value is not modified if (!x.isReturnValueModified()) @@ -1973,25 +1191,24 @@ Node SygusUnif::constructSolution(Node e, << " reg : PBE: Look for direct solutions for conditional " "enumerator " << ce << " ... " << std::endl; - Assert(einfo_child.d_enum_vals.size() - == einfo_child.d_enum_vals_res.size()); + Assert(ecache_child.d_enum_vals.size() + == ecache_child.d_enum_vals_res.size()); for (unsigned i = 1; i <= 2; i++) { std::pair& te_pair = etis->d_cenum[i]; Node te = te_pair.first; - std::map::iterator itnt = d_einfo.find(te); - Assert(itnt != d_einfo.end()); + EnumCache& ecache_te = d_ecache[te]; bool branch_pol = (i == 1); // for each condition, get terms that satisfy it in this // branch - for (unsigned k = 0, size = einfo_child.d_enum_vals.size(); + for (unsigned k = 0, size = ecache_child.d_enum_vals.size(); k < size; k++) { - Node cond = einfo_child.d_enum_vals[k]; + Node cond = ecache_child.d_enum_vals[k]; std::vector solved; - itnt->second.d_term_trie.getSubsumedBy( - einfo_child.d_enum_vals_res[k], branch_pol, solved); + ecache_te.d_term_trie.getSubsumedBy( + ecache_child.d_enum_vals_res[k], branch_pol, solved); Trace("sygus-pbe-dt-debug2") << " reg : PBE: " << d_tds->sygusToBuiltin(cond) << " has " << solved.size() << " solutions in branch " @@ -2016,7 +1233,7 @@ Node SygusUnif::constructSolution(Node e, // distinguishable std::map > possible_cond; std::map solved_cond; // stores branch - einfo_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond); + ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond); std::map >::iterator itpc = possible_cond.find(0); @@ -2101,13 +1318,13 @@ Node SygusUnif::constructSolution(Node e, } if (!rec_c.isNull()) { - Assert(einfo_child.d_enum_val_to_index.find(rec_c) - != einfo_child.d_enum_val_to_index.end()); - split_cond_res_index = einfo_child.d_enum_val_to_index[rec_c]; + Assert(ecache_child.d_enum_val_to_index.find(rec_c) + != ecache_child.d_enum_val_to_index.end()); + split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c]; split_cond_enum = ce; Assert(split_cond_res_index >= 0); Assert(split_cond_res_index - < (int)einfo_child.d_enum_vals_res.size()); + < (int)ecache_child.d_enum_vals_res.size()); } } else @@ -2163,27 +1380,6 @@ Node SygusUnif::constructSolution(Node e, return ret_dt; } -bool SygusUnif::EnumTypeInfoStrat::isValid(SygusUnif* pbe, UnifContext& x) -{ - if ((x.d_has_string_pos == role_string_prefix - && d_this == strat_CONCAT_SUFFIX) - || (x.d_has_string_pos == role_string_suffix - && d_this == strat_CONCAT_PREFIX)) - { - return false; - } - return true; -} - -SygusUnif::StrategyNode::~StrategyNode() -{ - for (unsigned j = 0, size = d_strats.size(); j < size; j++) - { - delete d_strats[j]; - } - d_strats.clear(); -} - void SygusUnif::indent(const char* c, int ind) { if (Trace.isOn(c)) diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 9bb321a09..4e7806bf0 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -265,11 +265,11 @@ class SubsumeTrie * * This class maintains: * (1) A "strategy tree" based on the syntactic restrictions for f that is - * constructed during initialize, + * constructed during initialize (d_strategy), * (2) A set of input/output examples that are the specification for f. This * can be updated via calls to resetExmaples/addExamples, - * (3) A set of terms that have been enumerated for enumerators. This can be - * updated via calls to notifyEnumeration. + * (3) A set of terms that have been enumerated for enumerators (d_ecache). This + * can be updated via calls to notifyEnumeration. * * Based on the above, solutions can be constructed via calls to * constructSolution. @@ -353,72 +353,25 @@ class SygusUnif bool pol = true); //-----------------------end debug printing - //------------------------------ representation of a enumeration strategy /** * This class stores information regarding an enumerator, including: - * - Information regarding the role of this enumerator (see EnumRole), its - * parent, whether it is templated, its slave enumerators, and so on, and - * - A database of values that have been enumerated for this enumerator. - * - * We say an enumerator is a master enumerator if it is the variable that - * we use to enumerate values for its sort. Master enumerators may have - * (possibly multiple) slave enumerators, stored in d_enum_slave. We make - * the first enumerator for each type a master enumerator, and any additional - * ones slaves of it. + * a database of values that have been enumerated for this enumerator. */ - class EnumInfo + class EnumCache { public: - EnumInfo() : d_role(enum_io), d_is_conditional(false) {} - /** initialize this class - * - * c is the parent function-to-synthesize - * role is the "role" the enumerator plays in the high-level strategy, - * which is one of enum_* above. - */ - void initialize(EnumRole role); - /** is this enumerator associated with a template? */ - bool isTemplated() { return !d_template.isNull(); } - /** set conditional - * - * This flag is set to true if this enumerator may not apply to all - * input/output examples. For example, if this enumerator is used - * as an output value beneath a conditional in an instance of strat_ITE, - * then this enumerator is conditional. - */ - void setConditional() { d_is_conditional = true; } - /** is conditional */ - bool isConditional() { return d_is_conditional; } - /** get the role of this enumerator */ - EnumRole getRole() { return d_role; } - /** enumerator template - * - * If d_template non-null, enumerated values V are immediately transformed to - * d_template { d_template_arg -> V }. - */ - Node d_template; - Node d_template_arg; - /** - * Slave enumerators of this enumerator. These are other enumerators that - * have the same type, but a different role in the strategy tree. We - * generally - * only use one enumerator per type, and hence these slaves are notified when - * values are enumerated for this enumerator. - */ - std::vector d_enum_slave; - - //---------------------------enumerated values + EnumCache() {} /** * Notify this class that the term v has been enumerated for this enumerator. * Its evaluation under the set of examples in pbe are stored in results. */ - void addEnumValue(SygusUnif* pbe, Node v, std::vector& results); + void addEnumValue(Node v, std::vector& results); /** * Notify this class that slv is the complete solution to the synthesis * conjecture. This occurs rarely, for instance, when during an ITE strategy * we find that a single enumerated term covers all examples. */ - void setSolved(Node slv); + void setSolved(Node slv) { d_enum_solved = slv; } /** Have we been notified that a complete solution exists? */ bool isSolved() { return !d_enum_solved.isNull(); } /** Get the complete solution to the synthesis conjecture. */ @@ -444,174 +397,61 @@ class SygusUnif * enum_concat_term). */ SubsumeTrie d_term_trie; - //---------------------------end enumerated values private: /** * Whether an enumerated value for this conjecture has solved the entire * conjecture. */ Node d_enum_solved; - /** the role of this enumerator (one of enum_* above). */ - EnumRole d_role; - /** is this enumerator conditional */ - bool d_is_conditional; }; /** maps enumerators to the information above */ - std::map d_einfo; + std::map d_ecache; - class CandidateInfo; - class EnumTypeInfoStrat; - - /** represents a node in the strategy graph - * - * It contains a list of possible strategies which are tried during calls - * to constructSolution. - */ - class StrategyNode - { - public: - StrategyNode() {} - ~StrategyNode(); - /** the set of strategies to try at this node in the strategy graph */ - std::vector d_strats; - }; - - /** stores enumerators and strategies for a SyGuS datatype type */ - class EnumTypeInfo - { - public: - EnumTypeInfo() : d_parent(NULL) {} - /** the parent candidate info (see below) */ - CandidateInfo* d_parent; - /** the type that this information is for */ - TypeNode d_this_type; - /** map from enum roles to enumerators for this type */ - std::map d_enum; - /** map from node roles to strategy nodes */ - std::map d_snodes; - }; - - /** stores strategy and enumeration information for a function-to-synthesize + /** + * Whether we will try to construct solution on the next call to + * constructSolution. This flag is set to true when we successfully + * register a new value for an enumerator. */ - class CandidateInfo - { - public: - CandidateInfo() : d_check_sol(false), d_cond_count(0) {} - Node d_this_candidate; - /** - * The root sygus datatype for the function-to-synthesize, - * which encodes the overall syntactic restrictions on the space - * of solutions. - */ - TypeNode d_root; - /** Info for sygus datatype type occurring in a field of d_root */ - std::map d_tinfo; - /** list of all enumerators for the function-to-synthesize */ - std::vector d_esym_list; - /** - * Maps sygus datatypes to their search enumerator. This is the (single) - * enumerator of that type that we enumerate values for. - */ - std::map d_search_enum; - bool d_check_sol; - unsigned d_cond_count; - Node d_solution; - void initialize(Node c); - void initializeType(TypeNode tn); - Node getRootEnumerator(); - }; + bool d_check_sol; + /** The number of values we have enumerated for all enumerators. */ + unsigned d_cond_count; + /** The solution for the function of this class, if one has been found */ + Node d_solution; /** the candidate for this class */ Node d_candidate; /** maps a function-to-synthesize to the above information */ - CandidateInfo d_cinfo; + SygusUnifStrategy d_strategy; - //------------------------------ representation of an enumeration strategy /** domain-specific enumerator exclusion techniques * - * Returns true if the value v for x can be excluded based on a + * Returns true if the value v for e can be excluded based on a * domain-specific exclusion technique like the ones below. * * results : the values of v under the input examples, - * ei : the enumerator information for x, * exp : if this function returns true, then exp contains a (possibly * generalize) explanation for why v can be excluded. */ - bool getExplanationForEnumeratorExclude(Node x, + bool getExplanationForEnumeratorExclude(Node e, Node v, std::vector& results, - EnumInfo& ei, std::vector& exp); - /** returns true if we can exlude values of x based on negative str.contains + /** returns true if we can exlude values of e based on negative str.contains * - * Values v for x may be excluded if we realize that the value of v under the + * Values v for e may be excluded if we realize that the value of v under the * substitution for some input example will never be contained in some output * example. For details on this technique, see NegContainsSygusInvarianceTest * in sygus_invariance.h. * - * This function depends on whether x is being used to enumerate values + * This function depends on whether e is being used to enumerate values * for any node that is conditional in the strategy graph. For example, * nodes that are children of ITE strategy nodes are conditional. If any node * is conditional, then this function returns false. */ - bool useStrContainsEnumeratorExclude(Node x, EnumInfo& ei); + bool useStrContainsEnumeratorExclude(Node e); /** cache for the above function */ std::map d_use_str_contains_eexc; - //------------------------------ strategy registration - /** collect enumerator types - * - * This builds the strategy for enumerated values of type tn for the given - * role of nrole, for solutions to function-to-synthesize of this class. - */ - void collectEnumeratorTypes(TypeNode tn, NodeRole nrole); - /** register enumerator - * - * This registers that et is an enumerator of type tn, having enumerator - * role enum_role. - * - * inSearch is whether we will enumerate values based on this enumerator. - * A strategy node is represented by a (enumerator, node role) pair. Hence, - * we may use enumerators for which this flag is false to represent strategy - * nodes that have child strategies. - */ - void registerEnumerator(Node et, - TypeNode tn, - EnumRole enum_role, - bool inSearch); - /** infer template */ - bool inferTemplate(unsigned k, - Node n, - std::map& templ_var_index, - std::map& templ_injection); - /** static learn redundant operators - * - * This learns static lemmas for pruning enumerative space based on the - * strategy for the function-to-synthesize of this class, and stores these - * into lemmas. - */ - void staticLearnRedundantOps(std::vector& lemmas); - /** helper for static learn redundant operators - * - * (e, nrole) specify the strategy node in the graph we are currently - * analyzing, visited stores the nodes we have already visited. - * - * This method builds the mapping needs_cons, which maps (master) enumerators - * to a map from the constructors that it needs. - * - * ind is the depth in the strategy graph we are at (for debugging). - * - * isCond is whether the current enumerator is conditional (beneath a - * conditional of an strat_ITE strategy). - */ - void staticLearnRedundantOps( - Node e, - NodeRole nrole, - std::map >& visited, - std::map >& needs_cons, - int ind, - bool isCond); - //------------------------------ end strategy registration - + //------------------------------ constructing solutions /** helper function for construct solution. * * Construct a solution based on enumerator e for function-to-synthesize of @@ -644,41 +484,6 @@ class SygusUnif std::map > incr, UnifContext& x); //------------------------------ end constructing solutions - - /** represents a strategy for a SyGuS datatype type - * - * This represents a possible strategy to apply when processing a strategy - * node in constructSolution. When applying the strategy represented by this - * class, we may make recursive calls to the children of the strategy, - * given in d_cenum. If all recursive calls to constructSolution for these - * children are successful, say: - * constructSolution( d_cenum[1], ... ) = t1, - * ..., - * constructSolution( d_cenum[n], ... ) = tn, - * Then, the solution returned by this strategy is - * d_sol_templ * { d_sol_templ_args -> (t1,...,tn) } - * where * is application of substitution. - */ - class EnumTypeInfoStrat - { - public: - /** the type of strategy this represents */ - StrategyType d_this; - /** the sygus datatype constructor that induced this strategy - * - * For example, this may be a sygus datatype whose sygus operator is ITE, - * if the strategy type above is strat_ITE. - */ - Node d_cons; - /** children of this strategy */ - std::vector > d_cenum; - /** the arguments for the (templated) solution */ - std::vector d_sol_templ_args; - /** the template for the solution */ - Node d_sol_templ; - /** Returns true if argument is valid strategy in context x */ - bool isValid(SygusUnif* pbe, UnifContext& x); - }; }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index c5899128d..c397dec52 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -108,6 +108,19 @@ Node SygusUnifStrategy::getRootEnumerator() return it->second; } +EnumInfo& SygusUnifStrategy::getEnumInfo(Node e) +{ + std::map::iterator it = d_einfo.find(e); + Assert(it != d_einfo.end()); + return it->second; +} + +EnumTypeInfo& SygusUnifStrategy::getEnumTypeInfo(TypeNode tn) +{ + std::map::iterator it = d_tinfo.find(tn); + Assert(it != d_tinfo.end()); + return it->second; +} // ----------------------------- establishing enumeration types void SygusUnifStrategy::registerEnumerator(Node et, diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index 94eadbc68..9a6c7ea4a 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -143,11 +143,6 @@ class EnumInfo std::vector d_enum_slave; private: - /** - * Whether an enumerated value for this conjecture has solved the entire - * conjecture. - */ - Node d_enum_solved; /** the role of this enumerator (one of enum_* above). */ EnumRole d_role; /** is this enumerator conditional */ @@ -250,18 +245,28 @@ class SygusUnifStrategy std::vector& lemmas); /** Get the root enumerator for this class */ Node getRootEnumerator(); - /** maps enumerators to relevant information */ - std::map d_einfo; - /** list of all enumerators for the function-to-synthesize */ - std::vector d_esym_list; - /** Info for sygus datatype type occurring in a field of d_root */ - std::map d_tinfo; + /** + * Get the enumerator info for enumerator e, where e must be an enumerator + * initialized by this class (in enums after a call to initialize). + */ + EnumInfo& getEnumInfo(Node e); + /** + * Get the enumerator type info for sygus type t, where t must be the type + * of some enumerator initialized by this class + */ + EnumTypeInfo& getEnumTypeInfo(TypeNode tn); private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; /** The candidate variable this strategy is for */ Node d_candidate; + /** maps enumerators to relevant information */ + std::map d_einfo; + /** list of all enumerators for the function-to-synthesize */ + std::vector d_esym_list; + /** Info for sygus datatype type occurring in a field of d_root */ + std::map d_tinfo; /** * The root sygus datatype for the function-to-synthesize, * which encodes the overall syntactic restrictions on the space