return false;
}
-void UnifContext::initialize(SygusUnif* pbe, Node c)
+void UnifContext::initialize(SygusUnif* pbe)
{
Assert(d_vals.empty());
Assert(d_str_pos.empty());
// initialize with #examples
- Assert(pbe->d_examples.find(c) != pbe->d_examples.end());
- unsigned sz = pbe->d_examples[c].size();
+ unsigned sz = pbe->d_examples.size();
for (unsigned i = 0; i < sz; i++)
{
d_vals.push_back(d_true);
}
- if (!pbe->d_examples_out[c].empty())
+ if (!pbe->d_examples_out.empty())
{
// output type of the examples
- TypeNode exotn = pbe->d_examples_out[c][0].getType();
+ TypeNode exotn = pbe->d_examples_out[0].getType();
if (exotn.isString())
{
std::vector<Node>& enums,
std::vector<Node>& lemmas)
{
+ Assert(d_candidate.isNull());
d_candidate = f;
d_qe = qe;
d_tds = qe->getTermDatabaseSygus();
TypeNode tn = f.getType();
- d_cinfo[f].initialize(f);
+ d_cinfo.initialize(f);
// collect the enumerator types and form the strategy
- collectEnumeratorTypes(f, tn, role_equal);
+ collectEnumeratorTypes(tn, role_equal);
// add the enumerators
- enums.insert(enums.end(),
- d_cinfo[f].d_esym_list.begin(),
- d_cinfo[f].d_esym_list.end());
+ enums.insert(
+ enums.end(), d_cinfo.d_esym_list.begin(), d_cinfo.d_esym_list.end());
// learn redundant ops
- staticLearnRedundantOps(f, lemmas);
+ staticLearnRedundantOps(lemmas);
}
void SygusUnif::resetExamples()
void SygusUnif::addExample(const std::vector<Node>& input, Node output)
{
- d_examples[d_candidate].push_back(input);
- d_examples_out[d_candidate].push_back(output);
+ d_examples.push_back(input);
+ d_examples_out.push_back(output);
}
void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
// iterations.
Node exp_exc;
- std::map<Node, CandidateInfo>::iterator itc = d_cinfo.find(c);
- Assert(itc != d_cinfo.end());
TypeNode xtn = e.getType();
Node bv = d_tds->sygusToBuiltin(v, xtn);
- std::map<Node, std::vector<std::vector<Node> > >::iterator itx =
- d_examples.find(c);
- std::map<Node, std::vector<Node> >::iterator itxo = d_examples_out.find(c);
- Assert(itx != d_examples.end());
- Assert(itxo != d_examples_out.end());
- Assert(itx->second.size() == itxo->second.size());
std::vector<Node> base_results;
// compte the results
- for (unsigned j = 0, size = itx->second.size(); j < size; j++)
+ for (unsigned j = 0, size = d_examples.size(); j < size; j++)
{
- Node res = d_tds->evaluateBuiltin(xtn, bv, itx->second[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(
- c, e, v, base_results, it->second, exp_exc_vec))
+ e, v, base_results, it->second, exp_exc_vec))
{
Assert(!exp_exc_vec.empty());
exp_exc = exp_exc_vec.size() == 1
Node resb;
if (itv->second.getRole() == enum_io)
{
- Node out = itxo->second[j];
+ Node out = d_examples_out[j];
Assert(out.isConst());
resb = res == out ? d_true : d_false;
}
Trace("sygus-pbe-enum")
<< " ...fail : term is not unique" << std::endl;
}
- itc->second.d_cond_count++;
+ d_cinfo.d_cond_count++;
}
if (keep)
{
// notify the parent to retry the build of PBE
- itc->second.d_check_sol = true;
+ d_cinfo.d_check_sol = true;
itv->second.addEnumValue(this, v, results);
}
}
Node SygusUnif::constructSolution()
{
Node c = d_candidate;
- std::map<Node, CandidateInfo>::iterator itc = d_cinfo.find(c);
- Assert(itc != d_cinfo.end());
- if (!itc->second.d_solution.isNull())
+ if (!d_cinfo.d_solution.isNull())
{
// already has a solution
- return itc->second.d_solution;
+ return d_cinfo.d_solution;
}
else
{
// only check if an enumerator updated
- if (itc->second.d_check_sol)
+ if (d_cinfo.d_check_sol)
{
Trace("sygus-pbe") << "Construct solution, #iterations = "
- << itc->second.d_cond_count << std::endl;
- itc->second.d_check_sol = false;
+ << d_cinfo.d_cond_count << std::endl;
+ d_cinfo.d_check_sol = false;
// try multiple times if we have done multiple conditions, due to
// non-determinism
Node vc;
- for (unsigned i = 0; i <= itc->second.d_cond_count; i++)
+ for (unsigned i = 0; i <= d_cinfo.d_cond_count; i++)
{
Trace("sygus-pbe-dt")
<< "ConstructPBE for candidate: " << c << std::endl;
- Node e = itc->second.getRootEnumerator();
+ Node e = d_cinfo.getRootEnumerator();
UnifContext x;
- x.initialize(this, c);
- Node vcc = constructSolution(c, e, role_equal, x, 1);
+ x.initialize(this);
+ Node vcc = constructSolution(e, role_equal, x, 1);
if (!vcc.isNull())
{
if (vc.isNull() || (!vc.isNull()
}
if (!vc.isNull())
{
- itc->second.d_solution = vc;
+ d_cinfo.d_solution = vc;
return vc;
}
Trace("sygus-pbe") << "...failed to solve." << std::endl;
// ----------------------------- establishing enumeration types
-void SygusUnif::registerEnumerator(
- Node et, Node c, TypeNode tn, EnumRole enum_role, bool inSearch)
+void SygusUnif::registerEnumerator(Node et,
+ TypeNode tn,
+ EnumRole enum_role,
+ bool inSearch)
{
if (d_einfo.find(et) == d_einfo.end())
{
// strategy)
if (inSearch)
{
- std::map<TypeNode, Node>::iterator itn =
- d_cinfo[c].d_search_enum.find(tn);
- if (itn == d_cinfo[c].d_search_enum.end())
+ 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[c].d_search_enum[tn] = et;
- d_cinfo[c].d_esym_list.push_back(et);
+ 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
}
}
-void SygusUnif::collectEnumeratorTypes(Node e, TypeNode tn, NodeRole nrole)
+void SygusUnif::collectEnumeratorTypes(TypeNode tn, NodeRole nrole)
{
NodeManager* nm = NodeManager::currentNM();
- if (d_cinfo[e].d_tinfo.find(tn) == d_cinfo[e].d_tinfo.end())
+ 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[e].initializeType(tn);
+ d_cinfo.initializeType(tn);
}
- EnumTypeInfo& eti = d_cinfo[e].d_tinfo[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())
{
if (nrole == role_ite_condition)
{
Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl;
- registerEnumerator(ee, e, tn, erole, true);
+ registerEnumerator(ee, tn, erole, true);
return;
}
// check whether we should also enumerate the current type
Trace("sygus-unif-debug2") << " register this enumerator..." << std::endl;
- registerEnumerator(ee, e, tn, erole, search_this);
+ registerEnumerator(ee, tn, erole, search_this);
if (cop_to_strat.empty())
{
.getDatatype()
.getName()
<< std::endl;
- registerEnumerator(et, e, ct, erole_c, true);
+ 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());
<< "...child type enumerate "
<< ((DatatypeType)ct.toType()).getDatatype().getName()
<< ", node role = " << nrole_c << std::endl;
- collectEnumeratorTypes(e, ct, nrole_c);
+ collectEnumeratorTypes(ct, nrole_c);
// otherwise use the previous
- Assert(d_cinfo[e].d_tinfo[ct].d_enum.find(erole_c)
- != d_cinfo[e].d_tinfo[ct].d_enum.end());
- et = d_cinfo[e].d_tinfo[ct].d_enum[erole_c];
+ 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 "
return true;
}
-void SygusUnif::staticLearnRedundantOps(Node c, std::vector<Node>& lemmas)
+void SygusUnif::staticLearnRedundantOps(std::vector<Node>& lemmas)
{
- for (unsigned i = 0; i < d_cinfo[c].d_esym_list.size(); i++)
+ for (unsigned i = 0; i < d_cinfo.d_esym_list.size(); i++)
{
- Node e = d_cinfo[c].d_esym_list[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") << std::endl;
- Trace("sygus-unif") << "Strategy for candidate " << c
+ 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(c,
- d_cinfo[c].getRootEnumerator(),
- role_equal,
- visited,
- needs_cons,
- 0,
- false);
+ 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)
{
}
void SygusUnif::staticLearnRedundantOps(
- Node c,
Node e,
NodeRole nrole,
std::map<Node, std::map<NodeRole, bool> >& visited,
// enumerator type info
std::map<TypeNode, EnumTypeInfo>::iterator itt =
- d_cinfo[c].d_tinfo.find(etn);
- Assert(itt != d_cinfo[c].d_tinfo.end());
+ d_cinfo.d_tinfo.find(etn);
+ Assert(itt != d_cinfo.d_tinfo.end());
EnumTypeInfo& tinfo = itt->second;
// strategy info
for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
{
// recurse
- staticLearnRedundantOps(c,
- cec.first,
- cec.second,
- visited,
- needs_cons,
- ind + 2,
- newIsCond);
+ 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[c].d_search_enum.find(etn);
- if (itse == d_cinfo[c].d_search_enum.end())
+ std::map<TypeNode, Node>::iterator itse = d_cinfo.d_search_enum.find(etn);
+ if (itse == d_cinfo.d_search_enum.end())
{
return;
}
return false;
}
-bool SygusUnif::getExplanationForEnumeratorExclude(Node c,
- Node x,
+bool SygusUnif::getExplanationForEnumeratorExclude(Node x,
Node v,
std::vector<Node>& results,
EnumInfo& ei,
Trace("sygus-pbe-enum") << std::endl;
}
// check if all examples had longer length that the output
- std::map<Node, std::vector<Node> >::iterator itxo = d_examples_out.find(c);
- Assert(itxo != d_examples_out.end());
- Assert(itxo->second.size() == results.size());
+ 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;
for (unsigned i = 0, size = results.size(); i < size; i++)
{
Assert(results[i].isConst());
- Assert(itxo->second[i].isConst());
- Trace("sygus-pbe-cterm-debug")
- << " " << results[i] << " <> " << itxo->second[i];
- Node cont = nm->mkNode(STRING_STRCTN, itxo->second[i], results[i]);
+ 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)
{
{
// we check invariance with respect to a negative contains test
NegContainsSygusInvarianceTest ncset;
- ncset.init(x, d_examples[c], itxo->second, cmp_indices);
+ ncset.init(x, d_examples, d_examples_out, cmp_indices);
// construct the generalized explanation
d_tds->getExplain()->getExplanationFor(x, v, exp, ncset);
Trace("sygus-pbe-cterm")
return strs[0];
}
-Node SygusUnif::constructSolution(
- Node c, Node e, NodeRole nrole, UnifContext& x, int ind)
+Node SygusUnif::constructSolution(Node e,
+ NodeRole nrole,
+ UnifContext& x,
+ int ind)
{
TypeNode etn = e.getType();
if (Trace.isOn("sygus-pbe-dt-debug"))
Trace("sygus-pbe-dt-debug") << std::endl;
}
// enumerator type info
- std::map<TypeNode, EnumTypeInfo>::iterator itt = d_cinfo[c].d_tinfo.find(etn);
- Assert(itt != d_cinfo[c].d_tinfo.end());
+ std::map<TypeNode, EnumTypeInfo>::iterator itt = d_cinfo.d_tinfo.find(etn);
+ Assert(itt != d_cinfo.d_tinfo.end());
EnumTypeInfo& tinfo = itt->second;
// get the enumerator information
if (success)
{
// get the current examples
- std::map<Node, std::vector<Node> >::iterator itx =
- d_examples_out.find(c);
- Assert(itx != d_examples_out.end());
std::vector<String> ex_vals;
- x.getCurrentStrings(this, itx->second, ex_vals);
+ x.getCurrentStrings(this, d_examples_out, ex_vals);
Assert(itn->second.d_enum_vals.size()
== itn->second.d_enum_vals_res.size());
bool isPrefix = nrole == role_string_prefix;
std::map<Node, unsigned> total_inc;
std::vector<Node> inc_strs;
- std::map<Node, std::vector<Node> >::iterator itx = d_examples_out.find(c);
- Assert(itx != d_examples_out.end());
// make the value of the examples
std::vector<String> ex_vals;
- x.getCurrentStrings(this, itx->second, ex_vals);
+ x.getCurrentStrings(this, d_examples_out, ex_vals);
if (Trace.isOn("sygus-pbe-dt-debug"))
{
indent("sygus-pbe-dt-debug", ind);
indent("sygus-pbe-dt-debug", ind);
Trace("sygus-pbe-dt-debug")
<< "increment string values : " << val_t << " : ";
- Assert(einfo.d_enum_vals_res[i].size() == itx->second.size());
+ Assert(einfo.d_enum_vals_res[i].size() == d_examples_out.size());
unsigned tot = 0;
bool exsuccess = x.getStringIncrement(this,
isPrefix,
}
else
{
- rec_c = constructSolution(c, cenum.first, cenum.second, x, ind + 2);
+ rec_c = constructSolution(cenum.first, cenum.second, x, ind + 2);
}
// undo update the context
{
public:
UnifContext();
- /** this intiializes this context for function-to-synthesize c */
- void initialize(SygusUnif* pbe, Node c);
+ /**
+ * 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
Node d_true;
Node d_false;
/** input of I/O examples */
- std::map<Node, std::vector<std::vector<Node> > > d_examples;
+ std::vector<std::vector<Node> > d_examples;
/** output of I/O examples */
- std::map<Node, std::vector<Node> > d_examples_out;
+ std::vector<Node> d_examples_out;
//------------------------------ representation of a enumeration strategy
/**
/** the candidate for this class */
Node d_candidate;
/** maps a function-to-synthesize to the above information */
- std::map<Node, CandidateInfo> d_cinfo;
+ CandidateInfo d_cinfo;
//------------------------------ representation of an enumeration strategy
/** domain-specific enumerator exclusion techniques
* Returns true if the value v for x can be excluded based on a
* domain-specific exclusion technique like the ones below.
*
- * c : the candidate variable that x is enumerating for,
- * results : the values of v under the input examples of c,
+ * 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 c,
- Node x,
+ bool getExplanationForEnumeratorExclude(Node x,
Node v,
std::vector<Node>& results,
EnumInfo& ei,
/** 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 c.
+ * role of nrole, for solutions to function-to-synthesize of this class.
*/
- void collectEnumeratorTypes(Node c, TypeNode tn, NodeRole nrole);
+ void collectEnumeratorTypes(TypeNode tn, NodeRole nrole);
/** register enumerator
*
- * This registers that et is an enumerator for function-to-synthesize c
- * of type tn, having enumerator role enum_role.
+ * 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, Node c, TypeNode tn, EnumRole enum_role, bool inSearch);
+ void registerEnumerator(Node et,
+ TypeNode tn,
+ EnumRole enum_role,
+ bool inSearch);
/** infer template */
bool inferTemplate(unsigned k,
Node n,
/** static learn redundant operators
*
* This learns static lemmas for pruning enumerative space based on the
- * strategy for the function-to-synthesize c, and stores these into lemmas.
+ * strategy for the function-to-synthesize of this class, and stores these
+ * into lemmas.
*/
- void staticLearnRedundantOps(Node c, std::vector<Node>& 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
* conditional of an strat_ITE strategy).
*/
void staticLearnRedundantOps(
- Node c,
Node e,
NodeRole nrole,
std::map<Node, std::map<NodeRole, bool> >& visited,
/** helper function for construct solution.
*
- * Construct a solution based on enumerator e for function-to-synthesize c
- * with node role nrole in context x.
+ * 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 c, Node e, NodeRole nrole, UnifContext& x, int ind);
+ Node constructSolution(Node e, NodeRole nrole, UnifContext& x, int ind);
/** Heuristically choose the best solved term from solved in context x,
* currently return the first. */
Node constructBestSolvedTerm(std::vector<Node>& solved, UnifContext& x);
* 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( c, d_cenum[1], ... ) = t1,
+ * constructSolution( d_cenum[1], ... ) = t1,
* ...,
- * constructSolution( c, d_cenum[n], ... ) = tn,
+ * 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.
projects / cvc5.git / commitdiff