diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.h | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.cpp | 1327 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif.h | 346 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 1272 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.h | 388 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_strat.cpp | 6 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_strat.h | 24 |
7 files changed, 1754 insertions, 1613 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index b45b602ec..235fbe3dd 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -19,7 +19,7 @@ #include "context/cdhashmap.h" #include "theory/quantifiers/sygus/sygus_module.h" -#include "theory/quantifiers/sygus/sygus_unif.h" +#include "theory/quantifiers/sygus/sygus_unif_io.h" namespace CVC4 { namespace theory { @@ -219,7 +219,7 @@ class CegConjecturePbe : public SygusModule * the core algorithm (e.g. decision tree learning) that this module relies * upon. */ - std::map<Node, SygusUnif> d_sygus_unif; + std::map<Node, SygusUnifIo> d_sygus_unif; /** * map from candidates to the list of enumerators that are being used to * build solutions for that candidate by the above utility. diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 27568fcce..4fcfd50eb 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -26,445 +26,8 @@ namespace CVC4 { namespace theory { namespace quantifiers { -UnifContext::UnifContext() : d_has_string_pos(role_invalid) -{ - d_true = NodeManager::currentNM()->mkConst(true); - d_false = NodeManager::currentNM()->mkConst(false); -} - -bool UnifContext::updateContext(SygusUnif* pbe, - std::vector<Node>& vals, - bool pol) -{ - Assert(d_vals.size() == vals.size()); - bool changed = false; - Node poln = pol ? d_true : d_false; - for (unsigned i = 0; i < vals.size(); i++) - { - if (vals[i] != poln) - { - if (d_vals[i] == d_true) - { - d_vals[i] = d_false; - changed = true; - } - } - } - if (changed) - { - d_visit_role.clear(); - } - return changed; -} - -bool UnifContext::updateStringPosition(SygusUnif* pbe, - std::vector<unsigned>& pos) -{ - Assert(pos.size() == d_str_pos.size()); - bool changed = false; - for (unsigned i = 0; i < pos.size(); i++) - { - if (pos[i] > 0) - { - d_str_pos[i] += pos[i]; - changed = true; - } - } - if (changed) - { - d_visit_role.clear(); - } - return changed; -} - -bool UnifContext::isReturnValueModified() -{ - if (d_has_string_pos != role_invalid) - { - return true; - } - return false; -} - -void UnifContext::initialize(SygusUnif* pbe) -{ - Assert(d_vals.empty()); - Assert(d_str_pos.empty()); - - // initialize with #examples - unsigned sz = pbe->d_examples.size(); - for (unsigned i = 0; i < sz; i++) - { - d_vals.push_back(d_true); - } - - if (!pbe->d_examples_out.empty()) - { - // output type of the examples - TypeNode exotn = pbe->d_examples_out[0].getType(); - - if (exotn.isString()) - { - for (unsigned i = 0; i < sz; i++) - { - d_str_pos.push_back(0); - } - } - } - d_visit_role.clear(); -} - -void UnifContext::getCurrentStrings(SygusUnif* pbe, - const std::vector<Node>& vals, - std::vector<String>& ex_vals) -{ - bool isPrefix = d_has_string_pos == role_string_prefix; - String dummy; - for (unsigned i = 0; i < vals.size(); i++) - { - if (d_vals[i] == pbe->d_true) - { - Assert(vals[i].isConst()); - unsigned pos_value = d_str_pos[i]; - if (pos_value > 0) - { - Assert(d_has_string_pos != role_invalid); - String s = vals[i].getConst<String>(); - Assert(pos_value <= s.size()); - ex_vals.push_back(isPrefix ? s.suffix(s.size() - pos_value) - : s.prefix(s.size() - pos_value)); - } - else - { - ex_vals.push_back(vals[i].getConst<String>()); - } - } - else - { - // irrelevant, add dummy - ex_vals.push_back(dummy); - } - } -} - -bool UnifContext::getStringIncrement(SygusUnif* pbe, - bool isPrefix, - const std::vector<String>& ex_vals, - const std::vector<Node>& vals, - std::vector<unsigned>& inc, - unsigned& tot) -{ - for (unsigned j = 0; j < vals.size(); j++) - { - unsigned ival = 0; - if (d_vals[j] == pbe->d_true) - { - // example is active in this context - Assert(vals[j].isConst()); - String mystr = vals[j].getConst<String>(); - ival = mystr.size(); - if (mystr.size() <= ex_vals[j].size()) - { - if (!(isPrefix ? ex_vals[j].strncmp(mystr, ival) - : ex_vals[j].rstrncmp(mystr, ival))) - { - Trace("sygus-pbe-dt-debug") << "X"; - return false; - } - } - else - { - Trace("sygus-pbe-dt-debug") << "X"; - return false; - } - } - Trace("sygus-pbe-dt-debug") << ival; - tot += ival; - inc.push_back(ival); - } - return true; -} -bool UnifContext::isStringSolved(SygusUnif* pbe, - const std::vector<String>& ex_vals, - const std::vector<Node>& vals) -{ - for (unsigned j = 0; j < vals.size(); j++) - { - if (d_vals[j] == pbe->d_true) - { - // example is active in this context - Assert(vals[j].isConst()); - String mystr = vals[j].getConst<String>(); - if (ex_vals[j] != mystr) - { - return false; - } - } - } - return true; -} - -// status : 0 : exact, -1 : vals is subset, 1 : vals is superset -Node SubsumeTrie::addTermInternal(Node t, - const std::vector<Node>& vals, - bool pol, - std::vector<Node>& subsumed, - bool spol, - unsigned index, - int status, - bool checkExistsOnly, - bool checkSubsume) -{ - if (index == vals.size()) - { - if (status == 0) - { - // set the term if checkExistsOnly = false - if (d_term.isNull() && !checkExistsOnly) - { - d_term = t; - } - } - else if (status == 1) - { - Assert(checkSubsume); - // found a subsumed term - if (!d_term.isNull()) - { - subsumed.push_back(d_term); - if (!checkExistsOnly) - { - // remove it if checkExistsOnly = false - d_term = Node::null(); - } - } - } - else - { - Assert(!checkExistsOnly && checkSubsume); - } - return d_term; - } - NodeManager* nm = NodeManager::currentNM(); - // the current value - Assert(pol || (vals[index].isConst() && vals[index].getType().isBoolean())); - Node cv = pol ? vals[index] : nm->mkConst(!vals[index].getConst<bool>()); - // if checkExistsOnly = false, check if the current value is subsumed if - // checkSubsume = true, if so, don't add - if (!checkExistsOnly && checkSubsume) - { - Assert(cv.isConst() && cv.getType().isBoolean()); - std::vector<bool> check_subsumed_by; - if (status == 0) - { - if (!cv.getConst<bool>()) - { - check_subsumed_by.push_back(spol); - } - } - else if (status == -1) - { - check_subsumed_by.push_back(spol); - if (!cv.getConst<bool>()) - { - check_subsumed_by.push_back(!spol); - } - } - // check for subsumed nodes - for (unsigned i = 0, size = check_subsumed_by.size(); i < size; i++) - { - bool csbi = check_subsumed_by[i]; - Node csval = nm->mkConst(csbi); - // check if subsumed - std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval); - if (itc != d_children.end()) - { - Node ret = itc->second.addTermInternal(t, - vals, - pol, - subsumed, - spol, - index + 1, - -1, - checkExistsOnly, - checkSubsume); - // ret subsumes t - if (!ret.isNull()) - { - return ret; - } - } - } - } - Node ret; - std::vector<bool> check_subsume; - if (status == 0) - { - if (checkExistsOnly) - { - std::map<Node, SubsumeTrie>::iterator itc = d_children.find(cv); - if (itc != d_children.end()) - { - ret = itc->second.addTermInternal(t, - vals, - pol, - subsumed, - spol, - index + 1, - 0, - checkExistsOnly, - checkSubsume); - } - } - else - { - Assert(spol); - ret = d_children[cv].addTermInternal(t, - vals, - pol, - subsumed, - spol, - index + 1, - 0, - checkExistsOnly, - checkSubsume); - if (ret != t) - { - // we were subsumed by ret, return - return ret; - } - } - if (checkSubsume) - { - Assert(cv.isConst() && cv.getType().isBoolean()); - // check for subsuming - if (cv.getConst<bool>()) - { - check_subsume.push_back(!spol); - } - } - } - else if (status == 1) - { - Assert(checkSubsume); - Assert(cv.isConst() && cv.getType().isBoolean()); - check_subsume.push_back(!spol); - if (cv.getConst<bool>()) - { - check_subsume.push_back(spol); - } - } - if (checkSubsume) - { - // check for subsumed terms - for (unsigned i = 0, size = check_subsume.size(); i < size; i++) - { - Node csval = nm->mkConst<bool>(check_subsume[i]); - std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval); - if (itc != d_children.end()) - { - itc->second.addTermInternal(t, - vals, - pol, - subsumed, - spol, - index + 1, - 1, - checkExistsOnly, - checkSubsume); - // clean up - if (itc->second.isEmpty()) - { - Assert(!checkExistsOnly); - d_children.erase(csval); - } - } - } - } - return ret; -} - -Node SubsumeTrie::addTerm(Node t, - const std::vector<Node>& vals, - bool pol, - std::vector<Node>& subsumed) -{ - return addTermInternal(t, vals, pol, subsumed, true, 0, 0, false, true); -} - -Node SubsumeTrie::addCond(Node c, const std::vector<Node>& vals, bool pol) -{ - std::vector<Node> subsumed; - return addTermInternal(c, vals, pol, subsumed, true, 0, 0, false, false); -} - -void SubsumeTrie::getSubsumed(const std::vector<Node>& vals, - bool pol, - std::vector<Node>& subsumed) -{ - addTermInternal(Node::null(), vals, pol, subsumed, true, 0, 1, true, true); -} - -void SubsumeTrie::getSubsumedBy(const std::vector<Node>& vals, - bool pol, - std::vector<Node>& subsumed_by) -{ - // flip polarities - addTermInternal( - Node::null(), vals, !pol, subsumed_by, false, 0, 1, true, true); -} - -void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals, - bool pol, - std::map<int, std::vector<Node> >& v, - unsigned index, - int status) -{ - if (index == vals.size()) - { - Assert(!d_term.isNull()); - Assert(std::find(v[status].begin(), v[status].end(), d_term) - == v[status].end()); - v[status].push_back(d_term); - } - else - { - Assert(vals[index].isConst() && vals[index].getType().isBoolean()); - bool curr_val_true = vals[index].getConst<bool>() == pol; - for (std::map<Node, SubsumeTrie>::iterator it = d_children.begin(); - it != d_children.end(); - ++it) - { - int new_status = status; - // if the current value is true - if (curr_val_true) - { - if (status != 0) - { - Assert(it->first.isConst() && it->first.getType().isBoolean()); - new_status = (it->first.getConst<bool>() ? 1 : -1); - if (status != -2 && new_status != status) - { - new_status = 0; - } - } - } - it->second.getLeavesInternal(vals, pol, v, index + 1, new_status); - } - } -} - -void SubsumeTrie::getLeaves(const std::vector<Node>& vals, - bool pol, - std::map<int, std::vector<Node> >& v) -{ - getLeavesInternal(vals, pol, v, 0, -2); -} - SygusUnif::SygusUnif() { - d_true = NodeManager::currentNM()->mkConst(true); - d_false = NodeManager::currentNM()->mkConst(false); } SygusUnif::~SygusUnif() {} @@ -478,215 +41,10 @@ void SygusUnif::initialize(QuantifiersEngine* qe, d_candidate = f; d_qe = qe; d_tds = qe->getTermDatabaseSygus(); - + // initialize the strategy d_strategy.initialize(qe, f, enums, lemmas); } -void SygusUnif::resetExamples() -{ - d_examples.clear(); - d_examples_out.clear(); - // also clear information in strategy tree - // TODO -} - -void SygusUnif::addExample(const std::vector<Node>& input, Node output) -{ - d_examples.push_back(input); - d_examples_out.push_back(output); -} - -void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) -{ - Node c = d_candidate; - Assert(!d_examples.empty()); - Assert(d_examples.size() == d_examples_out.size()); - - EnumInfo& ei = d_strategy.getEnumInfo(e); - // The explanation for why the current value should be excluded in future - // iterations. - Node exp_exc; - - TypeNode xtn = e.getType(); - Node bv = d_tds->sygusToBuiltin(v, xtn); - std::vector<Node> base_results; - // compte the results - for (unsigned j = 0, size = d_examples.size(); j < size; j++) - { - Node res = d_tds->evaluateBuiltin(xtn, bv, d_examples[j]); - Trace("sygus-pbe-enum-debug") - << "...got res = " << res << " from " << bv << std::endl; - base_results.push_back(res); - } - // is it excluded for domain-specific reason? - std::vector<Node> exp_exc_vec; - if (getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec)) - { - Assert(!exp_exc_vec.empty()); - exp_exc = exp_exc_vec.size() == 1 - ? exp_exc_vec[0] - : NodeManager::currentNM()->mkNode(AND, exp_exc_vec); - Trace("sygus-pbe-enum") - << " ...fail : term is excluded (domain-specific)" << std::endl; - } - else - { - // notify all slaves - Assert(!ei.d_enum_slave.empty()); - // explanation for why this value should be excluded - for (unsigned s = 0; s < ei.d_enum_slave.size(); s++) - { - 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 (eiv.getRole() == enum_io) - { - Trace("sygus-pbe-enum") << " IO-Eval of "; - // prevIsCover = eiv.isFeasible(); - } - else - { - Trace("sygus-pbe-enum") << "Evaluation of "; - } - Trace("sygus-pbe-enum") << xs << " : "; - // evaluate all input/output examples - std::vector<Node> results; - Node templ = eiv.d_template; - TNode templ_var = eiv.d_template_arg; - std::map<Node, bool> cond_vals; - for (unsigned j = 0, size = base_results.size(); j < size; j++) - { - Node res = base_results[j]; - Assert(res.isConst()); - if (!templ.isNull()) - { - TNode tres = res; - res = templ.substitute(templ_var, res); - res = Rewriter::rewrite(res); - Assert(res.isConst()); - } - Node resb; - if (eiv.getRole() == enum_io) - { - Node out = d_examples_out[j]; - Assert(out.isConst()); - resb = res == out ? d_true : d_false; - } - else - { - resb = res; - } - cond_vals[resb] = true; - results.push_back(resb); - if (Trace.isOn("sygus-pbe-enum")) - { - if (resb.getType().isBoolean()) - { - Trace("sygus-pbe-enum") << (resb == d_true ? "1" : "0"); - } - else - { - Trace("sygus-pbe-enum") << "?"; - } - } - } - bool keep = false; - 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()) - { - // check subsumbed/subsuming - std::vector<Node> subsume; - if (cond_vals.find(d_false) == cond_vals.end()) - { - // it is the entire solution, we are done - Trace("sygus-pbe-enum") - << " ...success, full solution added to PBE pool : " - << d_tds->sygusToBuiltin(v) << std::endl; - if (!ecv.isSolved()) - { - ecv.setSolved(v); - // it subsumes everything - ecv.d_term_trie.clear(); - ecv.d_term_trie.addTerm(v, results, true, subsume); - } - keep = true; - } - else - { - Node val = ecv.d_term_trie.addTerm(v, results, true, subsume); - if (val == v) - { - Trace("sygus-pbe-enum") << " ...success"; - if (!subsume.empty()) - { - ecv.d_enum_subsume.insert( - ecv.d_enum_subsume.end(), subsume.begin(), subsume.end()); - Trace("sygus-pbe-enum") - << " and subsumed " << subsume.size() << " terms"; - } - Trace("sygus-pbe-enum") - << "! add to PBE pool : " << d_tds->sygusToBuiltin(v) - << std::endl; - keep = true; - } - else - { - Assert(subsume.empty()); - Trace("sygus-pbe-enum") << " ...fail : subsumed" << std::endl; - } - } - } - else - { - Trace("sygus-pbe-enum") - << " ...fail : it does not satisfy examples." << std::endl; - } - } - else - { - // must be unique up to examples - Node val = ecv.d_term_trie.addCond(v, results, true); - if (val == v) - { - Trace("sygus-pbe-enum") << " ...success! add to PBE pool : " - << d_tds->sygusToBuiltin(v) << std::endl; - keep = true; - } - else - { - Trace("sygus-pbe-enum") - << " ...fail : term is not unique" << std::endl; - } - d_cond_count++; - } - if (keep) - { - // notify to retry the build of solution - d_check_sol = true; - ecv.addEnumValue(v, results); - } - } - } - - // exclude this value on subsequent iterations - if (exp_exc.isNull()) - { - // if we did not already explain why this should be excluded, use default - exp_exc = d_tds->getExplain()->getExplanationForEquality(e, v); - } - exp_exc = exp_exc.negate(); - Trace("sygus-pbe-enum-lemma") - << "SygusUnif : enumeration exclude lemma : " << exp_exc << std::endl; - lemmas.push_back(exp_exc); -} - Node SygusUnif::constructSolution() { Node c = d_candidate; @@ -695,179 +53,65 @@ Node SygusUnif::constructSolution() // already has a solution return d_solution; } - else - { - // only check if an enumerator updated - if (d_check_sol) - { - 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_cond_count; i++) - { - Trace("sygus-pbe-dt") - << "ConstructPBE for candidate: " << c << std::endl; - Node e = d_strategy.getRootEnumerator(); - UnifContext x; - x.initialize(this); - Node vcc = constructSolution(e, role_equal, x, 1); - if (!vcc.isNull()) - { - if (vc.isNull() || (!vc.isNull() + // only check if an enumerator updated + if (d_check_sol) + { + 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_cond_count; i++) + { + Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl; + Node e = d_strategy.getRootEnumerator(); + // initialize a call to construct solution + initializeConstructSol(); + // call the virtual construct solution method + Node vcc = constructSol(e, role_equal, 1); + // if we constructed the solution, and we either did not previously have + // a solution, or the new solution is better (smaller). + if (!vcc.isNull() + && (vc.isNull() || (!vc.isNull() && d_tds->getSygusTermSize(vcc) - < d_tds->getSygusTermSize(vc))) - { - Trace("sygus-pbe") - << "**** PBE SOLVED : " << c << " = " << vcc << std::endl; - Trace("sygus-pbe") << "...solved at iteration " << i << std::endl; - vc = vcc; - } - } - } - if (!vc.isNull()) + < d_tds->getSygusTermSize(vc)))) { - d_solution = vc; - return vc; + Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc + << std::endl; + Trace("sygus-pbe") << "...solved at iteration " << i << std::endl; + vc = vcc; } - Trace("sygus-pbe") << "...failed to solve." << std::endl; } - return Node::null(); - } -} - -// ------------------------------------ solution construction from enumeration - -bool SygusUnif::useStrContainsEnumeratorExclude(Node e) -{ - TypeNode xbt = d_tds->sygusToBuiltinType(e.getType()); - if (xbt.isString()) - { - std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(e); - if (itx != d_use_str_contains_eexc.end()) + if (!vc.isNull()) { - return itx->second; - } - 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) - { - 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[e] = false; - return false; - } - if (eis.isConditional()) - { - Trace("sygus-pbe-enum-debug") - << " conditional slave : " << sn << std::endl; - 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[e]; - } - return false; -} - -bool SygusUnif::getExplanationForEnumeratorExclude(Node e, - Node v, - std::vector<Node>& results, - std::vector<Node>& exp) -{ - if (useStrContainsEnumeratorExclude(e)) - { - NodeManager* nm = NodeManager::currentNM(); - // This check whether the example evaluates to something that is larger than - // the output for some input/output pair. If so, then this term is never - // useful. We generalize its explanation below. - - if (Trace.isOn("sygus-pbe-cterm-debug")) - { - Trace("sygus-pbe-enum") << std::endl; - } - // 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 " << e - << " -> " << d_tds->sygusToBuiltin(v) - << " based on str.contains." << std::endl; - std::vector<unsigned> cmp_indices; - for (unsigned i = 0, size = results.size(); i < size; i++) - { - Assert(results[i].isConst()); - Assert(d_examples_out[i].isConst()); - Trace("sygus-pbe-cterm-debug") << " " << results[i] << " <> " - << d_examples_out[i]; - Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]); - Node contr = Rewriter::rewrite(cont); - if (contr == d_false) - { - cmp_indices.push_back(i); - Trace("sygus-pbe-cterm-debug") << "...not contained." << std::endl; - } - else - { - Trace("sygus-pbe-cterm-debug") << "...contained." << std::endl; - } - } - if (!cmp_indices.empty()) - { - // we check invariance with respect to a negative contains test - NegContainsSygusInvarianceTest ncset; - ncset.init(e, d_examples, d_examples_out, cmp_indices); - // construct the generalized explanation - 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; - return true; + d_solution = vc; + return vc; } + Trace("sygus-pbe") << "...failed to solve." << std::endl; } - return false; + return Node::null(); } -void SygusUnif::EnumCache::addEnumValue(Node v, std::vector<Node>& results) -{ - // should not have been enumerated before - Assert(d_enum_val_to_index.find(v) == d_enum_val_to_index.end()); - d_enum_val_to_index[v] = d_enum_vals.size(); - d_enum_vals.push_back(v); - d_enum_vals_res.push_back(results); -} - -Node SygusUnif::constructBestSolvedTerm(std::vector<Node>& solved, - UnifContext& x) +Node SygusUnif::constructBestSolvedTerm(const std::vector<Node>& solved) { Assert(!solved.empty()); return solved[0]; } -Node SygusUnif::constructBestStringSolvedTerm(std::vector<Node>& solved, - UnifContext& x) +Node SygusUnif::constructBestStringSolvedTerm(const std::vector<Node>& solved) { Assert(!solved.empty()); return solved[0]; } -Node SygusUnif::constructBestSolvedConditional(std::vector<Node>& solved, - UnifContext& x) +Node SygusUnif::constructBestSolvedConditional(const std::vector<Node>& solved) { Assert(!solved.empty()); return solved[0]; } -Node SygusUnif::constructBestConditional(std::vector<Node>& conds, - UnifContext& x) +Node SygusUnif::constructBestConditional(const std::vector<Node>& conds) { Assert(!conds.empty()); double r = Random::getRandom().pickDouble(0.0, 1.0); @@ -880,504 +124,23 @@ Node SygusUnif::constructBestConditional(std::vector<Node>& conds, } Node SygusUnif::constructBestStringToConcat( - std::vector<Node> strs, - std::map<Node, unsigned> total_inc, - std::map<Node, std::vector<unsigned> > incr, - UnifContext& x) + const std::vector<Node>& strs, + const std::map<Node, unsigned>& total_inc, + const std::map<Node, std::vector<unsigned> >& incr) { Assert(!strs.empty()); - std::random_shuffle(strs.begin(), strs.end()); + std::vector<Node> strs_tmp = strs; + std::random_shuffle(strs_tmp.begin(), strs_tmp.end()); // prefer one that has incremented by more than 0 - for (const Node& ns : strs) + for (const Node& ns : strs_tmp) { - if (total_inc[ns] > 0) + const std::map<Node, unsigned>::const_iterator iti = total_inc.find(ns); + if (iti != total_inc.end() && iti->second > 0) { return ns; } } - return strs[0]; -} - -Node SygusUnif::constructSolution(Node e, - NodeRole nrole, - UnifContext& x, - int ind) -{ - TypeNode etn = e.getType(); - if (Trace.isOn("sygus-pbe-dt-debug")) - { - indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") << "ConstructPBE: (" << e << ", " << nrole - << ") for type " << etn << " in context "; - print_val("sygus-pbe-dt-debug", x.d_vals); - if (x.d_has_string_pos != role_invalid) - { - Trace("sygus-pbe-dt-debug") << ", string context [" << x.d_has_string_pos; - for (unsigned i = 0, size = x.d_str_pos.size(); i < size; i++) - { - Trace("sygus-pbe-dt-debug") << " " << x.d_str_pos[i]; - } - Trace("sygus-pbe-dt-debug") << "]"; - } - Trace("sygus-pbe-dt-debug") << std::endl; - } - // enumerator type info - EnumTypeInfo& tinfo = d_strategy.getEnumTypeInfo(etn); - - // get the enumerator information - EnumInfo& einfo = d_strategy.getEnumInfo(e); - - EnumCache& ecache = d_ecache[e]; - - Node ret_dt; - if (nrole == role_equal) - { - if (!x.isReturnValueModified()) - { - if (ecache.isSolved()) - { - // this type has a complete solution - ret_dt = ecache.getSolved(); - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "return PBE: success : solved " - << d_tds->sygusToBuiltin(ret_dt) << std::endl; - Assert(!ret_dt.isNull()); - } - else - { - // could be conditionally solved - std::vector<Node> subsumed_by; - ecache.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by); - if (!subsumed_by.empty()) - { - ret_dt = constructBestSolvedTerm(subsumed_by, x); - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "return PBE: success : conditionally solved" - << d_tds->sygusToBuiltin(ret_dt) << std::endl; - } - else - { - indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") - << " ...not currently conditionally solved." << std::endl; - } - } - } - if (ret_dt.isNull()) - { - if (d_tds->sygusToBuiltinType(e.getType()).isString()) - { - // check if a current value that closes all examples - // get the term enumerator for this type - std::map<EnumRole, Node>::iterator itnt = - tinfo.d_enum.find(enum_concat_term); - if (itnt != tinfo.d_enum.end()) - { - Node et = itnt->second; - - EnumCache& ecachet = d_ecache[et]; - // get the current examples - std::vector<String> ex_vals; - x.getCurrentStrings(this, d_examples_out, ex_vals); - Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size()); - - // test each example in the term enumerator for the type - std::vector<Node> str_solved; - for (unsigned i = 0, size = ecachet.d_enum_vals.size(); i < size; i++) - { - if (x.isStringSolved(this, ex_vals, ecachet.d_enum_vals_res[i])) - { - str_solved.push_back(ecachet.d_enum_vals[i]); - } - } - if (!str_solved.empty()) - { - ret_dt = constructBestStringSolvedTerm(str_solved, x); - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "return PBE: success : string solved " - << d_tds->sygusToBuiltin(ret_dt) << std::endl; - } - else - { - indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") - << " ...not currently string solved." << std::endl; - } - } - } - } - } - else if (nrole == role_string_prefix || nrole == role_string_suffix) - { - // check if each return value is a prefix/suffix of all open examples - if (!x.isReturnValueModified() || x.d_has_string_pos == nrole) - { - std::map<Node, std::vector<unsigned> > incr; - bool isPrefix = nrole == role_string_prefix; - std::map<Node, unsigned> total_inc; - std::vector<Node> inc_strs; - // make the value of the examples - std::vector<String> ex_vals; - x.getCurrentStrings(this, d_examples_out, ex_vals); - if (Trace.isOn("sygus-pbe-dt-debug")) - { - indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") << "current strings : " << std::endl; - for (unsigned i = 0, size = ex_vals.size(); i < size; i++) - { - indent("sygus-pbe-dt-debug", ind + 1); - Trace("sygus-pbe-dt-debug") << ex_vals[i] << std::endl; - } - } - - // check if there is a value for which is a prefix/suffix of all active - // examples - Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size()); - - for (unsigned i = 0, size = ecache.d_enum_vals.size(); i < size; 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(ecache.d_enum_vals_res[i].size() == d_examples_out.size()); - unsigned tot = 0; - bool exsuccess = x.getStringIncrement(this, - isPrefix, - ex_vals, - ecache.d_enum_vals_res[i], - incr[val_t], - tot); - if (!exsuccess) - { - incr.erase(val_t); - Trace("sygus-pbe-dt-debug") << "...fail" << std::endl; - } - else - { - total_inc[val_t] = tot; - inc_strs.push_back(val_t); - Trace("sygus-pbe-dt-debug") - << "...success, total increment = " << tot << std::endl; - } - } - - if (!incr.empty()) - { - ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr, x); - Assert(!ret_dt.isNull()); - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") - << "PBE: CONCAT strategy : choose " << (isPrefix ? "pre" : "suf") - << "fix value " << d_tds->sygusToBuiltin(ret_dt) << std::endl; - // update the context - bool ret = x.updateStringPosition(this, incr[ret_dt]); - AlwaysAssert(ret == (total_inc[ret_dt] > 0)); - x.d_has_string_pos = nrole; - } - else - { - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "PBE: failed CONCAT strategy, no values are " - << (isPrefix ? "pre" : "suf") - << "fix of all examples." << std::endl; - } - } - else - { - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") - << "PBE: failed CONCAT strategy, prefix/suffix mismatch." - << std::endl; - } - } - if (ret_dt.isNull() && !einfo.isTemplated()) - { - // we will try a single strategy - EnumTypeInfoStrat* etis = nullptr; - std::map<NodeRole, StrategyNode>::iterator itsn = - tinfo.d_snodes.find(nrole); - if (itsn != tinfo.d_snodes.end()) - { - // strategy info - StrategyNode& snode = itsn->second; - if (x.d_visit_role[e].find(nrole) == x.d_visit_role[e].end()) - { - x.d_visit_role[e][nrole] = true; - // try a random strategy - if (snode.d_strats.size() > 1) - { - std::random_shuffle(snode.d_strats.begin(), snode.d_strats.end()); - } - // get an eligible strategy index - unsigned sindex = 0; - while (sindex < snode.d_strats.size() - && !snode.d_strats[sindex]->isValid(&x)) - { - sindex++; - } - // if we found a eligible strategy - if (sindex < snode.d_strats.size()) - { - etis = snode.d_strats[sindex]; - } - } - } - if (etis != nullptr) - { - StrategyType strat = etis->d_this; - indent("sygus-pbe-dt", ind + 1); - Trace("sygus-pbe-dt") - << "...try STRATEGY " << strat << "..." << std::endl; - - std::map<unsigned, Node> look_ahead_solved_children; - std::vector<Node> dt_children_cons; - bool success = true; - - // for ITE - Node split_cond_enum; - int split_cond_res_index = -1; - - for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++) - { - indent("sygus-pbe-dt", ind + 1); - Trace("sygus-pbe-dt") - << "construct PBE child #" << sc << "..." << std::endl; - Node rec_c; - std::map<unsigned, Node>::iterator itla = - look_ahead_solved_children.find(sc); - if (itla != look_ahead_solved_children.end()) - { - rec_c = itla->second; - indent("sygus-pbe-dt-debug", ind + 1); - Trace("sygus-pbe-dt-debug") - << "ConstructPBE: look ahead solved : " - << d_tds->sygusToBuiltin(rec_c) << std::endl; - } - else - { - std::pair<Node, NodeRole>& cenum = etis->d_cenum[sc]; - - // update the context - std::vector<Node> prev; - if (strat == strat_ITE && sc > 0) - { - EnumCache& ecache_cond = d_ecache[split_cond_enum]; - Assert(split_cond_res_index >= 0); - Assert(split_cond_res_index - < (int)ecache_cond.d_enum_vals_res.size()); - prev = x.d_vals; - bool ret = x.updateContext( - this, - ecache_cond.d_enum_vals_res[split_cond_res_index], - sc == 1); - AlwaysAssert(ret); - } - - // recurse - if (strat == strat_ITE && sc == 0) - { - Node ce = cenum.first; - - EnumCache& ecache_child = d_ecache[ce]; - - // only used if the return value is not modified - if (!x.isReturnValueModified()) - { - if (x.d_uinfo.find(ce) == x.d_uinfo.end()) - { - Trace("sygus-pbe-dt-debug2") - << " reg : PBE: Look for direct solutions for conditional " - "enumerator " - << ce << " ... " << std::endl; - Assert(ecache_child.d_enum_vals.size() - == ecache_child.d_enum_vals_res.size()); - for (unsigned i = 1; i <= 2; i++) - { - std::pair<Node, NodeRole>& te_pair = etis->d_cenum[i]; - Node te = te_pair.first; - 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 = ecache_child.d_enum_vals.size(); - k < size; - k++) - { - Node cond = ecache_child.d_enum_vals[k]; - std::vector<Node> 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 " - << i << std::endl; - if (!solved.empty()) - { - Node slv = constructBestSolvedTerm(solved, x); - Trace("sygus-pbe-dt-debug2") - << " reg : PBE: ..." << d_tds->sygusToBuiltin(slv) - << " is a solution under branch " << i; - Trace("sygus-pbe-dt-debug2") - << " of condition " << d_tds->sygusToBuiltin(cond) - << std::endl; - x.d_uinfo[ce].d_look_ahead_sols[cond][i] = slv; - } - } - } - } - } - - // get the conditionals in the current context : they must be - // distinguishable - std::map<int, std::vector<Node> > possible_cond; - std::map<Node, int> solved_cond; // stores branch - ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond); - - std::map<int, std::vector<Node> >::iterator itpc = - possible_cond.find(0); - if (itpc != possible_cond.end()) - { - if (Trace.isOn("sygus-pbe-dt-debug")) - { - indent("sygus-pbe-dt-debug", ind + 1); - Trace("sygus-pbe-dt-debug") - << "PBE : We have " << itpc->second.size() - << " distinguishable conditionals:" << std::endl; - for (Node& cond : itpc->second) - { - indent("sygus-pbe-dt-debug", ind + 2); - Trace("sygus-pbe-dt-debug") - << d_tds->sygusToBuiltin(cond) << std::endl; - } - } - - // static look ahead conditional : choose conditionals that have - // solved terms in at least one branch - // only applicable if we have not modified the return value - std::map<int, std::vector<Node> > solved_cond; - if (!x.isReturnValueModified()) - { - Assert(x.d_uinfo.find(ce) != x.d_uinfo.end()); - int solve_max = 0; - for (Node& cond : itpc->second) - { - std::map<Node, std::map<unsigned, Node> >::iterator itla = - x.d_uinfo[ce].d_look_ahead_sols.find(cond); - if (itla != x.d_uinfo[ce].d_look_ahead_sols.end()) - { - int nsolved = itla->second.size(); - solve_max = nsolved > solve_max ? nsolved : solve_max; - solved_cond[nsolved].push_back(cond); - } - } - int n = solve_max; - while (n > 0) - { - if (!solved_cond[n].empty()) - { - rec_c = constructBestSolvedConditional(solved_cond[n], x); - indent("sygus-pbe-dt", ind + 1); - Trace("sygus-pbe-dt") - << "PBE: ITE strategy : choose solved conditional " - << d_tds->sygusToBuiltin(rec_c) << " with " << n - << " solved children..." << std::endl; - std::map<Node, std::map<unsigned, Node> >::iterator itla = - x.d_uinfo[ce].d_look_ahead_sols.find(rec_c); - Assert(itla != x.d_uinfo[ce].d_look_ahead_sols.end()); - for (std::pair<const unsigned, Node>& las : itla->second) - { - look_ahead_solved_children[las.first] = las.second; - } - break; - } - n--; - } - } - - // otherwise, guess a conditional - if (rec_c.isNull()) - { - rec_c = constructBestConditional(itpc->second, x); - Assert(!rec_c.isNull()); - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") - << "PBE: ITE strategy : choose random conditional " - << d_tds->sygusToBuiltin(rec_c) << std::endl; - } - } - else - { - // TODO (#1250) : degenerate case where children have different - // types? - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "return PBE: failed ITE strategy, " - "cannot find a distinguishable condition" - << std::endl; - } - if (!rec_c.isNull()) - { - 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)ecache_child.d_enum_vals_res.size()); - } - } - else - { - rec_c = constructSolution(cenum.first, cenum.second, x, ind + 2); - } - - // undo update the context - if (strat == strat_ITE && sc > 0) - { - x.d_vals = prev; - } - } - if (!rec_c.isNull()) - { - dt_children_cons.push_back(rec_c); - } - else - { - success = false; - break; - } - } - if (success) - { - Assert(dt_children_cons.size() == etis->d_sol_templ_args.size()); - // ret_dt = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, - // dt_children ); - ret_dt = etis->d_sol_templ; - ret_dt = ret_dt.substitute(etis->d_sol_templ_args.begin(), - etis->d_sol_templ_args.end(), - dt_children_cons.begin(), - dt_children_cons.end()); - indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") - << "PBE: success : constructed for strategy " << strat << std::endl; - } - else - { - indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") - << "PBE: failed for strategy " << strat << std::endl; - } - } - } - - if (!ret_dt.isNull()) - { - Assert(ret_dt.getType() == e.getType()); - } - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "ConstructPBE: returned " << ret_dt << std::endl; - return ret_dt; + return strs_tmp[0]; } void SygusUnif::indent(const char* c, int ind) diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 4e7806bf0..a2e81040a 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -26,235 +26,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class SygusUnif; - -/** Unification context - * - * This class maintains state information during calls to - * SygusUnif::constructSolution, which implements unification-based - * approaches for construction solutions to synthesis conjectures. - */ -class UnifContext -{ - public: - UnifContext(); - /** - * This intiializes this context based on information in pbe regarding the - * kinds of examples it contains. - */ - void initialize(SygusUnif* pbe); - - //----------for ITE strategy - /** the value of the context conditional - * - * This stores a list of Boolean constants that is the same length of the - * number of input/output example pairs we are considering. For each i, - * if d_vals[i] = true, i/o pair #i is active according to this context - * if d_vals[i] = false, i/o pair #i is inactive according to this context - */ - std::vector<Node> d_vals; - /** update the examples - * - * if pol=true, this method updates d_vals to d_vals & vals - * if pol=false, this method updates d_vals to d_vals & ( ~vals ) - */ - bool updateContext(SygusUnif* pbe, std::vector<Node>& vals, bool pol); - //----------end for ITE strategy - - //----------for CONCAT strategies - /** the position in the strings - * - * For each i/o example pair, this stores the length of the current solution - * for the input of the pair, where the solution for that input is a prefix - * or - * suffix of the output of the pair. For example, if our i/o pairs are: - * f( "abcd" ) = "abcdcd" - * f( "aa" ) = "aacd" - * If the solution we have currently constructed is str.++( x1, "c", ... ), - * then d_str_pos = ( 5, 3 ), where notice that - * str.++( "abc", "c" ) is a prefix of "abcdcd" and - * str.++( "aa", "c" ) is a prefix of "aacd". - */ - std::vector<unsigned> d_str_pos; - /** has string position - * - * Whether the solution positions indicate a prefix or suffix of the output - * examples. If this is role_invalid, then we have not updated the string - * position. - */ - NodeRole d_has_string_pos; - /** update the string examples - * - * This method updates d_str_pos to d_str_pos + pos. - */ - bool updateStringPosition(SygusUnif* pbe, std::vector<unsigned>& pos); - /** get current strings - * - * This returns the prefix/suffix of the string constants stored in vals - * of size d_str_pos, and stores the result in ex_vals. For example, if vals - * is (abcdcd", "aacde") and d_str_pos = ( 5, 3 ), then we add - * "d" and "de" to ex_vals. - */ - void getCurrentStrings(SygusUnif* pbe, - const std::vector<Node>& vals, - std::vector<String>& ex_vals); - /** get string increment - * - * If this method returns true, then inc and tot are updated such that - * for all active indices i, - * vals[i] is a prefix (or suffix if isPrefix=false) of ex_vals[i], and - * inc[i] = str.len(vals[i]) - * for all inactive indices i, inc[i] = 0 - * We set tot to the sum of inc[i] for i=1,...,n. This indicates the total - * number of characters incremented across all examples. - */ - bool getStringIncrement(SygusUnif* pbe, - bool isPrefix, - const std::vector<String>& ex_vals, - const std::vector<Node>& vals, - std::vector<unsigned>& inc, - unsigned& tot); - /** returns true if ex_vals[i] = vals[i] for all active indices i. */ - bool isStringSolved(SygusUnif* pbe, - const std::vector<String>& ex_vals, - const std::vector<Node>& vals); - //----------end for CONCAT strategies - - /** is return value modified? - * - * This returns true if we are currently in a state where the return value - * of the solution has been modified, e.g. by a previous node that solved - * for a prefix. - */ - bool isReturnValueModified(); - /** visited role - * - * This is the current set of enumerator/node role pairs we are currently - * visiting. This set is cleared when the context is updated. - */ - std::map<Node, std::map<NodeRole, bool> > d_visit_role; - - /** unif context enumerator information */ - class UEnumInfo - { - public: - UEnumInfo() {} - /** map from conditions and branch positions to a solved node - * - * For example, if we have: - * f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 - * Then, valid entries in this map is: - * d_look_ahead_sols[x>0][1] = x+1 - * d_look_ahead_sols[x>0][2] = 1 - * For the first entry, notice that for all input examples such that x>0 - * evaluates to true, which are (1) and (3), we have that their output - * values for x+1 under the substitution that maps x to the input value, - * resulting in 2 and 4, are equal to the output value for the respective - * pairs. - */ - std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols; - }; - /** map from enumerators to the above info class */ - std::map<Node, UEnumInfo> d_uinfo; - - private: - /** true and false nodes */ - Node d_true; - Node d_false; -}; - -/** Subsumption trie -* -* This class manages a set of terms for a PBE sygus enumerator. -* -* In PBE sygus, we are interested in, for each term t, the set of I/O examples -* that it satisfies, which can be represented by a vector of Booleans. -* For example, given conjecture: -* f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 ^ f( 5 ) = 5 -* If solutions for f are of the form (lambda x. [term]), then: -* Term x satisfies 0001, -* Term x+1 satisfies 1100, -* Term 2 satisfies 0100. -* Above, term 2 is subsumed by term x+1, since the set of I/O examples that -* x+1 satisfies are a superset of those satisfied by 2. -*/ -class SubsumeTrie -{ - public: - SubsumeTrie() {} - /** - * Adds term t to the trie, removes all terms that are subsumed by t from the - * trie and adds them to subsumed. The set of I/O examples that t satisfies - * is given by (pol ? vals : !vals). - */ - Node addTerm(Node t, - const std::vector<Node>& vals, - bool pol, - std::vector<Node>& subsumed); - /** - * Adds term c to the trie, without calculating/updating based on - * subsumption. This is useful for using this class to store conditionals - * in ITE strategies, where any conditional whose set of vals is unique - * (as opposed to not subsumed) is useful. - */ - Node addCond(Node c, const std::vector<Node>& vals, bool pol); - /** - * Returns the set of terms that are subsumed by (pol ? vals : !vals). - */ - void getSubsumed(const std::vector<Node>& vals, - bool pol, - std::vector<Node>& subsumed); - /** - * Returns the set of terms that subsume (pol ? vals : !vals). This - * is for instance useful when determining whether there exists a term - * that satisfies all active examples in the decision tree learning - * algorithm. - */ - void getSubsumedBy(const std::vector<Node>& vals, - bool pol, - std::vector<Node>& subsumed_by); - /** - * Get the leaves of the trie, which we store in the map v. - * v[-1] stores the children that always evaluate to !pol, - * v[1] stores the children that always evaluate to pol, - * v[0] stores the children that both evaluate to true and false for at least - * one example. - */ - void getLeaves(const std::vector<Node>& vals, - bool pol, - std::map<int, std::vector<Node> >& v); - /** is this trie empty? */ - bool isEmpty() { return d_term.isNull() && d_children.empty(); } - /** clear this trie */ - void clear() - { - d_term = Node::null(); - d_children.clear(); - } - - private: - /** the term at this node */ - Node d_term; - /** the children nodes of this trie */ - std::map<Node, SubsumeTrie> d_children; - /** helper function for above functions */ - Node addTermInternal(Node t, - const std::vector<Node>& vals, - bool pol, - std::vector<Node>& subsumed, - bool spol, - unsigned index, - int status, - bool checkExistsOnly, - bool checkSubsume); - /** helper function for above functions */ - void getLeavesInternal(const std::vector<Node>& vals, - bool pol, - std::map<int, std::vector<Node> >& v, - unsigned index, - int status); -}; - /** Sygus unification utility * * This utility implements synthesis-by-unification style approaches for a @@ -276,8 +47,6 @@ class SubsumeTrie */ class SygusUnif { - friend class UnifContext; - public: SygusUnif(); ~SygusUnif(); @@ -296,32 +65,17 @@ class SygusUnif * those that exclude ITE from enumerators whose role is enum_io when the * strategy is ITE_strat). */ - void initialize(QuantifiersEngine* qe, - Node f, - std::vector<Node>& enums, - std::vector<Node>& lemmas); - /** reset examples - * - * Reset the specification for f. - * - * Notice that this does not reset the - */ - void resetExamples(); - /** add example - * - * This adds input -> output to the specification for f. The arity of - * input should be equal to the number of arguments in the sygus variable - * list of the grammar of f. That is, if we are searching for solutions for f - * of the form (lambda v1...vn. t), then the arity of input should be n. - */ - void addExample(const std::vector<Node>& input, Node output); + virtual void initialize(QuantifiersEngine* qe, + Node f, + std::vector<Node>& enums, + std::vector<Node>& lemmas); /** * Notify that the value v has been enumerated for enumerator e. This call * will add lemmas L to lemmas such that L entails e^M != v for all future * models M. */ - void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas); + virtual void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) = 0; /** construct solution * * This attempts to construct a solution based on the current set of @@ -329,20 +83,13 @@ class SygusUnif * set of enumerated values is insufficient, or if a non-deterministic * strategy aborts). */ - Node constructSolution(); + virtual Node constructSolution(); - private: + protected: /** reference to quantifier engine */ QuantifiersEngine* d_qe; /** sygus term database of d_qe */ quantifiers::TermDbSygus* d_tds; - /** true and false nodes */ - Node d_true; - Node d_false; - /** input of I/O examples */ - std::vector<std::vector<Node> > d_examples; - /** output of I/O examples */ - std::vector<Node> d_examples_out; //-----------------------debug printing /** print ind indentations on trace c */ @@ -353,59 +100,6 @@ class SygusUnif bool pol = true); //-----------------------end debug printing - /** - * This class stores information regarding an enumerator, including: - * a database of values that have been enumerated for this enumerator. - */ - class EnumCache - { - public: - 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(Node v, std::vector<Node>& 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) { 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. */ - Node getSolved() { return d_enum_solved; } - /** Values that have been enumerated for this enumerator */ - std::vector<Node> d_enum_vals; - /** - * This either stores the values of f( I ) for inputs - * or the value of f( I ) = O if d_role==enum_io - */ - std::vector<std::vector<Node> > d_enum_vals_res; - /** - * The set of values in d_enum_vals that have been "subsumed" by others - * (see SubsumeTrie for explanation of subsumed). - */ - std::vector<Node> d_enum_subsume; - /** Map from values to their index in d_enum_vals. */ - std::map<Node, unsigned> d_enum_val_to_index; - /** - * A subsumption trie containing the values in d_enum_vals. Depending on the - * role of this enumerator, values may either be added to d_term_trie with - * subsumption (if role=enum_io), or without (if role=enum_ite_condition or - * enum_concat_term). - */ - SubsumeTrie d_term_trie; - private: - /** - * Whether an enumerated value for this conjecture has solved the entire - * conjecture. - */ - Node d_enum_solved; - }; - /** maps enumerators to the information above */ - std::map<Node, EnumCache> d_ecache; /** * Whether we will try to construct solution on the next call to @@ -452,37 +146,41 @@ class SygusUnif std::map<Node, bool> d_use_str_contains_eexc; //------------------------------ constructing solutions - /** helper function for construct solution. + /** implementation-dependent initialize construct solution + * + * Called once before each attempt to construct solutions. + */ + virtual void initializeConstructSol() = 0; + /** implementation-dependent function for construct solution. * * Construct a solution based on enumerator e for function-to-synthesize of * this class with node role nrole in context x. * * ind is the term depth of the context (for debugging). */ - Node constructSolution(Node e, NodeRole nrole, UnifContext& x, int ind); + virtual Node constructSol(Node e, NodeRole nrole, int ind) = 0; /** Heuristically choose the best solved term from solved in context x, * currently return the first. */ - Node constructBestSolvedTerm(std::vector<Node>& solved, UnifContext& x); + virtual Node constructBestSolvedTerm(const std::vector<Node>& solved); /** Heuristically choose the best solved string term from solved in context * x, currently return the first. */ - Node constructBestStringSolvedTerm(std::vector<Node>& solved, UnifContext& x); + virtual Node constructBestStringSolvedTerm(const std::vector<Node>& solved); /** Heuristically choose the best solved conditional term from solved in * context x, currently random */ - Node constructBestSolvedConditional(std::vector<Node>& solved, - UnifContext& x); + virtual Node constructBestSolvedConditional(const std::vector<Node>& solved); /** Heuristically choose the best conditional term from conds in context x, * currently random */ - Node constructBestConditional(std::vector<Node>& conds, UnifContext& x); + virtual Node constructBestConditional(const std::vector<Node>& conds); /** Heuristically choose the best string to concatenate from strs to the * solution in context x, currently random * incr stores the vector of indices that are incremented by this solution in * example outputs. * total_inc[x] is the sum of incr[x] for each x in strs. */ - Node constructBestStringToConcat(std::vector<Node> strs, - std::map<Node, unsigned> total_inc, - std::map<Node, std::vector<unsigned> > incr, - UnifContext& x); + virtual Node constructBestStringToConcat( + const std::vector<Node>& strs, + const std::map<Node, unsigned>& total_inc, + const std::map<Node, std::vector<unsigned> >& incr); //------------------------------ end constructing solutions }; diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp new file mode 100644 index 000000000..abdaf0cb2 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -0,0 +1,1272 @@ +/********************* */ +/*! \file sygus_unif_io.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of sygus_unif_io + **/ + +#include "theory/quantifiers/sygus/sygus_unif_io.h" + +#include "theory/datatypes/datatypes_rewriter.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" +#include "util/random.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +UnifContextIo::UnifContextIo() : d_curr_role(role_invalid) +{ + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); +} + +NodeRole UnifContextIo::getCurrentRole() { return d_curr_role; } + +bool UnifContextIo::updateContext(SygusUnifIo* sui, + std::vector<Node>& vals, + bool pol) +{ + Assert(d_vals.size() == vals.size()); + bool changed = false; + Node poln = pol ? d_true : d_false; + for (unsigned i = 0; i < vals.size(); i++) + { + if (vals[i] != poln) + { + if (d_vals[i] == d_true) + { + d_vals[i] = d_false; + changed = true; + } + } + } + if (changed) + { + d_visit_role.clear(); + } + return changed; +} + +bool UnifContextIo::updateStringPosition(SygusUnifIo* sui, + std::vector<unsigned>& pos, + NodeRole nrole) +{ + Assert(pos.size() == d_str_pos.size()); + bool changed = false; + for (unsigned i = 0; i < pos.size(); i++) + { + if (pos[i] > 0) + { + d_str_pos[i] += pos[i]; + changed = true; + } + } + if (changed) + { + d_visit_role.clear(); + } + d_curr_role = nrole; + return changed; +} + +void UnifContextIo::initialize(SygusUnifIo* sui) +{ + // clear previous data + d_vals.clear(); + d_str_pos.clear(); + d_curr_role = role_equal; + d_visit_role.clear(); + d_uinfo.clear(); + + // initialize with #examples + unsigned sz = sui->d_examples.size(); + for (unsigned i = 0; i < sz; i++) + { + d_vals.push_back(d_true); + } + + if (!sui->d_examples_out.empty()) + { + // output type of the examples + TypeNode exotn = sui->d_examples_out[0].getType(); + + if (exotn.isString()) + { + for (unsigned i = 0; i < sz; i++) + { + d_str_pos.push_back(0); + } + } + } + d_visit_role.clear(); +} + +void UnifContextIo::getCurrentStrings(SygusUnifIo* sui, + const std::vector<Node>& vals, + std::vector<String>& ex_vals) +{ + bool isPrefix = d_curr_role == role_string_prefix; + String dummy; + for (unsigned i = 0; i < vals.size(); i++) + { + if (d_vals[i] == sui->d_true) + { + Assert(vals[i].isConst()); + unsigned pos_value = d_str_pos[i]; + if (pos_value > 0) + { + Assert(d_curr_role != role_invalid); + String s = vals[i].getConst<String>(); + Assert(pos_value <= s.size()); + ex_vals.push_back(isPrefix ? s.suffix(s.size() - pos_value) + : s.prefix(s.size() - pos_value)); + } + else + { + ex_vals.push_back(vals[i].getConst<String>()); + } + } + else + { + // irrelevant, add dummy + ex_vals.push_back(dummy); + } + } +} + +bool UnifContextIo::getStringIncrement(SygusUnifIo* sui, + bool isPrefix, + const std::vector<String>& ex_vals, + const std::vector<Node>& vals, + std::vector<unsigned>& inc, + unsigned& tot) +{ + for (unsigned j = 0; j < vals.size(); j++) + { + unsigned ival = 0; + if (d_vals[j] == sui->d_true) + { + // example is active in this context + Assert(vals[j].isConst()); + String mystr = vals[j].getConst<String>(); + ival = mystr.size(); + if (mystr.size() <= ex_vals[j].size()) + { + if (!(isPrefix ? ex_vals[j].strncmp(mystr, ival) + : ex_vals[j].rstrncmp(mystr, ival))) + { + Trace("sygus-sui-dt-debug") << "X"; + return false; + } + } + else + { + Trace("sygus-sui-dt-debug") << "X"; + return false; + } + } + Trace("sygus-sui-dt-debug") << ival; + tot += ival; + inc.push_back(ival); + } + return true; +} +bool UnifContextIo::isStringSolved(SygusUnifIo* sui, + const std::vector<String>& ex_vals, + const std::vector<Node>& vals) +{ + for (unsigned j = 0; j < vals.size(); j++) + { + if (d_vals[j] == sui->d_true) + { + // example is active in this context + Assert(vals[j].isConst()); + String mystr = vals[j].getConst<String>(); + if (ex_vals[j] != mystr) + { + return false; + } + } + } + return true; +} + +// status : 0 : exact, -1 : vals is subset, 1 : vals is superset +Node SubsumeTrie::addTermInternal(Node t, + const std::vector<Node>& vals, + bool pol, + std::vector<Node>& subsumed, + bool spol, + unsigned index, + int status, + bool checkExistsOnly, + bool checkSubsume) +{ + if (index == vals.size()) + { + if (status == 0) + { + // set the term if checkExistsOnly = false + if (d_term.isNull() && !checkExistsOnly) + { + d_term = t; + } + } + else if (status == 1) + { + Assert(checkSubsume); + // found a subsumed term + if (!d_term.isNull()) + { + subsumed.push_back(d_term); + if (!checkExistsOnly) + { + // remove it if checkExistsOnly = false + d_term = Node::null(); + } + } + } + else + { + Assert(!checkExistsOnly && checkSubsume); + } + return d_term; + } + NodeManager* nm = NodeManager::currentNM(); + // the current value + Assert(pol || (vals[index].isConst() && vals[index].getType().isBoolean())); + Node cv = pol ? vals[index] : nm->mkConst(!vals[index].getConst<bool>()); + // if checkExistsOnly = false, check if the current value is subsumed if + // checkSubsume = true, if so, don't add + if (!checkExistsOnly && checkSubsume) + { + Assert(cv.isConst() && cv.getType().isBoolean()); + std::vector<bool> check_subsumed_by; + if (status == 0) + { + if (!cv.getConst<bool>()) + { + check_subsumed_by.push_back(spol); + } + } + else if (status == -1) + { + check_subsumed_by.push_back(spol); + if (!cv.getConst<bool>()) + { + check_subsumed_by.push_back(!spol); + } + } + // check for subsumed nodes + for (unsigned i = 0, size = check_subsumed_by.size(); i < size; i++) + { + bool csbi = check_subsumed_by[i]; + Node csval = nm->mkConst(csbi); + // check if subsumed + std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval); + if (itc != d_children.end()) + { + Node ret = itc->second.addTermInternal(t, + vals, + pol, + subsumed, + spol, + index + 1, + -1, + checkExistsOnly, + checkSubsume); + // ret subsumes t + if (!ret.isNull()) + { + return ret; + } + } + } + } + Node ret; + std::vector<bool> check_subsume; + if (status == 0) + { + if (checkExistsOnly) + { + std::map<Node, SubsumeTrie>::iterator itc = d_children.find(cv); + if (itc != d_children.end()) + { + ret = itc->second.addTermInternal(t, + vals, + pol, + subsumed, + spol, + index + 1, + 0, + checkExistsOnly, + checkSubsume); + } + } + else + { + Assert(spol); + ret = d_children[cv].addTermInternal(t, + vals, + pol, + subsumed, + spol, + index + 1, + 0, + checkExistsOnly, + checkSubsume); + if (ret != t) + { + // we were subsumed by ret, return + return ret; + } + } + if (checkSubsume) + { + Assert(cv.isConst() && cv.getType().isBoolean()); + // check for subsuming + if (cv.getConst<bool>()) + { + check_subsume.push_back(!spol); + } + } + } + else if (status == 1) + { + Assert(checkSubsume); + Assert(cv.isConst() && cv.getType().isBoolean()); + check_subsume.push_back(!spol); + if (cv.getConst<bool>()) + { + check_subsume.push_back(spol); + } + } + if (checkSubsume) + { + // check for subsumed terms + for (unsigned i = 0, size = check_subsume.size(); i < size; i++) + { + Node csval = nm->mkConst<bool>(check_subsume[i]); + std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval); + if (itc != d_children.end()) + { + itc->second.addTermInternal(t, + vals, + pol, + subsumed, + spol, + index + 1, + 1, + checkExistsOnly, + checkSubsume); + // clean up + if (itc->second.isEmpty()) + { + Assert(!checkExistsOnly); + d_children.erase(csval); + } + } + } + } + return ret; +} + +Node SubsumeTrie::addTerm(Node t, + const std::vector<Node>& vals, + bool pol, + std::vector<Node>& subsumed) +{ + return addTermInternal(t, vals, pol, subsumed, true, 0, 0, false, true); +} + +Node SubsumeTrie::addCond(Node c, const std::vector<Node>& vals, bool pol) +{ + std::vector<Node> subsumed; + return addTermInternal(c, vals, pol, subsumed, true, 0, 0, false, false); +} + +void SubsumeTrie::getSubsumed(const std::vector<Node>& vals, + bool pol, + std::vector<Node>& subsumed) +{ + addTermInternal(Node::null(), vals, pol, subsumed, true, 0, 1, true, true); +} + +void SubsumeTrie::getSubsumedBy(const std::vector<Node>& vals, + bool pol, + std::vector<Node>& subsumed_by) +{ + // flip polarities + addTermInternal( + Node::null(), vals, !pol, subsumed_by, false, 0, 1, true, true); +} + +void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals, + bool pol, + std::map<int, std::vector<Node> >& v, + unsigned index, + int status) +{ + if (index == vals.size()) + { + Assert(!d_term.isNull()); + Assert(std::find(v[status].begin(), v[status].end(), d_term) + == v[status].end()); + v[status].push_back(d_term); + } + else + { + Assert(vals[index].isConst() && vals[index].getType().isBoolean()); + bool curr_val_true = vals[index].getConst<bool>() == pol; + for (std::map<Node, SubsumeTrie>::iterator it = d_children.begin(); + it != d_children.end(); + ++it) + { + int new_status = status; + // if the current value is true + if (curr_val_true) + { + if (status != 0) + { + Assert(it->first.isConst() && it->first.getType().isBoolean()); + new_status = (it->first.getConst<bool>() ? 1 : -1); + if (status != -2 && new_status != status) + { + new_status = 0; + } + } + } + it->second.getLeavesInternal(vals, pol, v, index + 1, new_status); + } + } +} + +void SubsumeTrie::getLeaves(const std::vector<Node>& vals, + bool pol, + std::map<int, std::vector<Node> >& v) +{ + getLeavesInternal(vals, pol, v, 0, -2); +} + +SygusUnifIo::SygusUnifIo() +{ + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); +} + +SygusUnifIo::~SygusUnifIo() {} + +void SygusUnifIo::initialize(QuantifiersEngine* qe, + Node f, + std::vector<Node>& enums, + std::vector<Node>& lemmas) +{ + d_examples.clear(); + d_examples_out.clear(); + d_ecache.clear(); + SygusUnif::initialize(qe, f, enums, lemmas); +} + +void SygusUnifIo::addExample(const std::vector<Node>& input, Node output) +{ + d_examples.push_back(input); + d_examples_out.push_back(output); +} + +void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) +{ + Trace("sygus-sui-enum") << "Notify enumeration for " << e << " : " << v + << std::endl; + Node c = d_candidate; + Assert(!d_examples.empty()); + Assert(d_examples.size() == d_examples_out.size()); + + EnumInfo& ei = d_strategy.getEnumInfo(e); + // The explanation for why the current value should be excluded in future + // iterations. + Node exp_exc; + + TypeNode xtn = e.getType(); + Node bv = d_tds->sygusToBuiltin(v, xtn); + std::vector<Node> base_results; + // compte the results + for (unsigned j = 0, size = d_examples.size(); j < size; j++) + { + Node res = d_tds->evaluateBuiltin(xtn, bv, d_examples[j]); + Trace("sygus-sui-enum-debug") + << "...got res = " << res << " from " << bv << std::endl; + base_results.push_back(res); + } + // is it excluded for domain-specific reason? + std::vector<Node> exp_exc_vec; + if (getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec)) + { + Assert(!exp_exc_vec.empty()); + exp_exc = exp_exc_vec.size() == 1 + ? exp_exc_vec[0] + : NodeManager::currentNM()->mkNode(AND, exp_exc_vec); + Trace("sygus-sui-enum") + << " ...fail : term is excluded (domain-specific)" << std::endl; + } + else + { + // notify all slaves + Assert(!ei.d_enum_slave.empty()); + // explanation for why this value should be excluded + for (unsigned s = 0; s < ei.d_enum_slave.size(); s++) + { + Node xs = ei.d_enum_slave[s]; + + EnumInfo& eiv = d_strategy.getEnumInfo(xs); + + EnumCache& ecv = d_ecache[xs]; + + Trace("sygus-sui-enum") << "Process " << xs << " from " << s << std::endl; + // bool prevIsCover = false; + if (eiv.getRole() == enum_io) + { + Trace("sygus-sui-enum") << " IO-Eval of "; + // prevIsCover = eiv.isFeasible(); + } + else + { + Trace("sygus-sui-enum") << "Evaluation of "; + } + Trace("sygus-sui-enum") << xs << " : "; + // evaluate all input/output examples + std::vector<Node> results; + Node templ = eiv.d_template; + TNode templ_var = eiv.d_template_arg; + std::map<Node, bool> cond_vals; + for (unsigned j = 0, size = base_results.size(); j < size; j++) + { + Node res = base_results[j]; + Assert(res.isConst()); + if (!templ.isNull()) + { + TNode tres = res; + res = templ.substitute(templ_var, res); + res = Rewriter::rewrite(res); + Assert(res.isConst()); + } + Node resb; + if (eiv.getRole() == enum_io) + { + Node out = d_examples_out[j]; + Assert(out.isConst()); + resb = res == out ? d_true : d_false; + } + else + { + resb = res; + } + cond_vals[resb] = true; + results.push_back(resb); + if (Trace.isOn("sygus-sui-enum")) + { + if (resb.getType().isBoolean()) + { + Trace("sygus-sui-enum") << (resb == d_true ? "1" : "0"); + } + else + { + Trace("sygus-sui-enum") << "?"; + } + } + } + bool keep = false; + 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()) + { + // check subsumbed/subsuming + std::vector<Node> subsume; + if (cond_vals.find(d_false) == cond_vals.end()) + { + // it is the entire solution, we are done + Trace("sygus-sui-enum") + << " ...success, full solution added to PBE pool : " + << d_tds->sygusToBuiltin(v) << std::endl; + if (!ecv.isSolved()) + { + ecv.setSolved(v); + // it subsumes everything + ecv.d_term_trie.clear(); + ecv.d_term_trie.addTerm(v, results, true, subsume); + } + keep = true; + } + else + { + Node val = ecv.d_term_trie.addTerm(v, results, true, subsume); + if (val == v) + { + Trace("sygus-sui-enum") << " ...success"; + if (!subsume.empty()) + { + ecv.d_enum_subsume.insert( + ecv.d_enum_subsume.end(), subsume.begin(), subsume.end()); + Trace("sygus-sui-enum") + << " and subsumed " << subsume.size() << " terms"; + } + Trace("sygus-sui-enum") + << "! add to PBE pool : " << d_tds->sygusToBuiltin(v) + << std::endl; + keep = true; + } + else + { + Assert(subsume.empty()); + Trace("sygus-sui-enum") << " ...fail : subsumed" << std::endl; + } + } + } + else + { + Trace("sygus-sui-enum") + << " ...fail : it does not satisfy examples." << std::endl; + } + } + else + { + // must be unique up to examples + Node val = ecv.d_term_trie.addCond(v, results, true); + if (val == v) + { + Trace("sygus-sui-enum") << " ...success! add to PBE pool : " + << d_tds->sygusToBuiltin(v) << std::endl; + keep = true; + } + else + { + Trace("sygus-sui-enum") + << " ...fail : term is not unique" << std::endl; + } + d_cond_count++; + } + if (keep) + { + // notify to retry the build of solution + d_check_sol = true; + ecv.addEnumValue(v, results); + } + } + } + + // exclude this value on subsequent iterations + if (exp_exc.isNull()) + { + // if we did not already explain why this should be excluded, use default + exp_exc = d_tds->getExplain()->getExplanationForEquality(e, v); + } + exp_exc = exp_exc.negate(); + Trace("sygus-sui-enum-lemma") + << "SygusUnifIo : enumeration exclude lemma : " << exp_exc << std::endl; + lemmas.push_back(exp_exc); +} + +// ------------------------------------ solution construction from enumeration + +bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e) +{ + TypeNode xbt = d_tds->sygusToBuiltinType(e.getType()); + if (xbt.isString()) + { + std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(e); + if (itx != d_use_str_contains_eexc.end()) + { + return itx->second; + } + Trace("sygus-sui-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) + { + EnumInfo& eis = d_strategy.getEnumInfo(sn); + EnumRole er = eis.getRole(); + if (er != enum_io && er != enum_concat_term) + { + Trace("sygus-sui-enum-debug") << " incompatible slave : " << sn + << ", role = " << er << std::endl; + d_use_str_contains_eexc[e] = false; + return false; + } + if (eis.isConditional()) + { + Trace("sygus-sui-enum-debug") + << " conditional slave : " << sn << std::endl; + d_use_str_contains_eexc[e] = false; + return false; + } + } + Trace("sygus-sui-enum-debug") + << "...can use str.contains exclusion." << std::endl; + return d_use_str_contains_eexc[e]; + } + return false; +} + +bool SygusUnifIo::getExplanationForEnumeratorExclude(Node e, + Node v, + std::vector<Node>& results, + std::vector<Node>& exp) +{ + if (useStrContainsEnumeratorExclude(e)) + { + NodeManager* nm = NodeManager::currentNM(); + // This check whether the example evaluates to something that is larger than + // the output for some input/output pair. If so, then this term is never + // useful. We generalize its explanation below. + + if (Trace.isOn("sygus-sui-cterm-debug")) + { + Trace("sygus-sui-enum") << std::endl; + } + // check if all examples had longer length that the output + Assert(d_examples_out.size() == results.size()); + Trace("sygus-sui-cterm-debug") + << "Check enumerator exclusion for " << e << " -> " + << d_tds->sygusToBuiltin(v) << " based on str.contains." << std::endl; + std::vector<unsigned> cmp_indices; + for (unsigned i = 0, size = results.size(); i < size; i++) + { + Assert(results[i].isConst()); + Assert(d_examples_out[i].isConst()); + Trace("sygus-sui-cterm-debug") + << " " << results[i] << " <> " << d_examples_out[i]; + Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]); + Node contr = Rewriter::rewrite(cont); + if (contr == d_false) + { + cmp_indices.push_back(i); + Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl; + } + else + { + Trace("sygus-sui-cterm-debug") << "...contained." << std::endl; + } + } + if (!cmp_indices.empty()) + { + // we check invariance with respect to a negative contains test + NegContainsSygusInvarianceTest ncset; + ncset.init(e, d_examples, d_examples_out, cmp_indices); + // construct the generalized explanation + d_tds->getExplain()->getExplanationFor(e, v, exp, ncset); + Trace("sygus-sui-cterm") + << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin(v) + << " due to negative containment." << std::endl; + return true; + } + } + return false; +} + +void SygusUnifIo::EnumCache::addEnumValue(Node v, std::vector<Node>& results) +{ + // should not have been enumerated before + Assert(d_enum_val_to_index.find(v) == d_enum_val_to_index.end()); + d_enum_val_to_index[v] = d_enum_vals.size(); + d_enum_vals.push_back(v); + d_enum_vals_res.push_back(results); +} + +void SygusUnifIo::initializeConstructSol() { d_context.initialize(this); } + +Node SygusUnifIo::constructSol(Node e, NodeRole nrole, int ind) +{ + UnifContextIo& x = d_context; + TypeNode etn = e.getType(); + if (Trace.isOn("sygus-sui-dt-debug")) + { + indent("sygus-sui-dt-debug", ind); + Trace("sygus-sui-dt-debug") << "ConstructPBE: (" << e << ", " << nrole + << ") for type " << etn << " in context "; + print_val("sygus-sui-dt-debug", x.d_vals); + NodeRole ctx_role = x.getCurrentRole(); + Trace("sygus-sui-dt-debug") << ", context role [" << ctx_role; + if (ctx_role == role_string_prefix || ctx_role == role_string_suffix) + { + Trace("sygus-sui-dt-debug") << ", string pos : "; + for (unsigned i = 0, size = x.d_str_pos.size(); i < size; i++) + { + Trace("sygus-sui-dt-debug") << " " << x.d_str_pos[i]; + } + } + Trace("sygus-sui-dt-debug") << "]"; + Trace("sygus-sui-dt-debug") << std::endl; + } + // enumerator type info + EnumTypeInfo& tinfo = d_strategy.getEnumTypeInfo(etn); + + // get the enumerator information + EnumInfo& einfo = d_strategy.getEnumInfo(e); + + EnumCache& ecache = d_ecache[e]; + + Node ret_dt; + if (nrole == role_equal) + { + if (!x.isReturnValueModified()) + { + if (ecache.isSolved()) + { + // this type has a complete solution + ret_dt = ecache.getSolved(); + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "return PBE: success : solved " + << d_tds->sygusToBuiltin(ret_dt) << std::endl; + Assert(!ret_dt.isNull()); + } + else + { + // could be conditionally solved + std::vector<Node> subsumed_by; + ecache.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by); + if (!subsumed_by.empty()) + { + ret_dt = constructBestSolvedTerm(subsumed_by); + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "return PBE: success : conditionally solved" + << d_tds->sygusToBuiltin(ret_dt) << std::endl; + } + else + { + indent("sygus-sui-dt-debug", ind); + Trace("sygus-sui-dt-debug") + << " ...not currently conditionally solved." << std::endl; + } + } + } + if (ret_dt.isNull()) + { + if (d_tds->sygusToBuiltinType(e.getType()).isString()) + { + // check if a current value that closes all examples + // get the term enumerator for this type + std::map<EnumRole, Node>::iterator itnt = + tinfo.d_enum.find(enum_concat_term); + if (itnt != tinfo.d_enum.end()) + { + Node et = itnt->second; + + EnumCache& ecachet = d_ecache[et]; + // get the current examples + std::vector<String> ex_vals; + x.getCurrentStrings(this, d_examples_out, ex_vals); + Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size()); + + // test each example in the term enumerator for the type + std::vector<Node> str_solved; + for (unsigned i = 0, size = ecachet.d_enum_vals.size(); i < size; i++) + { + if (x.isStringSolved(this, ex_vals, ecachet.d_enum_vals_res[i])) + { + str_solved.push_back(ecachet.d_enum_vals[i]); + } + } + if (!str_solved.empty()) + { + ret_dt = constructBestStringSolvedTerm(str_solved); + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "return PBE: success : string solved " + << d_tds->sygusToBuiltin(ret_dt) << std::endl; + } + else + { + indent("sygus-sui-dt-debug", ind); + Trace("sygus-sui-dt-debug") + << " ...not currently string solved." << std::endl; + } + } + } + } + } + else if (nrole == role_string_prefix || nrole == role_string_suffix) + { + // check if each return value is a prefix/suffix of all open examples + if (!x.isReturnValueModified() || x.getCurrentRole() == nrole) + { + std::map<Node, std::vector<unsigned> > incr; + bool isPrefix = nrole == role_string_prefix; + std::map<Node, unsigned> total_inc; + std::vector<Node> inc_strs; + // make the value of the examples + std::vector<String> ex_vals; + x.getCurrentStrings(this, d_examples_out, ex_vals); + if (Trace.isOn("sygus-sui-dt-debug")) + { + indent("sygus-sui-dt-debug", ind); + Trace("sygus-sui-dt-debug") << "current strings : " << std::endl; + for (unsigned i = 0, size = ex_vals.size(); i < size; i++) + { + indent("sygus-sui-dt-debug", ind + 1); + Trace("sygus-sui-dt-debug") << ex_vals[i] << std::endl; + } + } + + // check if there is a value for which is a prefix/suffix of all active + // examples + Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size()); + + for (unsigned i = 0, size = ecache.d_enum_vals.size(); i < size; i++) + { + Node val_t = ecache.d_enum_vals[i]; + Assert(incr.find(val_t) == incr.end()); + indent("sygus-sui-dt-debug", ind); + Trace("sygus-sui-dt-debug") + << "increment string values : " << val_t << " : "; + Assert(ecache.d_enum_vals_res[i].size() == d_examples_out.size()); + unsigned tot = 0; + bool exsuccess = x.getStringIncrement(this, + isPrefix, + ex_vals, + ecache.d_enum_vals_res[i], + incr[val_t], + tot); + if (!exsuccess) + { + incr.erase(val_t); + Trace("sygus-sui-dt-debug") << "...fail" << std::endl; + } + else + { + total_inc[val_t] = tot; + inc_strs.push_back(val_t); + Trace("sygus-sui-dt-debug") + << "...success, total increment = " << tot << std::endl; + } + } + + if (!incr.empty()) + { + ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr); + Assert(!ret_dt.isNull()); + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") + << "PBE: CONCAT strategy : choose " << (isPrefix ? "pre" : "suf") + << "fix value " << d_tds->sygusToBuiltin(ret_dt) << std::endl; + // update the context + bool ret = x.updateStringPosition(this, incr[ret_dt], nrole); + AlwaysAssert(ret == (total_inc[ret_dt] > 0)); + } + else + { + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "PBE: failed CONCAT strategy, no values are " + << (isPrefix ? "pre" : "suf") + << "fix of all examples." << std::endl; + } + } + else + { + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") + << "PBE: failed CONCAT strategy, prefix/suffix mismatch." + << std::endl; + } + } + if (ret_dt.isNull() && !einfo.isTemplated()) + { + // we will try a single strategy + EnumTypeInfoStrat* etis = nullptr; + std::map<NodeRole, StrategyNode>::iterator itsn = + tinfo.d_snodes.find(nrole); + if (itsn != tinfo.d_snodes.end()) + { + // strategy info + StrategyNode& snode = itsn->second; + if (x.d_visit_role[e].find(nrole) == x.d_visit_role[e].end()) + { + x.d_visit_role[e][nrole] = true; + // try a random strategy + if (snode.d_strats.size() > 1) + { + std::random_shuffle(snode.d_strats.begin(), snode.d_strats.end()); + } + // get an eligible strategy index + unsigned sindex = 0; + while (sindex < snode.d_strats.size() + && !snode.d_strats[sindex]->isValid(x)) + { + sindex++; + } + // if we found a eligible strategy + if (sindex < snode.d_strats.size()) + { + etis = snode.d_strats[sindex]; + } + } + } + if (etis != nullptr) + { + StrategyType strat = etis->d_this; + indent("sygus-sui-dt", ind + 1); + Trace("sygus-sui-dt") + << "...try STRATEGY " << strat << "..." << std::endl; + + std::map<unsigned, Node> look_ahead_solved_children; + std::vector<Node> dt_children_cons; + bool success = true; + + // for ITE + Node split_cond_enum; + int split_cond_res_index = -1; + + for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++) + { + indent("sygus-sui-dt", ind + 1); + Trace("sygus-sui-dt") + << "construct PBE child #" << sc << "..." << std::endl; + Node rec_c; + std::map<unsigned, Node>::iterator itla = + look_ahead_solved_children.find(sc); + if (itla != look_ahead_solved_children.end()) + { + rec_c = itla->second; + indent("sygus-sui-dt-debug", ind + 1); + Trace("sygus-sui-dt-debug") + << "ConstructPBE: look ahead solved : " + << d_tds->sygusToBuiltin(rec_c) << std::endl; + } + else + { + std::pair<Node, NodeRole>& cenum = etis->d_cenum[sc]; + + // update the context + std::vector<Node> prev; + if (strat == strat_ITE && sc > 0) + { + EnumCache& ecache_cond = d_ecache[split_cond_enum]; + Assert(split_cond_res_index >= 0); + Assert(split_cond_res_index + < (int)ecache_cond.d_enum_vals_res.size()); + prev = x.d_vals; + bool ret = x.updateContext( + this, + ecache_cond.d_enum_vals_res[split_cond_res_index], + sc == 1); + AlwaysAssert(ret); + } + + // recurse + if (strat == strat_ITE && sc == 0) + { + Node ce = cenum.first; + + EnumCache& ecache_child = d_ecache[ce]; + + // only used if the return value is not modified + if (!x.isReturnValueModified()) + { + if (x.d_uinfo.find(ce) == x.d_uinfo.end()) + { + Trace("sygus-sui-dt-debug2") + << " reg : PBE: Look for direct solutions for conditional " + "enumerator " + << ce << " ... " << std::endl; + Assert(ecache_child.d_enum_vals.size() + == ecache_child.d_enum_vals_res.size()); + for (unsigned i = 1; i <= 2; i++) + { + std::pair<Node, NodeRole>& te_pair = etis->d_cenum[i]; + Node te = te_pair.first; + 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 = ecache_child.d_enum_vals.size(); + k < size; + k++) + { + Node cond = ecache_child.d_enum_vals[k]; + std::vector<Node> solved; + ecache_te.d_term_trie.getSubsumedBy( + ecache_child.d_enum_vals_res[k], branch_pol, solved); + Trace("sygus-sui-dt-debug2") + << " reg : PBE: " << d_tds->sygusToBuiltin(cond) + << " has " << solved.size() << " solutions in branch " + << i << std::endl; + if (!solved.empty()) + { + Node slv = constructBestSolvedTerm(solved); + Trace("sygus-sui-dt-debug2") + << " reg : PBE: ..." << d_tds->sygusToBuiltin(slv) + << " is a solution under branch " << i; + Trace("sygus-sui-dt-debug2") + << " of condition " << d_tds->sygusToBuiltin(cond) + << std::endl; + x.d_uinfo[ce].d_look_ahead_sols[cond][i] = slv; + } + } + } + } + } + + // get the conditionals in the current context : they must be + // distinguishable + std::map<int, std::vector<Node> > possible_cond; + std::map<Node, int> solved_cond; // stores branch + ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond); + + std::map<int, std::vector<Node> >::iterator itpc = + possible_cond.find(0); + if (itpc != possible_cond.end()) + { + if (Trace.isOn("sygus-sui-dt-debug")) + { + indent("sygus-sui-dt-debug", ind + 1); + Trace("sygus-sui-dt-debug") + << "PBE : We have " << itpc->second.size() + << " distinguishable conditionals:" << std::endl; + for (Node& cond : itpc->second) + { + indent("sygus-sui-dt-debug", ind + 2); + Trace("sygus-sui-dt-debug") + << d_tds->sygusToBuiltin(cond) << std::endl; + } + } + + // static look ahead conditional : choose conditionals that have + // solved terms in at least one branch + // only applicable if we have not modified the return value + std::map<int, std::vector<Node> > solved_cond; + if (!x.isReturnValueModified()) + { + Assert(x.d_uinfo.find(ce) != x.d_uinfo.end()); + int solve_max = 0; + for (Node& cond : itpc->second) + { + std::map<Node, std::map<unsigned, Node> >::iterator itla = + x.d_uinfo[ce].d_look_ahead_sols.find(cond); + if (itla != x.d_uinfo[ce].d_look_ahead_sols.end()) + { + int nsolved = itla->second.size(); + solve_max = nsolved > solve_max ? nsolved : solve_max; + solved_cond[nsolved].push_back(cond); + } + } + int n = solve_max; + while (n > 0) + { + if (!solved_cond[n].empty()) + { + rec_c = constructBestSolvedConditional(solved_cond[n]); + indent("sygus-sui-dt", ind + 1); + Trace("sygus-sui-dt") + << "PBE: ITE strategy : choose solved conditional " + << d_tds->sygusToBuiltin(rec_c) << " with " << n + << " solved children..." << std::endl; + std::map<Node, std::map<unsigned, Node> >::iterator itla = + x.d_uinfo[ce].d_look_ahead_sols.find(rec_c); + Assert(itla != x.d_uinfo[ce].d_look_ahead_sols.end()); + for (std::pair<const unsigned, Node>& las : itla->second) + { + look_ahead_solved_children[las.first] = las.second; + } + break; + } + n--; + } + } + + // otherwise, guess a conditional + if (rec_c.isNull()) + { + rec_c = constructBestConditional(itpc->second); + Assert(!rec_c.isNull()); + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") + << "PBE: ITE strategy : choose random conditional " + << d_tds->sygusToBuiltin(rec_c) << std::endl; + } + } + else + { + // TODO (#1250) : degenerate case where children have different + // types? + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, " + "cannot find a distinguishable condition" + << std::endl; + } + if (!rec_c.isNull()) + { + 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)ecache_child.d_enum_vals_res.size()); + } + } + else + { + rec_c = constructSol(cenum.first, cenum.second, ind + 2); + } + + // undo update the context + if (strat == strat_ITE && sc > 0) + { + x.d_vals = prev; + } + } + if (!rec_c.isNull()) + { + dt_children_cons.push_back(rec_c); + } + else + { + success = false; + break; + } + } + if (success) + { + Assert(dt_children_cons.size() == etis->d_sol_templ_args.size()); + // ret_dt = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, + // dt_children ); + ret_dt = etis->d_sol_templ; + ret_dt = ret_dt.substitute(etis->d_sol_templ_args.begin(), + etis->d_sol_templ_args.end(), + dt_children_cons.begin(), + dt_children_cons.end()); + indent("sygus-sui-dt-debug", ind); + Trace("sygus-sui-dt-debug") + << "PBE: success : constructed for strategy " << strat << std::endl; + } + else + { + indent("sygus-sui-dt-debug", ind); + Trace("sygus-sui-dt-debug") + << "PBE: failed for strategy " << strat << std::endl; + } + } + } + + if (!ret_dt.isNull()) + { + Assert(ret_dt.getType() == e.getType()); + } + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "ConstructPBE: returned " << ret_dt << std::endl; + return ret_dt; +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h new file mode 100644 index 000000000..94fb2e754 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -0,0 +1,388 @@ +/********************* */ +/*! \file sygus_unif_io.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief sygus_unif_io + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H + +#include <map> +#include "theory/quantifiers/sygus/sygus_unif.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class SygusUnifIo; + +/** Unification context + * + * This class maintains state information during calls to + * SygusUnifIo::constructSolution, which implements unification-based + * approaches for constructing solutions to synthesis conjectures. + */ +class UnifContextIo : public UnifContext +{ + public: + UnifContextIo(); + /** get current role */ + virtual NodeRole getCurrentRole() override; + + /** + * This intiializes this context based on information in sui regarding the + * kinds of examples it contains. + */ + void initialize(SygusUnifIo* sui); + + //----------for ITE strategy + /** the value of the context conditional + * + * This stores a list of Boolean constants that is the same length of the + * number of input/output example pairs we are considering. For each i, + * if d_vals[i] = true, i/o pair #i is active according to this context + * if d_vals[i] = false, i/o pair #i is inactive according to this context + */ + std::vector<Node> d_vals; + /** update the examples + * + * if pol=true, this method updates d_vals to d_vals & vals + * if pol=false, this method updates d_vals to d_vals & ( ~vals ) + */ + bool updateContext(SygusUnifIo* sui, std::vector<Node>& vals, bool pol); + //----------end for ITE strategy + + //----------for CONCAT strategies + /** the position in the strings + * + * For each i/o example pair, this stores the length of the current solution + * for the input of the pair, where the solution for that input is a prefix + * or + * suffix of the output of the pair. For example, if our i/o pairs are: + * f( "abcd" ) = "abcdcd" + * f( "aa" ) = "aacd" + * If the solution we have currently constructed is str.++( x1, "c", ... ), + * then d_str_pos = ( 5, 3 ), where notice that + * str.++( "abc", "c" ) is a prefix of "abcdcd" and + * str.++( "aa", "c" ) is a prefix of "aacd". + */ + std::vector<unsigned> d_str_pos; + /** update the string examples + * + * This method updates d_str_pos to d_str_pos + pos, and updates the current + * role to nrole. + */ + bool updateStringPosition(SygusUnifIo* sui, + std::vector<unsigned>& pos, + NodeRole nrole); + /** get current strings + * + * This returns the prefix/suffix of the string constants stored in vals + * of size d_str_pos, and stores the result in ex_vals. For example, if vals + * is (abcdcd", "aacde") and d_str_pos = ( 5, 3 ), then we add + * "d" and "de" to ex_vals. + */ + void getCurrentStrings(SygusUnifIo* sui, + const std::vector<Node>& vals, + std::vector<String>& ex_vals); + /** get string increment + * + * If this method returns true, then inc and tot are updated such that + * for all active indices i, + * vals[i] is a prefix (or suffix if isPrefix=false) of ex_vals[i], and + * inc[i] = str.len(vals[i]) + * for all inactive indices i, inc[i] = 0 + * We set tot to the sum of inc[i] for i=1,...,n. This indicates the total + * number of characters incremented across all examples. + */ + bool getStringIncrement(SygusUnifIo* sui, + bool isPrefix, + const std::vector<String>& ex_vals, + const std::vector<Node>& vals, + std::vector<unsigned>& inc, + unsigned& tot); + /** returns true if ex_vals[i] = vals[i] for all active indices i. */ + bool isStringSolved(SygusUnifIo* sui, + const std::vector<String>& ex_vals, + const std::vector<Node>& vals); + //----------end for CONCAT strategies + + /** visited role + * + * This is the current set of enumerator/node role pairs we are currently + * visiting. This set is cleared when the context is updated. + */ + std::map<Node, std::map<NodeRole, bool> > d_visit_role; + + /** unif context enumerator information */ + class UEnumInfo + { + public: + UEnumInfo() {} + /** map from conditions and branch positions to a solved node + * + * For example, if we have: + * f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 + * Then, valid entries in this map is: + * d_look_ahead_sols[x>0][1] = x+1 + * d_look_ahead_sols[x>0][2] = 1 + * For the first entry, notice that for all input examples such that x>0 + * evaluates to true, which are (1) and (3), we have that their output + * values for x+1 under the substitution that maps x to the input value, + * resulting in 2 and 4, are equal to the output value for the respective + * pairs. + */ + std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols; + }; + /** map from enumerators to the above info class */ + std::map<Node, UEnumInfo> d_uinfo; + + private: + /** true and false nodes */ + Node d_true; + Node d_false; + /** current role (see getCurrentRole). */ + NodeRole d_curr_role; +}; + +/** Subsumption trie +* +* This class manages a set of terms for a PBE sygus enumerator. +* +* In PBE sygus, we are interested in, for each term t, the set of I/O examples +* that it satisfies, which can be represented by a vector of Booleans. +* For example, given conjecture: +* f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 ^ f( 5 ) = 5 +* If solutions for f are of the form (lambda x. [term]), then: +* Term x satisfies 0001, +* Term x+1 satisfies 1100, +* Term 2 satisfies 0100. +* Above, term 2 is subsumed by term x+1, since the set of I/O examples that +* x+1 satisfies are a superset of those satisfied by 2. +*/ +class SubsumeTrie +{ + public: + SubsumeTrie() {} + /** + * Adds term t to the trie, removes all terms that are subsumed by t from the + * trie and adds them to subsumed. The set of I/O examples that t satisfies + * is given by (pol ? vals : !vals). + */ + Node addTerm(Node t, + const std::vector<Node>& vals, + bool pol, + std::vector<Node>& subsumed); + /** + * Adds term c to the trie, without calculating/updating based on + * subsumption. This is useful for using this class to store conditionals + * in ITE strategies, where any conditional whose set of vals is unique + * (as opposed to not subsumed) is useful. + */ + Node addCond(Node c, const std::vector<Node>& vals, bool pol); + /** + * Returns the set of terms that are subsumed by (pol ? vals : !vals). + */ + void getSubsumed(const std::vector<Node>& vals, + bool pol, + std::vector<Node>& subsumed); + /** + * Returns the set of terms that subsume (pol ? vals : !vals). This + * is for instance useful when determining whether there exists a term + * that satisfies all active examples in the decision tree learning + * algorithm. + */ + void getSubsumedBy(const std::vector<Node>& vals, + bool pol, + std::vector<Node>& subsumed_by); + /** + * Get the leaves of the trie, which we store in the map v. + * v[-1] stores the children that always evaluate to !pol, + * v[1] stores the children that always evaluate to pol, + * v[0] stores the children that both evaluate to true and false for at least + * one example. + */ + void getLeaves(const std::vector<Node>& vals, + bool pol, + std::map<int, std::vector<Node> >& v); + /** is this trie empty? */ + bool isEmpty() { return d_term.isNull() && d_children.empty(); } + /** clear this trie */ + void clear() + { + d_term = Node::null(); + d_children.clear(); + } + + private: + /** the term at this node */ + Node d_term; + /** the children nodes of this trie */ + std::map<Node, SubsumeTrie> d_children; + /** helper function for above functions */ + Node addTermInternal(Node t, + const std::vector<Node>& vals, + bool pol, + std::vector<Node>& subsumed, + bool spol, + unsigned index, + int status, + bool checkExistsOnly, + bool checkSubsume); + /** helper function for above functions */ + void getLeavesInternal(const std::vector<Node>& vals, + bool pol, + std::map<int, std::vector<Node> >& v, + unsigned index, + int status); +}; + +/** Sygus unification I/O utility + * + * This class implement synthesis-by-unification, where the specification is + * I/O examples. With respect to SygusUnif, it's main interface function is + * addExample, which adds an I/O example to the specification. + */ +class SygusUnifIo : public SygusUnif +{ + friend class UnifContextIo; + + public: + SygusUnifIo(); + ~SygusUnifIo(); + + /** initialize */ + virtual void initialize(QuantifiersEngine* qe, + Node f, + std::vector<Node>& enums, + std::vector<Node>& lemmas) override; + /** Notify enumeration */ + virtual void notifyEnumeration(Node e, + Node v, + std::vector<Node>& lemmas) override; + + /** add example + * + * This adds input -> output to the specification for f. The arity of + * input should be equal to the number of arguments in the sygus variable + * list of the grammar of f. That is, if we are searching for solutions for f + * of the form (lambda v1...vn. t), then the arity of input should be n. + */ + void addExample(const std::vector<Node>& input, Node output); + + protected: + /** true and false nodes */ + Node d_true; + Node d_false; + /** input of I/O examples */ + std::vector<std::vector<Node> > d_examples; + /** output of I/O examples */ + std::vector<Node> d_examples_out; + + /** + * This class stores information regarding an enumerator, including: + * a database of values that have been enumerated for this enumerator. + */ + class EnumCache + { + public: + EnumCache() {} + /** + * Notify this class that the term v has been enumerated for this enumerator. + * Its evaluation under the set of examples in sui are stored in results. + */ + void addEnumValue(Node v, std::vector<Node>& 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) { 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. */ + Node getSolved() { return d_enum_solved; } + /** Values that have been enumerated for this enumerator */ + std::vector<Node> d_enum_vals; + /** + * This either stores the values of f( I ) for inputs + * or the value of f( I ) = O if d_role==enum_io + */ + std::vector<std::vector<Node> > d_enum_vals_res; + /** + * The set of values in d_enum_vals that have been "subsumed" by others + * (see SubsumeTrie for explanation of subsumed). + */ + std::vector<Node> d_enum_subsume; + /** Map from values to their index in d_enum_vals. */ + std::map<Node, unsigned> d_enum_val_to_index; + /** + * A subsumption trie containing the values in d_enum_vals. Depending on the + * role of this enumerator, values may either be added to d_term_trie with + * subsumption (if role=enum_io), or without (if role=enum_ite_condition or + * enum_concat_term). + */ + SubsumeTrie d_term_trie; + + private: + /** + * Whether an enumerated value for this conjecture has solved the entire + * conjecture. + */ + Node d_enum_solved; + }; + /** maps enumerators to the information above */ + std::map<Node, EnumCache> d_ecache; + + /** domain-specific enumerator exclusion techniques + * + * 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, + * exp : if this function returns true, then exp contains a (possibly + * generalize) explanation for why v can be excluded. + */ + bool getExplanationForEnumeratorExclude(Node e, + Node v, + std::vector<Node>& results, + std::vector<Node>& exp); + /** returns true if we can exlude values of e based on negative str.contains + * + * 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 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 e); + /** cache for the above function */ + std::map<Node, bool> d_use_str_contains_eexc; + + /** the unification context used within constructSolution */ + UnifContextIo d_context; + /** initialize construct solution */ + void initializeConstructSol() override; + /** construct solution */ + Node constructSol(Node e, NodeRole nrole, int ind) override; +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index c397dec52..86efffd1f 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -848,11 +848,11 @@ void SygusUnifStrategy::staticLearnRedundantOps( } void EnumInfo::initialize(EnumRole role) { d_role = role; } -bool EnumTypeInfoStrat::isValid(UnifContext* x) +bool EnumTypeInfoStrat::isValid(UnifContext& x) { - if ((x->d_has_string_pos == role_string_prefix + if ((x.getCurrentRole() == role_string_prefix && d_this == strat_CONCAT_SUFFIX) - || (x->d_has_string_pos == role_string_suffix + || (x.getCurrentRole() == role_string_suffix && d_this == strat_CONCAT_PREFIX)) { return false; diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index 9a6c7ea4a..0ab7ea1d6 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -89,7 +89,27 @@ enum StrategyType }; std::ostream& operator<<(std::ostream& os, StrategyType st); -class UnifContext; +/** virtual base class for context in synthesis-by-unification approaches */ +class UnifContext +{ + public: + /** Get the current role + * + * In a particular context when constructing solutions in synthesis by + * unification, we may be solving based on a modified role. For example, + * if we are currently synthesizing x in a solution ("a" ++ x), we are + * synthesizing the string suffix of the overall solution. In this case, this + * function returns role_string_suffix. + */ + virtual NodeRole getCurrentRole() = 0; + /** is return value modified? + * + * This returns true if we are currently in a state where the return value + * of the solution has been modified, e.g. by a previous node that solved + * for a string prefix. + */ + bool isReturnValueModified() { return getCurrentRole() != role_equal; } +}; /** * This class stores information regarding an enumerator, including @@ -212,7 +232,7 @@ class EnumTypeInfoStrat /** the template for the solution */ Node d_sol_templ; /** Returns true if argument is valid strategy in unification context x */ - bool isValid(UnifContext* x); + bool isValid(UnifContext& x); }; /** |