#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"
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;
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);
<< "...got res = " << res << " from " << bv << std::endl;
base_results.push_back(res);
}
+ // get the results for each slave enumerator
+ std::map<Node, std::vector<Node>> 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<Node> args;
+ args.push_back(templ_var);
+ std::vector<Node> sresults;
+ for (const Node& res : base_results)
+ {
+ TNode tres = res;
+ std::vector<Node> 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<Node> exp_exc_vec;
if (getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec))
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)
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++)
+ std::map<Node, std::vector<Node>>::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)
{
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;
// 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;
}
return false;
}
-bool SygusUnifIo::getExplanationForEnumeratorExclude(Node e,
- Node v,
- std::vector<Node>& results,
- std::vector<Node>& exp)
+bool SygusUnifIo::getExplanationForEnumeratorExclude(
+ Node e,
+ Node v,
+ std::vector<Node>& results,
+ std::vector<Node>& 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.
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);
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,
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);
<< 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<NodeRole, StrategyNode>::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<NodeRole, StrategyNode>::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")
{
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 "
// 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())
+ 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)
{
}
else
{
+ did_recurse = true;
rec_c = constructSol(f, cenum.first, cenum.second, ind + 2, lemmas);
}
<< "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;
* pairs.
*/
std::map<Node, std::map<unsigned, Node>> 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<Node, UEnumInfo> d_uinfo;
* 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;
* 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);
+ 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
projects / cvc5.git / commitdiff