From 585d2ac394e99a155ed40aa2da2fb550ff60fc7b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 21 Jul 2018 07:27:28 -0500 Subject: [PATCH] sygusComp2018: refactor and improve sygus io utility (#2185) --- .../quantifiers/sygus/sygus_unif_io.cpp | 216 ++++++++++++------ src/theory/quantifiers/sygus/sygus_unif_io.h | 36 ++- 2 files changed, 181 insertions(+), 71 deletions(-) diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 73a76c032..c36bdbcbf 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -14,7 +14,9 @@ #include "theory/quantifiers/sygus/sygus_unif_io.h" +#include "options/quantifiers_options.h" #include "theory/datatypes/datatypes_rewriter.h" +#include "theory/evaluator.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "util/random.h" @@ -175,9 +177,14 @@ bool UnifContextIo::getStringIncrement(SygusUnifIo* sui, Trace("sygus-sui-dt-debug") << "X"; return false; } + Trace("sygus-sui-dt-debug") << ival; + tot += ival; + } + else + { + // inactive in this context + Trace("sygus-sui-dt-debug") << "-"; } - Trace("sygus-sui-dt-debug") << ival; - tot += ival; inc.push_back(ival); } return true; @@ -459,7 +466,8 @@ void SubsumeTrie::getLeaves(const std::vector& vals, getLeavesInternal(vals, pol, v, 0, -2); } -SygusUnifIo::SygusUnifIo() : d_check_sol(false), d_cond_count(0) +SygusUnifIo::SygusUnifIo() + : d_check_sol(false), d_cond_count(0), d_sol_cons_nondet(false) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -511,6 +519,47 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) << "...got res = " << res << " from " << bv << std::endl; base_results.push_back(res); } + // get the results for each slave enumerator + std::map> srmap; + Evaluator* ev = d_tds->getEvaluator(); + bool tryEval = options::sygusEvalOpt(); + for (const Node& xs : ei.d_enum_slave) + { + Assert(srmap.find(xs) == srmap.end()); + EnumInfo& eiv = d_strategy[c].getEnumInfo(xs); + Node templ = eiv.d_template; + if (!templ.isNull()) + { + TNode templ_var = eiv.d_template_arg; + std::vector args; + args.push_back(templ_var); + std::vector sresults; + for (const Node& res : base_results) + { + TNode tres = res; + std::vector vals; + vals.push_back(tres); + Node sres; + if (tryEval) + { + sres = ev->eval(templ, args, vals); + } + if (sres.isNull()) + { + // fall back on rewriter + sres = templ.substitute(templ_var, tres); + sres = Rewriter::rewrite(sres); + } + sresults.push_back(sres); + } + srmap[xs] = sresults; + } + else + { + srmap[xs] = base_results; + } + } + // is it excluded for domain-specific reason? std::vector exp_exc_vec; if (getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec)) @@ -530,11 +579,8 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) for (unsigned s = 0; s < ei.d_enum_slave.size(); s++) { Node xs = ei.d_enum_slave[s]; - EnumInfo& eiv = d_strategy[c].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) @@ -549,20 +595,13 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) Trace("sygus-sui-enum") << xs << " : "; // evaluate all input/output examples std::vector results; - Node templ = eiv.d_template; - TNode templ_var = eiv.d_template_arg; std::map cond_vals; - for (unsigned j = 0, size = base_results.size(); j < size; j++) + std::map>::iterator itsr = srmap.find(xs); + Assert(itsr != srmap.end()); + for (unsigned j = 0, size = itsr->second.size(); j < size; j++) { - Node res = base_results[j]; + Node res = itsr->second[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) { @@ -708,7 +747,7 @@ Node SygusUnifIo::constructSolutionNode(std::vector& lemmas) d_check_sol = false; // try multiple times if we have done multiple conditions, due to // non-determinism - Node vc; + unsigned sol_term_size = 0; for (unsigned i = 0; i <= d_cond_count; i++) { Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl; @@ -721,20 +760,24 @@ Node SygusUnifIo::constructSolutionNode(std::vector& lemmas) // 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)))) + && (d_solution.isNull() + || (!d_solution.isNull() + && d_tds->getSygusTermSize(vcc) < sol_term_size))) { Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc << std::endl; Trace("sygus-pbe") << "...solved at iteration " << i << std::endl; - vc = vcc; + d_solution = vcc; + sol_term_size = d_tds->getSygusTermSize(vcc); + } + else if (!d_sol_cons_nondet) + { + break; } } - if (!vc.isNull()) + if (!d_solution.isNull()) { - d_solution = vc; - return vc; + return d_solution; } Trace("sygus-pbe") << "...failed to solve." << std::endl; } @@ -784,14 +827,15 @@ bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e) return false; } -bool SygusUnifIo::getExplanationForEnumeratorExclude(Node e, - Node v, - std::vector& results, - std::vector& exp) +bool SygusUnifIo::getExplanationForEnumeratorExclude( + Node e, + Node v, + std::vector& results, + std::vector& exp) { + NodeManager* nm = NodeManager::currentNM(); 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. @@ -849,7 +893,12 @@ void SygusUnifIo::EnumCache::addEnumValue(Node v, std::vector& results) d_enum_vals_res.push_back(results); } -void SygusUnifIo::initializeConstructSol() { d_context.initialize(this); } +void SygusUnifIo::initializeConstructSol() +{ + d_context.initialize(this); + d_sol_cons_nondet = false; +} + void SygusUnifIo::initializeConstructSolFor(Node f) { Assert(d_candidate == f); @@ -998,8 +1047,9 @@ Node SygusUnifIo::constructSol( 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 << " : "; + Trace("sygus-sui-dt-debug") << "increment string values : "; + TermDbSygus::toStreamSygus("sygus-sui-dt-debug", val_t); + Trace("sygus-sui-dt-debug") << " : "; Assert(ecache.d_enum_vals_res[i].size() == d_examples_out.size()); unsigned tot = 0; bool exsuccess = x.getStringIncrement(this, @@ -1024,6 +1074,9 @@ Node SygusUnifIo::constructSol( if (!incr.empty()) { + // solution construction for strings concatenation is non-deterministic + // with respect to failure/success. + d_sol_cons_nondet = true; ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr); Assert(!ret_dt.isNull()); indent("sygus-sui-dt", ind); @@ -1050,40 +1103,69 @@ Node SygusUnifIo::constructSol( << std::endl; } } - if (ret_dt.isNull() && !einfo.isTemplated()) + if (!ret_dt.isNull() || einfo.isTemplated()) + { + Assert(ret_dt.isNull() || ret_dt.getType() == e.getType()); + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "ConstructPBE: returned (pre-strategy) " << ret_dt + << std::endl; + return ret_dt; + } + // we will try a single strategy + EnumTypeInfoStrat* etis = nullptr; + std::map::iterator itsn = tinfo.d_snodes.find(nrole); + if (itsn == tinfo.d_snodes.end()) + { + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "ConstructPBE: returned (no-strategy) " << ret_dt + << std::endl; + return ret_dt; + } + // strategy info + StrategyNode& snode = itsn->second; + if (x.d_visit_role[e].find(nrole) != x.d_visit_role[e].end()) + { + // already visited and context not changed (notice d_visit_role is cleared + // when the context changes). + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "ConstructPBE: returned (already visited) " + << ret_dt << std::endl; + return ret_dt; + } + x.d_visit_role[e][nrole] = true; + // try a random strategy + if (snode.d_strats.size() > 1) { - // we will try a single strategy - EnumTypeInfoStrat* etis = nullptr; - std::map::iterator itsn = - tinfo.d_snodes.find(nrole); - if (itsn != tinfo.d_snodes.end()) + std::random_shuffle(snode.d_strats.begin(), snode.d_strats.end()); + } + // ITE always first if we have not yet solved + // the reasoning is that splitting on conditions only subdivides the problem + // and cannot be the source of failure, whereas the wrong choice for a + // concatenation term may lead to failure + if (d_solution.isNull()) + { + for (unsigned i = 0; i < snode.d_strats.size(); i++) { - // strategy info - StrategyNode& snode = itsn->second; - if (x.d_visit_role[e].find(nrole) == x.d_visit_role[e].end()) + if (snode.d_strats[i]->d_this == strat_ITE) { - 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]; - } + // flip the two + EnumTypeInfoStrat* etis = snode.d_strats[i]; + snode.d_strats[i] = snode.d_strats[0]; + snode.d_strats[0] = etis; + break; } } - if (etis != nullptr) + } + + // iterate over the strategies + unsigned sindex = 0; + bool did_recurse = false; + while (ret_dt.isNull() && !did_recurse && sindex < snode.d_strats.size()) + { + if (snode.d_strats[sindex]->isValid(x)) { + etis = snode.d_strats[sindex]; + Assert(etis != nullptr); StrategyType strat = etis->d_this; indent("sygus-sui-dt", ind + 1); Trace("sygus-sui-dt") @@ -1145,6 +1227,7 @@ Node SygusUnifIo::constructSol( { if (x.d_uinfo.find(ce) == x.d_uinfo.end()) { + x.d_uinfo[ce].clear(); Trace("sygus-sui-dt-debug2") << " reg : PBE: Look for direct solutions for conditional " "enumerator " @@ -1215,9 +1298,8 @@ Node SygusUnifIo::constructSol( // solved terms in at least one branch // only applicable if we have not modified the return value std::map > solved_cond; - if (!x.isReturnValueModified()) + if (!x.isReturnValueModified() && !x.d_uinfo[ce].empty()) { - Assert(x.d_uinfo.find(ce) != x.d_uinfo.end()); int solve_max = 0; for (Node& cond : itpc->second) { @@ -1287,6 +1369,7 @@ Node SygusUnifIo::constructSol( } else { + did_recurse = true; rec_c = constructSol(f, cenum.first, cenum.second, ind + 2, lemmas); } @@ -1327,12 +1410,11 @@ Node SygusUnifIo::constructSol( << "PBE: failed for strategy " << strat << std::endl; } } + // increment + sindex++; } - if (!ret_dt.isNull()) - { - Assert(ret_dt.getType() == e.getType()); - } + Assert(ret_dt.isNull() || ret_dt.getType() == e.getType()); indent("sygus-sui-dt", ind); Trace("sygus-sui-dt") << "ConstructPBE: returned " << ret_dt << std::endl; return ret_dt; diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 0870ea2dc..f1aa08c65 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -143,6 +143,10 @@ class UnifContextIo : public UnifContext * pairs. */ std::map> d_look_ahead_sols; + /** clear */ + void clear() { d_look_ahead_sols.clear(); } + /** is empty */ + bool empty() { return d_look_ahead_sols.empty(); } }; /** map from enumerators to the above info class */ std::map d_uinfo; @@ -306,10 +310,33 @@ class SygusUnifIo : public SygusUnif * register a new value for an enumerator. */ bool d_check_sol; + /** whether we have solved the overall conjecture */ + bool d_solved; /** The number of values we have enumerated for all enumerators. */ unsigned d_cond_count; /** The solution for the function of this class, if one has been found */ Node d_solution; + /** + * This flag is set to true if the solution construction was + * non-deterministic with respect to failure/success. + * + * The solution construction for the string concatenation strategy is + * non-deterministic with respect to success/failure. That is, choosing + * a particular string may lead to being unsolvable in the recursive calls, + * whereas others may not. For example, if our pool of enumerated strings is: + * { "A", x, "B" } + * and our I/O example is: + * f( "AC" ) = "ACB" + * then choosing to consider a solution of the form ( "A" ++ _ ) leads + * to a recursive call where we are solving for f' in: + * "A" ++ f'("AC") = "ACB" + * which is unsolvable since we cannot generate a term starting with "C" + * from the pool above. Whereas if we would have chosen ( x ++ _ ), this + * leads to a recursive call where we are solving for f' in: + * "AC" ++ f'("AC") = "ACB" + * which can be closed with "B", giving us (x ++ "B") as a solution. + */ + bool d_sol_cons_nondet; /** true and false nodes */ Node d_true; Node d_false; @@ -388,10 +415,11 @@ class SygusUnifIo : public SygusUnif * 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& results, - std::vector& exp); + bool getExplanationForEnumeratorExclude( + Node e, + Node v, + std::vector& results, + std::vector& 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 -- 2.30.2