d_qe = qe;
d_tds = qe->getTermDatabaseSygus();
- TypeNode tn = f.getType();
- d_cinfo.initialize(f);
- // collect the enumerator types and form the strategy
- collectEnumeratorTypes(tn, role_equal);
- // add the enumerators
- enums.insert(
- enums.end(), d_cinfo.d_esym_list.begin(), d_cinfo.d_esym_list.end());
- // learn redundant ops
- staticLearnRedundantOps(lemmas);
+ d_strategy.initialize(qe, f, enums, lemmas);
}
void SygusUnif::resetExamples()
Node c = d_candidate;
Assert(!d_examples.empty());
Assert(d_examples.size() == d_examples_out.size());
- std::map<Node, EnumInfo>::iterator it = d_einfo.find(e);
- Assert(it != d_einfo.end());
- Assert(
- std::find(it->second.d_enum_vals.begin(), it->second.d_enum_vals.end(), v)
- == it->second.d_enum_vals.end());
+
+ EnumInfo& ei = d_strategy.getEnumInfo(e);
// The explanation for why the current value should be excluded in future
// iterations.
Node exp_exc;
}
// is it excluded for domain-specific reason?
std::vector<Node> exp_exc_vec;
- if (getExplanationForEnumeratorExclude(
- e, v, base_results, it->second, exp_exc_vec))
+ if (getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec))
{
Assert(!exp_exc_vec.empty());
exp_exc = exp_exc_vec.size() == 1
else
{
// notify all slaves
- Assert(!it->second.d_enum_slave.empty());
+ Assert(!ei.d_enum_slave.empty());
// explanation for why this value should be excluded
- for (unsigned s = 0; s < it->second.d_enum_slave.size(); s++)
+ for (unsigned s = 0; s < ei.d_enum_slave.size(); s++)
{
- Node xs = it->second.d_enum_slave[s];
- std::map<Node, EnumInfo>::iterator itv = d_einfo.find(xs);
- Assert(itv != d_einfo.end());
+ Node xs = ei.d_enum_slave[s];
+
+ EnumInfo& eiv = d_strategy.getEnumInfo(xs);
+
+ EnumCache& ecv = d_ecache[xs];
+
Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl;
// bool prevIsCover = false;
- if (itv->second.getRole() == enum_io)
+ if (eiv.getRole() == enum_io)
{
Trace("sygus-pbe-enum") << " IO-Eval of ";
- // prevIsCover = itv->second.isFeasible();
+ // prevIsCover = eiv.isFeasible();
}
else
{
Trace("sygus-pbe-enum") << xs << " : ";
// evaluate all input/output examples
std::vector<Node> results;
- Node templ = itv->second.d_template;
- TNode templ_var = itv->second.d_template_arg;
+ Node templ = eiv.d_template;
+ TNode templ_var = eiv.d_template_arg;
std::map<Node, bool> cond_vals;
for (unsigned j = 0, size = base_results.size(); j < size; j++)
{
Assert(res.isConst());
}
Node resb;
- if (itv->second.getRole() == enum_io)
+ if (eiv.getRole() == enum_io)
{
Node out = d_examples_out[j];
Assert(out.isConst());
}
}
bool keep = false;
- if (itv->second.getRole() == enum_io)
+ if (eiv.getRole() == enum_io)
{
// latter is the degenerate case of no examples
if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty())
Trace("sygus-pbe-enum")
<< " ...success, full solution added to PBE pool : "
<< d_tds->sygusToBuiltin(v) << std::endl;
- if (!itv->second.isSolved())
+ if (!ecv.isSolved())
{
- itv->second.setSolved(v);
+ ecv.setSolved(v);
// it subsumes everything
- itv->second.d_term_trie.clear();
- itv->second.d_term_trie.addTerm(v, results, true, subsume);
+ ecv.d_term_trie.clear();
+ ecv.d_term_trie.addTerm(v, results, true, subsume);
}
keep = true;
}
else
{
- Node val =
- itv->second.d_term_trie.addTerm(v, results, true, subsume);
+ Node val = ecv.d_term_trie.addTerm(v, results, true, subsume);
if (val == v)
{
Trace("sygus-pbe-enum") << " ...success";
if (!subsume.empty())
{
- itv->second.d_enum_subsume.insert(
- itv->second.d_enum_subsume.end(),
- subsume.begin(),
- subsume.end());
+ ecv.d_enum_subsume.insert(
+ ecv.d_enum_subsume.end(), subsume.begin(), subsume.end());
Trace("sygus-pbe-enum")
<< " and subsumed " << subsume.size() << " terms";
}
else
{
// must be unique up to examples
- Node val = itv->second.d_term_trie.addCond(v, results, true);
+ Node val = ecv.d_term_trie.addCond(v, results, true);
if (val == v)
{
Trace("sygus-pbe-enum") << " ...success! add to PBE pool : "
Trace("sygus-pbe-enum")
<< " ...fail : term is not unique" << std::endl;
}
- d_cinfo.d_cond_count++;
+ d_cond_count++;
}
if (keep)
{
- // notify the parent to retry the build of PBE
- d_cinfo.d_check_sol = true;
- itv->second.addEnumValue(this, v, results);
+ // notify to retry the build of solution
+ d_check_sol = true;
+ ecv.addEnumValue(v, results);
}
}
}
Node SygusUnif::constructSolution()
{
Node c = d_candidate;
- if (!d_cinfo.d_solution.isNull())
+ if (!d_solution.isNull())
{
// already has a solution
- return d_cinfo.d_solution;
+ return d_solution;
}
else
{
// only check if an enumerator updated
- if (d_cinfo.d_check_sol)
+ if (d_check_sol)
{
- Trace("sygus-pbe") << "Construct solution, #iterations = "
- << d_cinfo.d_cond_count << std::endl;
- d_cinfo.d_check_sol = false;
+ Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count
+ << std::endl;
+ d_check_sol = false;
// try multiple times if we have done multiple conditions, due to
// non-determinism
Node vc;
- for (unsigned i = 0; i <= d_cinfo.d_cond_count; i++)
+ for (unsigned i = 0; i <= d_cond_count; i++)
{
Trace("sygus-pbe-dt")
<< "ConstructPBE for candidate: " << c << std::endl;
- Node e = d_cinfo.getRootEnumerator();
+ Node e = d_strategy.getRootEnumerator();
UnifContext x;
x.initialize(this);
Node vcc = constructSolution(e, role_equal, x, 1);
}
if (!vc.isNull())
{
- d_cinfo.d_solution = vc;
+ d_solution = vc;
return vc;
}
Trace("sygus-pbe") << "...failed to solve." << std::endl;
}
}
-// ----------------------------- establishing enumeration types
-
-void SygusUnif::registerEnumerator(Node et,
- TypeNode tn,
- EnumRole enum_role,
- bool inSearch)
-{
- if (d_einfo.find(et) == d_einfo.end())
- {
- Trace("sygus-unif-debug")
- << "...register " << et << " for "
- << static_cast<DatatypeType>(tn.toType()).getDatatype().getName();
- Trace("sygus-unif-debug") << ", role = " << enum_role
- << ", in search = " << inSearch << std::endl;
- d_einfo[et].initialize(enum_role);
- // if we are actually enumerating this (could be a compound node in the
- // strategy)
- if (inSearch)
- {
- std::map<TypeNode, Node>::iterator itn = d_cinfo.d_search_enum.find(tn);
- if (itn == d_cinfo.d_search_enum.end())
- {
- // use this for the search
- d_cinfo.d_search_enum[tn] = et;
- d_cinfo.d_esym_list.push_back(et);
- d_einfo[et].d_enum_slave.push_back(et);
- }
- else
- {
- Trace("sygus-unif-debug")
- << "Make " << et << " a slave of " << itn->second << std::endl;
- d_einfo[itn->second].d_enum_slave.push_back(et);
- }
- }
- }
-}
-
-void SygusUnif::collectEnumeratorTypes(TypeNode tn, NodeRole nrole)
-{
- NodeManager* nm = NodeManager::currentNM();
- if (d_cinfo.d_tinfo.find(tn) == d_cinfo.d_tinfo.end())
- {
- // register type
- Trace("sygus-unif") << "Register enumerating type : " << tn << std::endl;
- d_cinfo.initializeType(tn);
- }
- EnumTypeInfo& eti = d_cinfo.d_tinfo[tn];
- std::map<NodeRole, StrategyNode>::iterator itsn = eti.d_snodes.find(nrole);
- if (itsn != eti.d_snodes.end())
- {
- // already initialized
- return;
- }
- StrategyNode& snode = eti.d_snodes[nrole];
-
- // get the enumerator for this
- EnumRole erole = getEnumeratorRoleForNodeRole(nrole);
-
- Node ee;
- std::map<EnumRole, Node>::iterator iten = eti.d_enum.find(erole);
- if (iten == eti.d_enum.end())
- {
- ee = nm->mkSkolem("ee", tn);
- eti.d_enum[erole] = ee;
- Trace("sygus-unif-debug")
- << "...enumerator " << ee << " for "
- << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
- << ", role = " << erole << std::endl;
- }
- else
- {
- ee = iten->second;
- }
-
- // roles that we do not recurse on
- if (nrole == role_ite_condition)
- {
- Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl;
- registerEnumerator(ee, tn, erole, true);
- return;
- }
-
- // look at information on how we will construct solutions for this type
- Assert(tn.isDatatype());
- const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
- Assert(dt.isSygus());
-
- std::map<Node, std::vector<StrategyType> > cop_to_strat;
- std::map<Node, unsigned> cop_to_cindex;
- std::map<Node, std::map<unsigned, Node> > cop_to_child_templ;
- std::map<Node, std::map<unsigned, Node> > cop_to_child_templ_arg;
- std::map<Node, std::vector<unsigned> > cop_to_carg_list;
- std::map<Node, std::vector<TypeNode> > cop_to_child_types;
- std::map<Node, std::vector<Node> > cop_to_sks;
-
- // whether we will enumerate the current type
- bool search_this = false;
- for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
- {
- Node cop = Node::fromExpr(dt[j].getConstructor());
- Node op = Node::fromExpr(dt[j].getSygusOp());
- Trace("sygus-unif-debug") << "--- Infer strategy from " << cop
- << " with sygus op " << op << "..." << std::endl;
-
- // expand the evaluation to see if this constuctor induces a strategy
- std::vector<Node> utchildren;
- utchildren.push_back(cop);
- std::vector<Node> sks;
- std::vector<TypeNode> sktns;
- for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
- {
- Type t = dt[j][k].getRangeType();
- TypeNode ttn = TypeNode::fromType(t);
- Node kv = nm->mkSkolem("ut", ttn);
- sks.push_back(kv);
- cop_to_sks[cop].push_back(kv);
- sktns.push_back(ttn);
- utchildren.push_back(kv);
- }
- Node ut = nm->mkNode(APPLY_CONSTRUCTOR, utchildren);
- std::vector<Node> echildren;
- echildren.push_back(Node::fromExpr(dt.getSygusEvaluationFunc()));
- echildren.push_back(ut);
- Node sbvl = Node::fromExpr(dt.getSygusVarList());
- for (const Node& sbv : sbvl)
- {
- echildren.push_back(sbv);
- }
- Node eut = nm->mkNode(APPLY_UF, echildren);
- Trace("sygus-unif-debug2")
- << " Test evaluation of " << eut << "..." << std::endl;
- eut = d_qe->getTermDatabaseSygus()->unfold(eut);
- Trace("sygus-unif-debug2") << " ...got " << eut;
- Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl;
-
- // candidate strategy
- if (eut.getKind() == ITE)
- {
- cop_to_strat[cop].push_back(strat_ITE);
- }
- else if (eut.getKind() == STRING_CONCAT)
- {
- if (nrole != role_string_suffix)
- {
- cop_to_strat[cop].push_back(strat_CONCAT_PREFIX);
- }
- if (nrole != role_string_prefix)
- {
- cop_to_strat[cop].push_back(strat_CONCAT_SUFFIX);
- }
- }
- else if (dt[j].isSygusIdFunc())
- {
- cop_to_strat[cop].push_back(strat_ID);
- }
-
- // the kinds for which there is a strategy
- if (cop_to_strat.find(cop) != cop_to_strat.end())
- {
- // infer an injection from the arguments of the datatype
- std::map<unsigned, unsigned> templ_injection;
- std::vector<Node> vs;
- std::vector<Node> ss;
- std::map<Node, unsigned> templ_var_index;
- for (unsigned k = 0, sksize = sks.size(); k < sksize; k++)
- {
- Assert(sks[k].getType().isDatatype());
- const Datatype& cdt =
- static_cast<DatatypeType>(sks[k].getType().toType()).getDatatype();
- echildren[0] = Node::fromExpr(cdt.getSygusEvaluationFunc());
- echildren[1] = sks[k];
- Trace("sygus-unif-debug2")
- << "...set eval dt to " << sks[k] << std::endl;
- Node esk = nm->mkNode(APPLY_UF, echildren);
- vs.push_back(esk);
- Node tvar = nm->mkSkolem("templ", esk.getType());
- templ_var_index[tvar] = k;
- Trace("sygus-unif-debug2") << "* template inference : looking for "
- << tvar << " for arg " << k << std::endl;
- ss.push_back(tvar);
- Trace("sygus-unif-debug2")
- << "* substitute : " << esk << " -> " << tvar << std::endl;
- }
- eut = eut.substitute(vs.begin(), vs.end(), ss.begin(), ss.end());
- Trace("sygus-unif-debug2")
- << "Constructor " << j << ", base term is " << eut << std::endl;
- std::map<unsigned, Node> test_args;
- if (dt[j].isSygusIdFunc())
- {
- test_args[0] = eut;
- }
- else
- {
- for (unsigned k = 0, size = eut.getNumChildren(); k < size; k++)
- {
- test_args[k] = eut[k];
- }
- }
-
- // TODO : prefix grouping prefix/suffix
- bool isAssoc = TermUtil::isAssoc(eut.getKind());
- Trace("sygus-unif-debug2")
- << eut.getKind() << " isAssoc = " << isAssoc << std::endl;
- std::map<unsigned, std::vector<unsigned> > assoc_combine;
- std::vector<unsigned> assoc_waiting;
- int assoc_last_valid_index = -1;
- for (std::pair<const unsigned, Node>& ta : test_args)
- {
- unsigned k = ta.first;
- Node eut_c = ta.second;
- // success if we can find a injection from args to sygus args
- if (!inferTemplate(k, eut_c, templ_var_index, templ_injection))
- {
- Trace("sygus-unif-debug")
- << "...fail: could not find injection (range)." << std::endl;
- cop_to_strat.erase(cop);
- break;
- }
- std::map<unsigned, unsigned>::iterator itti = templ_injection.find(k);
- if (itti != templ_injection.end())
- {
- // if associative, combine arguments if it is the same variable
- if (isAssoc && assoc_last_valid_index >= 0
- && itti->second == templ_injection[assoc_last_valid_index])
- {
- templ_injection.erase(k);
- assoc_combine[assoc_last_valid_index].push_back(k);
- }
- else
- {
- assoc_last_valid_index = (int)k;
- if (!assoc_waiting.empty())
- {
- assoc_combine[k].insert(assoc_combine[k].end(),
- assoc_waiting.begin(),
- assoc_waiting.end());
- assoc_waiting.clear();
- }
- assoc_combine[k].push_back(k);
- }
- }
- else
- {
- // a ground argument
- if (!isAssoc)
- {
- Trace("sygus-unif-debug")
- << "...fail: could not find injection (functional)."
- << std::endl;
- cop_to_strat.erase(cop);
- break;
- }
- else
- {
- if (assoc_last_valid_index >= 0)
- {
- assoc_combine[assoc_last_valid_index].push_back(k);
- }
- else
- {
- assoc_waiting.push_back(k);
- }
- }
- }
- }
- if (cop_to_strat.find(cop) != cop_to_strat.end())
- {
- // construct the templates
- if (!assoc_waiting.empty())
- {
- // could not find a way to fit some arguments into injection
- cop_to_strat.erase(cop);
- }
- else
- {
- for (std::pair<const unsigned, Node>& ta : test_args)
- {
- unsigned k = ta.first;
- Trace("sygus-unif-debug2")
- << "- processing argument " << k << "..." << std::endl;
- if (templ_injection.find(k) != templ_injection.end())
- {
- unsigned sk_index = templ_injection[k];
- if (std::find(cop_to_carg_list[cop].begin(),
- cop_to_carg_list[cop].end(),
- sk_index)
- == cop_to_carg_list[cop].end())
- {
- cop_to_carg_list[cop].push_back(sk_index);
- }
- else
- {
- Trace("sygus-unif-debug")
- << "...fail: duplicate argument used" << std::endl;
- cop_to_strat.erase(cop);
- break;
- }
- // also store the template information, if necessary
- Node teut;
- if (isAssoc)
- {
- std::vector<unsigned>& ac = assoc_combine[k];
- Assert(!ac.empty());
- std::vector<Node> children;
- for (unsigned ack = 0, size_ac = ac.size(); ack < size_ac;
- ack++)
- {
- children.push_back(eut[ac[ack]]);
- }
- teut = children.size() == 1
- ? children[0]
- : nm->mkNode(eut.getKind(), children);
- teut = Rewriter::rewrite(teut);
- }
- else
- {
- teut = ta.second;
- }
-
- if (!teut.isVar())
- {
- cop_to_child_templ[cop][k] = teut;
- cop_to_child_templ_arg[cop][k] = ss[sk_index];
- Trace("sygus-unif-debug")
- << " Arg " << k << " (template : " << teut << " arg "
- << ss[sk_index] << "), index " << sk_index << std::endl;
- }
- else
- {
- Trace("sygus-unif-debug")
- << " Arg " << k << ", index " << sk_index << std::endl;
- Assert(teut == ss[sk_index]);
- }
- }
- else
- {
- Assert(isAssoc);
- }
- }
- }
- }
- }
- if (cop_to_strat.find(cop) == cop_to_strat.end())
- {
- Trace("sygus-unif") << "...constructor " << cop
- << " does not correspond to a strategy." << std::endl;
- search_this = true;
- }
- else
- {
- Trace("sygus-unif") << "-> constructor " << cop
- << " matches strategy for " << eut.getKind() << "..."
- << std::endl;
- // collect children types
- for (unsigned k = 0, size = cop_to_carg_list[cop].size(); k < size; k++)
- {
- TypeNode tn = sktns[cop_to_carg_list[cop][k]];
- Trace("sygus-unif-debug")
- << " Child type " << k << " : "
- << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
- << std::endl;
- cop_to_child_types[cop].push_back(tn);
- }
- }
- }
-
- // check whether we should also enumerate the current type
- Trace("sygus-unif-debug2") << " register this enumerator..." << std::endl;
- registerEnumerator(ee, tn, erole, search_this);
-
- if (cop_to_strat.empty())
- {
- Trace("sygus-unif") << "...consider " << dt.getName() << " a basic type"
- << std::endl;
- }
- else
- {
- for (std::pair<const Node, std::vector<StrategyType> >& cstr : cop_to_strat)
- {
- Node cop = cstr.first;
- Trace("sygus-unif-debug")
- << "Constructor " << cop << " has " << cstr.second.size()
- << " strategies..." << std::endl;
- for (unsigned s = 0, ssize = cstr.second.size(); s < ssize; s++)
- {
- EnumTypeInfoStrat* cons_strat = new EnumTypeInfoStrat;
- StrategyType strat = cstr.second[s];
-
- cons_strat->d_this = strat;
- cons_strat->d_cons = cop;
- Trace("sygus-unif-debug")
- << "Process strategy #" << s << " for operator : " << cop << " : "
- << strat << std::endl;
- Assert(cop_to_child_types.find(cop) != cop_to_child_types.end());
- std::vector<TypeNode>& childTypes = cop_to_child_types[cop];
- Assert(cop_to_carg_list.find(cop) != cop_to_carg_list.end());
- std::vector<unsigned>& cargList = cop_to_carg_list[cop];
-
- std::vector<Node> sol_templ_children;
- sol_templ_children.resize(cop_to_sks[cop].size());
-
- for (unsigned j = 0, csize = childTypes.size(); j < csize; j++)
- {
- // calculate if we should allocate a new enumerator : should be true
- // if we have a new role
- NodeRole nrole_c = nrole;
- if (strat == strat_ITE)
- {
- if (j == 0)
- {
- nrole_c = role_ite_condition;
- }
- }
- else if (strat == strat_CONCAT_PREFIX)
- {
- if ((j + 1) < childTypes.size())
- {
- nrole_c = role_string_prefix;
- }
- }
- else if (strat == strat_CONCAT_SUFFIX)
- {
- if (j > 0)
- {
- nrole_c = role_string_suffix;
- }
- }
- // in all other cases, role is same as parent
-
- // register the child type
- TypeNode ct = childTypes[j];
- Node csk = cop_to_sks[cop][cargList[j]];
- cons_strat->d_sol_templ_args.push_back(csk);
- sol_templ_children[cargList[j]] = csk;
-
- EnumRole erole_c = getEnumeratorRoleForNodeRole(nrole_c);
- // make the enumerator
- Node et;
- if (cop_to_child_templ[cop].find(j) != cop_to_child_templ[cop].end())
- {
- // it is templated, allocate a fresh variable
- et = nm->mkSkolem("et", ct);
- Trace("sygus-unif-debug")
- << "...enumerate " << et << " of type "
- << ((DatatypeType)ct.toType()).getDatatype().getName();
- Trace("sygus-unif-debug") << " for arg " << j << " of "
- << static_cast<DatatypeType>(tn.toType())
- .getDatatype()
- .getName()
- << std::endl;
- registerEnumerator(et, ct, erole_c, true);
- d_einfo[et].d_template = cop_to_child_templ[cop][j];
- d_einfo[et].d_template_arg = cop_to_child_templ_arg[cop][j];
- Assert(!d_einfo[et].d_template.isNull());
- Assert(!d_einfo[et].d_template_arg.isNull());
- }
- else
- {
- Trace("sygus-unif-debug")
- << "...child type enumerate "
- << ((DatatypeType)ct.toType()).getDatatype().getName()
- << ", node role = " << nrole_c << std::endl;
- collectEnumeratorTypes(ct, nrole_c);
- // otherwise use the previous
- Assert(d_cinfo.d_tinfo[ct].d_enum.find(erole_c)
- != d_cinfo.d_tinfo[ct].d_enum.end());
- et = d_cinfo.d_tinfo[ct].d_enum[erole_c];
- }
- Trace("sygus-unif-debug")
- << "Register child enumerator " << et << ", arg " << j << " of "
- << cop << ", role = " << erole_c << std::endl;
- Assert(!et.isNull());
- cons_strat->d_cenum.push_back(std::pair<Node, NodeRole>(et, nrole_c));
- }
- // children that are unused in the strategy can be arbitrary
- for (unsigned j = 0, stsize = sol_templ_children.size(); j < stsize;
- j++)
- {
- if (sol_templ_children[j].isNull())
- {
- sol_templ_children[j] = cop_to_sks[cop][j].getType().mkGroundTerm();
- }
- }
- sol_templ_children.insert(sol_templ_children.begin(), cop);
- cons_strat->d_sol_templ =
- nm->mkNode(APPLY_CONSTRUCTOR, sol_templ_children);
- if (strat == strat_CONCAT_SUFFIX)
- {
- std::reverse(cons_strat->d_cenum.begin(), cons_strat->d_cenum.end());
- std::reverse(cons_strat->d_sol_templ_args.begin(),
- cons_strat->d_sol_templ_args.end());
- }
- if (Trace.isOn("sygus-unif"))
- {
- Trace("sygus-unif") << "Initialized strategy " << strat;
- Trace("sygus-unif")
- << " for "
- << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
- << ", operator " << cop;
- Trace("sygus-unif") << ", #children = " << cons_strat->d_cenum.size()
- << ", solution template = (lambda ( ";
- for (const Node& targ : cons_strat->d_sol_templ_args)
- {
- Trace("sygus-unif") << targ << " ";
- }
- Trace("sygus-unif") << ") " << cons_strat->d_sol_templ << ")";
- Trace("sygus-unif") << std::endl;
- }
- // make the strategy
- snode.d_strats.push_back(cons_strat);
- }
- }
- }
-}
-
-bool SygusUnif::inferTemplate(unsigned k,
- Node n,
- std::map<Node, unsigned>& templ_var_index,
- std::map<unsigned, unsigned>& templ_injection)
-{
- if (n.getNumChildren() == 0)
- {
- std::map<Node, unsigned>::iterator itt = templ_var_index.find(n);
- if (itt != templ_var_index.end())
- {
- unsigned kk = itt->second;
- std::map<unsigned, unsigned>::iterator itti = templ_injection.find(k);
- if (itti == templ_injection.end())
- {
- Trace("sygus-unif-debug")
- << "...set template injection " << k << " -> " << kk << std::endl;
- templ_injection[k] = kk;
- }
- else if (itti->second != kk)
- {
- // two distinct variables in this term, we fail
- return false;
- }
- }
- return true;
- }
- else
- {
- for (unsigned i = 0; i < n.getNumChildren(); i++)
- {
- if (!inferTemplate(k, n[i], templ_var_index, templ_injection))
- {
- return false;
- }
- }
- }
- return true;
-}
-
-void SygusUnif::staticLearnRedundantOps(std::vector<Node>& lemmas)
-{
- for (unsigned i = 0; i < d_cinfo.d_esym_list.size(); i++)
- {
- Node e = d_cinfo.d_esym_list[i];
- std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e);
- Assert(itn != d_einfo.end());
- // see if there is anything we can eliminate
- Trace("sygus-unif")
- << "* Search enumerator #" << i << " : type "
- << ((DatatypeType)e.getType().toType()).getDatatype().getName()
- << " : ";
- Trace("sygus-unif") << e << " has " << itn->second.d_enum_slave.size()
- << " slaves:" << std::endl;
- for (unsigned j = 0; j < itn->second.d_enum_slave.size(); j++)
- {
- Node es = itn->second.d_enum_slave[j];
- std::map<Node, EnumInfo>::iterator itns = d_einfo.find(es);
- Assert(itns != d_einfo.end());
- Trace("sygus-unif") << " " << es << ", role = " << itns->second.getRole()
- << std::endl;
- }
- }
- Trace("sygus-unif") << std::endl;
- Trace("sygus-unif") << "Strategy for candidate " << d_candidate
- << " is : " << std::endl;
- std::map<Node, std::map<NodeRole, bool> > visited;
- std::map<Node, std::map<unsigned, bool> > needs_cons;
- staticLearnRedundantOps(
- d_cinfo.getRootEnumerator(), role_equal, visited, needs_cons, 0, false);
- // now, check the needs_cons map
- for (std::pair<const Node, std::map<unsigned, bool> >& nce : needs_cons)
- {
- Node em = nce.first;
- const Datatype& dt =
- static_cast<DatatypeType>(em.getType().toType()).getDatatype();
- for (std::pair<const unsigned, bool>& nc : nce.second)
- {
- Assert(nc.first < dt.getNumConstructors());
- if (!nc.second)
- {
- Node tst =
- datatypes::DatatypesRewriter::mkTester(em, nc.first, dt).negate();
- if (std::find(lemmas.begin(), lemmas.end(), tst) == lemmas.end())
- {
- Trace("sygus-unif")
- << "...can exclude based on : " << tst << std::endl;
- lemmas.push_back(tst);
- }
- }
- }
- }
-}
-
-void SygusUnif::staticLearnRedundantOps(
- Node e,
- NodeRole nrole,
- std::map<Node, std::map<NodeRole, bool> >& visited,
- std::map<Node, std::map<unsigned, bool> >& needs_cons,
- int ind,
- bool isCond)
-{
- std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e);
- Assert(itn != d_einfo.end());
-
- if (visited[e].find(nrole) == visited[e].end()
- || (isCond && !itn->second.isConditional()))
- {
- visited[e][nrole] = true;
- // if conditional
- if (isCond)
- {
- itn->second.setConditional();
- }
- indent("sygus-unif", ind);
- Trace("sygus-unif") << e << " :: node role : " << nrole;
- Trace("sygus-unif")
- << ", type : "
- << ((DatatypeType)e.getType().toType()).getDatatype().getName();
- if (isCond)
- {
- Trace("sygus-unif") << ", conditional";
- }
- Trace("sygus-unif") << ", enum role : " << itn->second.getRole();
-
- if (itn->second.isTemplated())
- {
- Trace("sygus-unif") << ", templated : (lambda "
- << itn->second.d_template_arg << " "
- << itn->second.d_template << ")" << std::endl;
- }
- else
- {
- Trace("sygus-unif") << std::endl;
- TypeNode etn = e.getType();
-
- // enumerator type info
- std::map<TypeNode, EnumTypeInfo>::iterator itt =
- d_cinfo.d_tinfo.find(etn);
- Assert(itt != d_cinfo.d_tinfo.end());
- EnumTypeInfo& tinfo = itt->second;
-
- // strategy info
- std::map<NodeRole, StrategyNode>::iterator itsn =
- tinfo.d_snodes.find(nrole);
- Assert(itsn != tinfo.d_snodes.end());
- StrategyNode& snode = itsn->second;
-
- if (snode.d_strats.empty())
- {
- return;
- }
- std::map<unsigned, bool> needs_cons_curr;
- // various strategies
- for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
- {
- EnumTypeInfoStrat* etis = snode.d_strats[j];
- StrategyType strat = etis->d_this;
- bool newIsCond = isCond || strat == strat_ITE;
- indent("sygus-unif", ind + 1);
- Trace("sygus-unif") << "Strategy : " << strat
- << ", from cons : " << etis->d_cons << std::endl;
- int cindex = Datatype::indexOf(etis->d_cons.toExpr());
- Assert(cindex != -1);
- needs_cons_curr[static_cast<unsigned>(cindex)] = false;
- for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
- {
- // recurse
- staticLearnRedundantOps(
- cec.first, cec.second, visited, needs_cons, ind + 2, newIsCond);
- }
- }
- // get the master enumerator for the type of this enumerator
- std::map<TypeNode, Node>::iterator itse = d_cinfo.d_search_enum.find(etn);
- if (itse == d_cinfo.d_search_enum.end())
- {
- return;
- }
- Node em = itse->second;
- Assert(!em.isNull());
- // get the current datatype
- const Datatype& dt =
- static_cast<DatatypeType>(etn.toType()).getDatatype();
- // all constructors that are not a part of a strategy are needed
- for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
- {
- if (needs_cons_curr.find(j) == needs_cons_curr.end())
- {
- needs_cons_curr[j] = true;
- }
- }
- // update the constructors that the master enumerator needs
- if (needs_cons.find(em) == needs_cons.end())
- {
- needs_cons[em] = needs_cons_curr;
- }
- else
- {
- for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
- {
- needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j];
- }
- }
- }
- }
- else
- {
- indent("sygus-unif", ind);
- Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl;
- }
-}
-
// ------------------------------------ solution construction from enumeration
-bool SygusUnif::useStrContainsEnumeratorExclude(Node x, EnumInfo& ei)
+bool SygusUnif::useStrContainsEnumeratorExclude(Node e)
{
- TypeNode xbt = d_tds->sygusToBuiltinType(x.getType());
+ TypeNode xbt = d_tds->sygusToBuiltinType(e.getType());
if (xbt.isString())
{
- std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(x);
+ 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-pbe-enum-debug")
- << "Is " << x << " is str.contains exclusion?" << std::endl;
- d_use_str_contains_eexc[x] = true;
+ Trace("sygus-pbe-enum-debug") << "Is " << e << " is str.contains exclusion?"
+ << std::endl;
+ d_use_str_contains_eexc[e] = true;
+ EnumInfo& ei = d_strategy.getEnumInfo(e);
for (const Node& sn : ei.d_enum_slave)
{
- std::map<Node, EnumInfo>::iterator itv = d_einfo.find(sn);
- EnumRole er = itv->second.getRole();
+ EnumInfo& eis = d_strategy.getEnumInfo(sn);
+ EnumRole er = eis.getRole();
if (er != enum_io && er != enum_concat_term)
{
Trace("sygus-pbe-enum-debug") << " incompatible slave : " << sn
<< ", role = " << er << std::endl;
- d_use_str_contains_eexc[x] = false;
+ d_use_str_contains_eexc[e] = false;
return false;
}
- if (itv->second.isConditional())
+ if (eis.isConditional())
{
Trace("sygus-pbe-enum-debug")
<< " conditional slave : " << sn << std::endl;
- d_use_str_contains_eexc[x] = false;
+ d_use_str_contains_eexc[e] = false;
return false;
}
}
Trace("sygus-pbe-enum-debug")
<< "...can use str.contains exclusion." << std::endl;
- return d_use_str_contains_eexc[x];
+ return d_use_str_contains_eexc[e];
}
return false;
}
-bool SygusUnif::getExplanationForEnumeratorExclude(Node x,
+bool SygusUnif::getExplanationForEnumeratorExclude(Node e,
Node v,
std::vector<Node>& results,
- EnumInfo& ei,
std::vector<Node>& exp)
{
- if (useStrContainsEnumeratorExclude(x, ei))
+ if (useStrContainsEnumeratorExclude(e))
{
NodeManager* nm = NodeManager::currentNM();
// This check whether the example evaluates to something that is larger than
}
// check if all examples had longer length that the output
Assert(d_examples_out.size() == results.size());
- Trace("sygus-pbe-cterm-debug")
- << "Check enumerator exclusion for " << x << " -> "
- << d_tds->sygusToBuiltin(v) << " based on str.contains." << std::endl;
+ Trace("sygus-pbe-cterm-debug") << "Check enumerator exclusion for " << e
+ << " -> " << d_tds->sygusToBuiltin(v)
+ << " based on str.contains." << std::endl;
std::vector<unsigned> cmp_indices;
for (unsigned i = 0, size = results.size(); i < size; i++)
{
{
// we check invariance with respect to a negative contains test
NegContainsSygusInvarianceTest ncset;
- ncset.init(x, d_examples, d_examples_out, cmp_indices);
+ ncset.init(e, d_examples, d_examples_out, cmp_indices);
// construct the generalized explanation
- d_tds->getExplain()->getExplanationFor(x, v, exp, ncset);
+ d_tds->getExplain()->getExplanationFor(e, v, exp, ncset);
Trace("sygus-pbe-cterm")
<< "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin(v)
<< " due to negative containment." << std::endl;
return false;
}
-void SygusUnif::EnumInfo::addEnumValue(SygusUnif* pbe,
- Node v,
- std::vector<Node>& results)
+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_vals_res.push_back(results);
}
-void SygusUnif::EnumInfo::initialize(EnumRole role) { d_role = role; }
-
-void SygusUnif::EnumInfo::setSolved(Node slv) { d_enum_solved = slv; }
-
-void SygusUnif::CandidateInfo::initialize(Node c)
-{
- d_this_candidate = c;
- d_root = c.getType();
-}
-
-void SygusUnif::CandidateInfo::initializeType(TypeNode tn)
-{
- d_tinfo[tn].d_this_type = tn;
- d_tinfo[tn].d_parent = this;
-}
-
-Node SygusUnif::CandidateInfo::getRootEnumerator()
-{
- std::map<EnumRole, Node>::iterator it = d_tinfo[d_root].d_enum.find(enum_io);
- Assert(it != d_tinfo[d_root].d_enum.end());
- return it->second;
-}
-
Node SygusUnif::constructBestSolvedTerm(std::vector<Node>& solved,
UnifContext& x)
{
Trace("sygus-pbe-dt-debug") << std::endl;
}
// enumerator type info
- std::map<TypeNode, EnumTypeInfo>::iterator itt = d_cinfo.d_tinfo.find(etn);
- Assert(itt != d_cinfo.d_tinfo.end());
- EnumTypeInfo& tinfo = itt->second;
+ EnumTypeInfo& tinfo = d_strategy.getEnumTypeInfo(etn);
// get the enumerator information
- std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e);
- Assert(itn != d_einfo.end());
- EnumInfo& einfo = itn->second;
+ EnumInfo& einfo = d_strategy.getEnumInfo(e);
+
+ EnumCache& ecache = d_ecache[e];
Node ret_dt;
if (nrole == role_equal)
{
if (!x.isReturnValueModified())
{
- if (einfo.isSolved())
+ if (ecache.isSolved())
{
// this type has a complete solution
- ret_dt = einfo.getSolved();
+ ret_dt = ecache.getSolved();
indent("sygus-pbe-dt", ind);
Trace("sygus-pbe-dt") << "return PBE: success : solved "
<< d_tds->sygusToBuiltin(ret_dt) << std::endl;
{
// could be conditionally solved
std::vector<Node> subsumed_by;
- einfo.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by);
+ ecache.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by);
if (!subsumed_by.empty())
{
ret_dt = constructBestSolvedTerm(subsumed_by, x);
{
// check if a current value that closes all examples
// get the term enumerator for this type
- bool success = true;
- std::map<Node, EnumInfo>::iterator itet;
std::map<EnumRole, Node>::iterator itnt =
tinfo.d_enum.find(enum_concat_term);
- if (itnt != itt->second.d_enum.end())
+ if (itnt != tinfo.d_enum.end())
{
Node et = itnt->second;
- itet = d_einfo.find(et);
- Assert(itet != d_einfo.end());
- }
- else
- {
- success = false;
- }
- if (success)
- {
+
+ EnumCache& ecachet = d_ecache[et];
// get the current examples
std::vector<String> ex_vals;
x.getCurrentStrings(this, d_examples_out, ex_vals);
- Assert(itn->second.d_enum_vals.size()
- == itn->second.d_enum_vals_res.size());
+ Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
// test each example in the term enumerator for the type
std::vector<Node> str_solved;
- for (unsigned i = 0, size = itet->second.d_enum_vals.size(); i < size;
- i++)
+ for (unsigned i = 0, size = ecachet.d_enum_vals.size(); i < size; i++)
{
- if (x.isStringSolved(
- this, ex_vals, itet->second.d_enum_vals_res[i]))
+ if (x.isStringSolved(this, ex_vals, ecachet.d_enum_vals_res[i]))
{
- str_solved.push_back(itet->second.d_enum_vals[i]);
+ str_solved.push_back(ecachet.d_enum_vals[i]);
}
}
if (!str_solved.empty())
// check if there is a value for which is a prefix/suffix of all active
// examples
- Assert(einfo.d_enum_vals.size() == einfo.d_enum_vals_res.size());
+ Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
- for (unsigned i = 0, size = einfo.d_enum_vals.size(); i < size; i++)
+ for (unsigned i = 0, size = ecache.d_enum_vals.size(); i < size; i++)
{
- Node val_t = einfo.d_enum_vals[i];
+ Node val_t = ecache.d_enum_vals[i];
Assert(incr.find(val_t) == incr.end());
indent("sygus-pbe-dt-debug", ind);
Trace("sygus-pbe-dt-debug")
<< "increment string values : " << val_t << " : ";
- Assert(einfo.d_enum_vals_res[i].size() == d_examples_out.size());
+ Assert(ecache.d_enum_vals_res[i].size() == d_examples_out.size());
unsigned tot = 0;
bool exsuccess = x.getStringIncrement(this,
isPrefix,
ex_vals,
- einfo.d_enum_vals_res[i],
+ ecache.d_enum_vals_res[i],
incr[val_t],
tot);
if (!exsuccess)
// get an eligible strategy index
unsigned sindex = 0;
while (sindex < snode.d_strats.size()
- && !snode.d_strats[sindex]->isValid(this, x))
+ && !snode.d_strats[sindex]->isValid(&x))
{
sindex++;
}
std::vector<Node> prev;
if (strat == strat_ITE && sc > 0)
{
- std::map<Node, EnumInfo>::iterator itnc =
- d_einfo.find(split_cond_enum);
- Assert(itnc != d_einfo.end());
+ EnumCache& ecache_cond = d_ecache[split_cond_enum];
Assert(split_cond_res_index >= 0);
Assert(split_cond_res_index
- < (int)itnc->second.d_enum_vals_res.size());
+ < (int)ecache_cond.d_enum_vals_res.size());
prev = x.d_vals;
bool ret = x.updateContext(
this,
- itnc->second.d_enum_vals_res[split_cond_res_index],
+ ecache_cond.d_enum_vals_res[split_cond_res_index],
sc == 1);
AlwaysAssert(ret);
}
{
Node ce = cenum.first;
- // register the condition enumerator
- std::map<Node, EnumInfo>::iterator itnc = d_einfo.find(ce);
- Assert(itnc != d_einfo.end());
- EnumInfo& einfo_child = itnc->second;
+ EnumCache& ecache_child = d_ecache[ce];
// only used if the return value is not modified
if (!x.isReturnValueModified())
<< " reg : PBE: Look for direct solutions for conditional "
"enumerator "
<< ce << " ... " << std::endl;
- Assert(einfo_child.d_enum_vals.size()
- == einfo_child.d_enum_vals_res.size());
+ Assert(ecache_child.d_enum_vals.size()
+ == ecache_child.d_enum_vals_res.size());
for (unsigned i = 1; i <= 2; i++)
{
std::pair<Node, NodeRole>& te_pair = etis->d_cenum[i];
Node te = te_pair.first;
- std::map<Node, EnumInfo>::iterator itnt = d_einfo.find(te);
- Assert(itnt != d_einfo.end());
+ EnumCache& ecache_te = d_ecache[te];
bool branch_pol = (i == 1);
// for each condition, get terms that satisfy it in this
// branch
- for (unsigned k = 0, size = einfo_child.d_enum_vals.size();
+ for (unsigned k = 0, size = ecache_child.d_enum_vals.size();
k < size;
k++)
{
- Node cond = einfo_child.d_enum_vals[k];
+ Node cond = ecache_child.d_enum_vals[k];
std::vector<Node> solved;
- itnt->second.d_term_trie.getSubsumedBy(
- einfo_child.d_enum_vals_res[k], branch_pol, solved);
+ ecache_te.d_term_trie.getSubsumedBy(
+ ecache_child.d_enum_vals_res[k], branch_pol, solved);
Trace("sygus-pbe-dt-debug2")
<< " reg : PBE: " << d_tds->sygusToBuiltin(cond)
<< " has " << solved.size() << " solutions in branch "
// distinguishable
std::map<int, std::vector<Node> > possible_cond;
std::map<Node, int> solved_cond; // stores branch
- einfo_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond);
+ ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond);
std::map<int, std::vector<Node> >::iterator itpc =
possible_cond.find(0);
}
if (!rec_c.isNull())
{
- Assert(einfo_child.d_enum_val_to_index.find(rec_c)
- != einfo_child.d_enum_val_to_index.end());
- split_cond_res_index = einfo_child.d_enum_val_to_index[rec_c];
+ Assert(ecache_child.d_enum_val_to_index.find(rec_c)
+ != ecache_child.d_enum_val_to_index.end());
+ split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c];
split_cond_enum = ce;
Assert(split_cond_res_index >= 0);
Assert(split_cond_res_index
- < (int)einfo_child.d_enum_vals_res.size());
+ < (int)ecache_child.d_enum_vals_res.size());
}
}
else
return ret_dt;
}
-bool SygusUnif::EnumTypeInfoStrat::isValid(SygusUnif* pbe, UnifContext& x)
-{
- if ((x.d_has_string_pos == role_string_prefix
- && d_this == strat_CONCAT_SUFFIX)
- || (x.d_has_string_pos == role_string_suffix
- && d_this == strat_CONCAT_PREFIX))
- {
- return false;
- }
- return true;
-}
-
-SygusUnif::StrategyNode::~StrategyNode()
-{
- for (unsigned j = 0, size = d_strats.size(); j < size; j++)
- {
- delete d_strats[j];
- }
- d_strats.clear();
-}
-
void SygusUnif::indent(const char* c, int ind)
{
if (Trace.isOn(c))
*
* This class maintains:
* (1) A "strategy tree" based on the syntactic restrictions for f that is
- * constructed during initialize,
+ * constructed during initialize (d_strategy),
* (2) A set of input/output examples that are the specification for f. This
* can be updated via calls to resetExmaples/addExamples,
- * (3) A set of terms that have been enumerated for enumerators. This can be
- * updated via calls to notifyEnumeration.
+ * (3) A set of terms that have been enumerated for enumerators (d_ecache). This
+ * can be updated via calls to notifyEnumeration.
*
* Based on the above, solutions can be constructed via calls to
* constructSolution.
bool pol = true);
//-----------------------end debug printing
- //------------------------------ representation of a enumeration strategy
/**
* This class stores information regarding an enumerator, including:
- * - Information regarding the role of this enumerator (see EnumRole), its
- * parent, whether it is templated, its slave enumerators, and so on, and
- * - A database of values that have been enumerated for this enumerator.
- *
- * We say an enumerator is a master enumerator if it is the variable that
- * we use to enumerate values for its sort. Master enumerators may have
- * (possibly multiple) slave enumerators, stored in d_enum_slave. We make
- * the first enumerator for each type a master enumerator, and any additional
- * ones slaves of it.
+ * a database of values that have been enumerated for this enumerator.
*/
- class EnumInfo
+ class EnumCache
{
public:
- EnumInfo() : d_role(enum_io), d_is_conditional(false) {}
- /** initialize this class
- *
- * c is the parent function-to-synthesize
- * role is the "role" the enumerator plays in the high-level strategy,
- * which is one of enum_* above.
- */
- void initialize(EnumRole role);
- /** is this enumerator associated with a template? */
- bool isTemplated() { return !d_template.isNull(); }
- /** set conditional
- *
- * This flag is set to true if this enumerator may not apply to all
- * input/output examples. For example, if this enumerator is used
- * as an output value beneath a conditional in an instance of strat_ITE,
- * then this enumerator is conditional.
- */
- void setConditional() { d_is_conditional = true; }
- /** is conditional */
- bool isConditional() { return d_is_conditional; }
- /** get the role of this enumerator */
- EnumRole getRole() { return d_role; }
- /** enumerator template
- *
- * If d_template non-null, enumerated values V are immediately transformed to
- * d_template { d_template_arg -> V }.
- */
- Node d_template;
- Node d_template_arg;
- /**
- * Slave enumerators of this enumerator. These are other enumerators that
- * have the same type, but a different role in the strategy tree. We
- * generally
- * only use one enumerator per type, and hence these slaves are notified when
- * values are enumerated for this enumerator.
- */
- std::vector<Node> d_enum_slave;
-
- //---------------------------enumerated values
+ EnumCache() {}
/**
* Notify this class that the term v has been enumerated for this enumerator.
* Its evaluation under the set of examples in pbe are stored in results.
*/
- void addEnumValue(SygusUnif* pbe, Node v, std::vector<Node>& 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);
+ 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. */
* enum_concat_term).
*/
SubsumeTrie d_term_trie;
- //---------------------------end enumerated values
private:
/**
* Whether an enumerated value for this conjecture has solved the entire
* conjecture.
*/
Node d_enum_solved;
- /** the role of this enumerator (one of enum_* above). */
- EnumRole d_role;
- /** is this enumerator conditional */
- bool d_is_conditional;
};
/** maps enumerators to the information above */
- std::map<Node, EnumInfo> d_einfo;
+ std::map<Node, EnumCache> d_ecache;
- class CandidateInfo;
- class EnumTypeInfoStrat;
-
- /** represents a node in the strategy graph
- *
- * It contains a list of possible strategies which are tried during calls
- * to constructSolution.
- */
- class StrategyNode
- {
- public:
- StrategyNode() {}
- ~StrategyNode();
- /** the set of strategies to try at this node in the strategy graph */
- std::vector<EnumTypeInfoStrat*> d_strats;
- };
-
- /** stores enumerators and strategies for a SyGuS datatype type */
- class EnumTypeInfo
- {
- public:
- EnumTypeInfo() : d_parent(NULL) {}
- /** the parent candidate info (see below) */
- CandidateInfo* d_parent;
- /** the type that this information is for */
- TypeNode d_this_type;
- /** map from enum roles to enumerators for this type */
- std::map<EnumRole, Node> d_enum;
- /** map from node roles to strategy nodes */
- std::map<NodeRole, StrategyNode> d_snodes;
- };
-
- /** stores strategy and enumeration information for a function-to-synthesize
+ /**
+ * Whether we will try to construct solution on the next call to
+ * constructSolution. This flag is set to true when we successfully
+ * register a new value for an enumerator.
*/
- class CandidateInfo
- {
- public:
- CandidateInfo() : d_check_sol(false), d_cond_count(0) {}
- Node d_this_candidate;
- /**
- * The root sygus datatype for the function-to-synthesize,
- * which encodes the overall syntactic restrictions on the space
- * of solutions.
- */
- TypeNode d_root;
- /** Info for sygus datatype type occurring in a field of d_root */
- std::map<TypeNode, EnumTypeInfo> d_tinfo;
- /** list of all enumerators for the function-to-synthesize */
- std::vector<Node> d_esym_list;
- /**
- * Maps sygus datatypes to their search enumerator. This is the (single)
- * enumerator of that type that we enumerate values for.
- */
- std::map<TypeNode, Node> d_search_enum;
- bool d_check_sol;
- unsigned d_cond_count;
- Node d_solution;
- void initialize(Node c);
- void initializeType(TypeNode tn);
- Node getRootEnumerator();
- };
+ bool d_check_sol;
+ /** The number of values we have enumerated for all enumerators. */
+ unsigned d_cond_count;
+ /** The solution for the function of this class, if one has been found */
+ Node d_solution;
/** the candidate for this class */
Node d_candidate;
/** maps a function-to-synthesize to the above information */
- CandidateInfo d_cinfo;
+ SygusUnifStrategy d_strategy;
- //------------------------------ representation of an enumeration strategy
/** domain-specific enumerator exclusion techniques
*
- * Returns true if the value v for x can be excluded based on a
+ * Returns true if the value v for e can be excluded based on a
* domain-specific exclusion technique like the ones below.
*
* results : the values of v under the input examples,
- * ei : the enumerator information for x,
* exp : if this function returns true, then exp contains a (possibly
* generalize) explanation for why v can be excluded.
*/
- bool getExplanationForEnumeratorExclude(Node x,
+ bool getExplanationForEnumeratorExclude(Node e,
Node v,
std::vector<Node>& results,
- EnumInfo& ei,
std::vector<Node>& exp);
- /** returns true if we can exlude values of x based on negative str.contains
+ /** returns true if we can exlude values of e based on negative str.contains
*
- * Values v for x may be excluded if we realize that the value of v under the
+ * Values v for e may be excluded if we realize that the value of v under the
* substitution for some input example will never be contained in some output
* example. For details on this technique, see NegContainsSygusInvarianceTest
* in sygus_invariance.h.
*
- * This function depends on whether x is being used to enumerate values
+ * This function depends on whether e is being used to enumerate values
* for any node that is conditional in the strategy graph. For example,
* nodes that are children of ITE strategy nodes are conditional. If any node
* is conditional, then this function returns false.
*/
- bool useStrContainsEnumeratorExclude(Node x, EnumInfo& ei);
+ bool useStrContainsEnumeratorExclude(Node e);
/** cache for the above function */
std::map<Node, bool> d_use_str_contains_eexc;
- //------------------------------ strategy registration
- /** collect enumerator types
- *
- * This builds the strategy for enumerated values of type tn for the given
- * role of nrole, for solutions to function-to-synthesize of this class.
- */
- void collectEnumeratorTypes(TypeNode tn, NodeRole nrole);
- /** register enumerator
- *
- * This registers that et is an enumerator of type tn, having enumerator
- * role enum_role.
- *
- * inSearch is whether we will enumerate values based on this enumerator.
- * A strategy node is represented by a (enumerator, node role) pair. Hence,
- * we may use enumerators for which this flag is false to represent strategy
- * nodes that have child strategies.
- */
- void registerEnumerator(Node et,
- TypeNode tn,
- EnumRole enum_role,
- bool inSearch);
- /** infer template */
- bool inferTemplate(unsigned k,
- Node n,
- std::map<Node, unsigned>& templ_var_index,
- std::map<unsigned, unsigned>& templ_injection);
- /** static learn redundant operators
- *
- * This learns static lemmas for pruning enumerative space based on the
- * strategy for the function-to-synthesize of this class, and stores these
- * into lemmas.
- */
- void staticLearnRedundantOps(std::vector<Node>& lemmas);
- /** helper for static learn redundant operators
- *
- * (e, nrole) specify the strategy node in the graph we are currently
- * analyzing, visited stores the nodes we have already visited.
- *
- * This method builds the mapping needs_cons, which maps (master) enumerators
- * to a map from the constructors that it needs.
- *
- * ind is the depth in the strategy graph we are at (for debugging).
- *
- * isCond is whether the current enumerator is conditional (beneath a
- * conditional of an strat_ITE strategy).
- */
- void staticLearnRedundantOps(
- Node e,
- NodeRole nrole,
- std::map<Node, std::map<NodeRole, bool> >& visited,
- std::map<Node, std::map<unsigned, bool> >& needs_cons,
- int ind,
- bool isCond);
- //------------------------------ end strategy registration
-
+ //------------------------------ constructing solutions
/** helper function for construct solution.
*
* Construct a solution based on enumerator e for function-to-synthesize of
std::map<Node, std::vector<unsigned> > incr,
UnifContext& x);
//------------------------------ end constructing solutions
-
- /** represents a strategy for a SyGuS datatype type
- *
- * This represents a possible strategy to apply when processing a strategy
- * node in constructSolution. When applying the strategy represented by this
- * class, we may make recursive calls to the children of the strategy,
- * given in d_cenum. If all recursive calls to constructSolution for these
- * children are successful, say:
- * constructSolution( d_cenum[1], ... ) = t1,
- * ...,
- * constructSolution( d_cenum[n], ... ) = tn,
- * Then, the solution returned by this strategy is
- * d_sol_templ * { d_sol_templ_args -> (t1,...,tn) }
- * where * is application of substitution.
- */
- class EnumTypeInfoStrat
- {
- public:
- /** the type of strategy this represents */
- StrategyType d_this;
- /** the sygus datatype constructor that induced this strategy
- *
- * For example, this may be a sygus datatype whose sygus operator is ITE,
- * if the strategy type above is strat_ITE.
- */
- Node d_cons;
- /** children of this strategy */
- std::vector<std::pair<Node, NodeRole> > d_cenum;
- /** the arguments for the (templated) solution */
- std::vector<Node> d_sol_templ_args;
- /** the template for the solution */
- Node d_sol_templ;
- /** Returns true if argument is valid strategy in context x */
- bool isValid(SygusUnif* pbe, UnifContext& x);
- };
};
} /* CVC4::theory::quantifiers namespace */
projects / cvc5.git / commitdiff