--- /dev/null
+/********************* */
+/*! \file sygus_unif.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of sygus_unif
+ **/
+
+#include "theory/quantifiers/sygus/sygus_unif.h"
+
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+#include "util/random.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+std::ostream& operator<<(std::ostream& os, EnumRole r)
+{
+ switch (r)
+ {
+ case enum_invalid: os << "INVALID"; break;
+ case enum_io: os << "IO"; break;
+ case enum_ite_condition: os << "CONDITION"; break;
+ case enum_concat_term: os << "CTERM"; break;
+ default: os << "enum_" << static_cast<unsigned>(r); break;
+ }
+ return os;
+}
+
+std::ostream& operator<<(std::ostream& os, NodeRole r)
+{
+ switch (r)
+ {
+ case role_equal: os << "equal"; break;
+ case role_string_prefix: os << "string_prefix"; break;
+ case role_string_suffix: os << "string_suffix"; break;
+ case role_ite_condition: os << "ite_condition"; break;
+ default: os << "role_" << static_cast<unsigned>(r); break;
+ }
+ return os;
+}
+
+EnumRole getEnumeratorRoleForNodeRole(NodeRole r)
+{
+ switch (r)
+ {
+ case role_equal: return enum_io; break;
+ case role_string_prefix: return enum_concat_term; break;
+ case role_string_suffix: return enum_concat_term; break;
+ case role_ite_condition: return enum_ite_condition; break;
+ default: break;
+ }
+ return enum_invalid;
+}
+
+std::ostream& operator<<(std::ostream& os, StrategyType st)
+{
+ switch (st)
+ {
+ case strat_ITE: os << "ITE"; break;
+ case strat_CONCAT_PREFIX: os << "CONCAT_PREFIX"; break;
+ case strat_CONCAT_SUFFIX: os << "CONCAT_SUFFIX"; break;
+ case strat_ID: os << "ID"; break;
+ default: os << "strat_" << static_cast<unsigned>(st); break;
+ }
+ return os;
+}
+
+UnifContext::UnifContext() : d_has_string_pos(role_invalid)
+{
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+bool UnifContext::updateContext(SygusUnif* pbe,
+ std::vector<Node>& vals,
+ bool pol)
+{
+ Assert(d_vals.size() == vals.size());
+ bool changed = false;
+ Node poln = pol ? d_true : d_false;
+ for (unsigned i = 0; i < vals.size(); i++)
+ {
+ if (vals[i] != poln)
+ {
+ if (d_vals[i] == d_true)
+ {
+ d_vals[i] = d_false;
+ changed = true;
+ }
+ }
+ }
+ if (changed)
+ {
+ d_visit_role.clear();
+ }
+ return changed;
+}
+
+bool UnifContext::updateStringPosition(SygusUnif* pbe,
+ std::vector<unsigned>& pos)
+{
+ Assert(pos.size() == d_str_pos.size());
+ bool changed = false;
+ for (unsigned i = 0; i < pos.size(); i++)
+ {
+ if (pos[i] > 0)
+ {
+ d_str_pos[i] += pos[i];
+ changed = true;
+ }
+ }
+ if (changed)
+ {
+ d_visit_role.clear();
+ }
+ return changed;
+}
+
+bool UnifContext::isReturnValueModified()
+{
+ if (d_has_string_pos != role_invalid)
+ {
+ return true;
+ }
+ return false;
+}
+
+void UnifContext::initialize(SygusUnif* pbe, Node c)
+{
+ 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();
+ for (unsigned i = 0; i < sz; i++)
+ {
+ d_vals.push_back(d_true);
+ }
+
+ if (!pbe->d_examples_out[c].empty())
+ {
+ // output type of the examples
+ TypeNode exotn = pbe->d_examples_out[c][0].getType();
+
+ if (exotn.isString())
+ {
+ for (unsigned i = 0; i < sz; i++)
+ {
+ d_str_pos.push_back(0);
+ }
+ }
+ }
+ d_visit_role.clear();
+}
+
+void UnifContext::getCurrentStrings(SygusUnif* pbe,
+ const std::vector<Node>& vals,
+ std::vector<String>& ex_vals)
+{
+ bool isPrefix = d_has_string_pos == role_string_prefix;
+ String dummy;
+ for (unsigned i = 0; i < vals.size(); i++)
+ {
+ if (d_vals[i] == pbe->d_true)
+ {
+ Assert(vals[i].isConst());
+ unsigned pos_value = d_str_pos[i];
+ if (pos_value > 0)
+ {
+ Assert(d_has_string_pos != role_invalid);
+ String s = vals[i].getConst<String>();
+ Assert(pos_value <= s.size());
+ ex_vals.push_back(isPrefix ? s.suffix(s.size() - pos_value)
+ : s.prefix(s.size() - pos_value));
+ }
+ else
+ {
+ ex_vals.push_back(vals[i].getConst<String>());
+ }
+ }
+ else
+ {
+ // irrelevant, add dummy
+ ex_vals.push_back(dummy);
+ }
+ }
+}
+
+bool UnifContext::getStringIncrement(SygusUnif* pbe,
+ bool isPrefix,
+ const std::vector<String>& ex_vals,
+ const std::vector<Node>& vals,
+ std::vector<unsigned>& inc,
+ unsigned& tot)
+{
+ for (unsigned j = 0; j < vals.size(); j++)
+ {
+ unsigned ival = 0;
+ if (d_vals[j] == pbe->d_true)
+ {
+ // example is active in this context
+ Assert(vals[j].isConst());
+ String mystr = vals[j].getConst<String>();
+ ival = mystr.size();
+ if (mystr.size() <= ex_vals[j].size())
+ {
+ if (!(isPrefix ? ex_vals[j].strncmp(mystr, ival)
+ : ex_vals[j].rstrncmp(mystr, ival)))
+ {
+ Trace("sygus-pbe-dt-debug") << "X";
+ return false;
+ }
+ }
+ else
+ {
+ Trace("sygus-pbe-dt-debug") << "X";
+ return false;
+ }
+ }
+ Trace("sygus-pbe-dt-debug") << ival;
+ tot += ival;
+ inc.push_back(ival);
+ }
+ return true;
+}
+bool UnifContext::isStringSolved(SygusUnif* pbe,
+ const std::vector<String>& ex_vals,
+ const std::vector<Node>& vals)
+{
+ for (unsigned j = 0; j < vals.size(); j++)
+ {
+ if (d_vals[j] == pbe->d_true)
+ {
+ // example is active in this context
+ Assert(vals[j].isConst());
+ String mystr = vals[j].getConst<String>();
+ if (ex_vals[j] != mystr)
+ {
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
+// status : 0 : exact, -1 : vals is subset, 1 : vals is superset
+Node SubsumeTrie::addTermInternal(Node t,
+ const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed,
+ bool spol,
+ unsigned index,
+ int status,
+ bool checkExistsOnly,
+ bool checkSubsume)
+{
+ if (index == vals.size())
+ {
+ if (status == 0)
+ {
+ // set the term if checkExistsOnly = false
+ if (d_term.isNull() && !checkExistsOnly)
+ {
+ d_term = t;
+ }
+ }
+ else if (status == 1)
+ {
+ Assert(checkSubsume);
+ // found a subsumed term
+ if (!d_term.isNull())
+ {
+ subsumed.push_back(d_term);
+ if (!checkExistsOnly)
+ {
+ // remove it if checkExistsOnly = false
+ d_term = Node::null();
+ }
+ }
+ }
+ else
+ {
+ Assert(!checkExistsOnly && checkSubsume);
+ }
+ return d_term;
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ // the current value
+ Assert(pol || (vals[index].isConst() && vals[index].getType().isBoolean()));
+ Node cv = pol ? vals[index] : nm->mkConst(!vals[index].getConst<bool>());
+ // if checkExistsOnly = false, check if the current value is subsumed if
+ // checkSubsume = true, if so, don't add
+ if (!checkExistsOnly && checkSubsume)
+ {
+ Assert(cv.isConst() && cv.getType().isBoolean());
+ std::vector<bool> check_subsumed_by;
+ if (status == 0)
+ {
+ if (!cv.getConst<bool>())
+ {
+ check_subsumed_by.push_back(spol);
+ }
+ }
+ else if (status == -1)
+ {
+ check_subsumed_by.push_back(spol);
+ if (!cv.getConst<bool>())
+ {
+ check_subsumed_by.push_back(!spol);
+ }
+ }
+ // check for subsumed nodes
+ for (unsigned i = 0, size = check_subsumed_by.size(); i < size; i++)
+ {
+ bool csbi = check_subsumed_by[i];
+ Node csval = nm->mkConst(csbi);
+ // check if subsumed
+ std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
+ if (itc != d_children.end())
+ {
+ Node ret = itc->second.addTermInternal(t,
+ vals,
+ pol,
+ subsumed,
+ spol,
+ index + 1,
+ -1,
+ checkExistsOnly,
+ checkSubsume);
+ // ret subsumes t
+ if (!ret.isNull())
+ {
+ return ret;
+ }
+ }
+ }
+ }
+ Node ret;
+ std::vector<bool> check_subsume;
+ if (status == 0)
+ {
+ if (checkExistsOnly)
+ {
+ std::map<Node, SubsumeTrie>::iterator itc = d_children.find(cv);
+ if (itc != d_children.end())
+ {
+ ret = itc->second.addTermInternal(t,
+ vals,
+ pol,
+ subsumed,
+ spol,
+ index + 1,
+ 0,
+ checkExistsOnly,
+ checkSubsume);
+ }
+ }
+ else
+ {
+ Assert(spol);
+ ret = d_children[cv].addTermInternal(t,
+ vals,
+ pol,
+ subsumed,
+ spol,
+ index + 1,
+ 0,
+ checkExistsOnly,
+ checkSubsume);
+ if (ret != t)
+ {
+ // we were subsumed by ret, return
+ return ret;
+ }
+ }
+ if (checkSubsume)
+ {
+ Assert(cv.isConst() && cv.getType().isBoolean());
+ // check for subsuming
+ if (cv.getConst<bool>())
+ {
+ check_subsume.push_back(!spol);
+ }
+ }
+ }
+ else if (status == 1)
+ {
+ Assert(checkSubsume);
+ Assert(cv.isConst() && cv.getType().isBoolean());
+ check_subsume.push_back(!spol);
+ if (cv.getConst<bool>())
+ {
+ check_subsume.push_back(spol);
+ }
+ }
+ if (checkSubsume)
+ {
+ // check for subsumed terms
+ for (unsigned i = 0, size = check_subsume.size(); i < size; i++)
+ {
+ Node csval = nm->mkConst<bool>(check_subsume[i]);
+ std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
+ if (itc != d_children.end())
+ {
+ itc->second.addTermInternal(t,
+ vals,
+ pol,
+ subsumed,
+ spol,
+ index + 1,
+ 1,
+ checkExistsOnly,
+ checkSubsume);
+ // clean up
+ if (itc->second.isEmpty())
+ {
+ Assert(!checkExistsOnly);
+ d_children.erase(csval);
+ }
+ }
+ }
+ }
+ return ret;
+}
+
+Node SubsumeTrie::addTerm(Node t,
+ const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed)
+{
+ return addTermInternal(t, vals, pol, subsumed, true, 0, 0, false, true);
+}
+
+Node SubsumeTrie::addCond(Node c, const std::vector<Node>& vals, bool pol)
+{
+ std::vector<Node> subsumed;
+ return addTermInternal(c, vals, pol, subsumed, true, 0, 0, false, false);
+}
+
+void SubsumeTrie::getSubsumed(const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed)
+{
+ addTermInternal(Node::null(), vals, pol, subsumed, true, 0, 1, true, true);
+}
+
+void SubsumeTrie::getSubsumedBy(const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed_by)
+{
+ // flip polarities
+ addTermInternal(
+ Node::null(), vals, !pol, subsumed_by, false, 0, 1, true, true);
+}
+
+void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals,
+ bool pol,
+ std::map<int, std::vector<Node> >& v,
+ unsigned index,
+ int status)
+{
+ if (index == vals.size())
+ {
+ Assert(!d_term.isNull());
+ Assert(std::find(v[status].begin(), v[status].end(), d_term)
+ == v[status].end());
+ v[status].push_back(d_term);
+ }
+ else
+ {
+ Assert(vals[index].isConst() && vals[index].getType().isBoolean());
+ bool curr_val_true = vals[index].getConst<bool>() == pol;
+ for (std::map<Node, SubsumeTrie>::iterator it = d_children.begin();
+ it != d_children.end();
+ ++it)
+ {
+ int new_status = status;
+ // if the current value is true
+ if (curr_val_true)
+ {
+ if (status != 0)
+ {
+ Assert(it->first.isConst() && it->first.getType().isBoolean());
+ new_status = (it->first.getConst<bool>() ? 1 : -1);
+ if (status != -2 && new_status != status)
+ {
+ new_status = 0;
+ }
+ }
+ }
+ it->second.getLeavesInternal(vals, pol, v, index + 1, new_status);
+ }
+ }
+}
+
+void SubsumeTrie::getLeaves(const std::vector<Node>& vals,
+ bool pol,
+ std::map<int, std::vector<Node> >& v)
+{
+ getLeavesInternal(vals, pol, v, 0, -2);
+}
+
+SygusUnif::SygusUnif(QuantifiersEngine* qe) : d_qe(qe)
+{
+ d_tds = qe->getTermDatabaseSygus();
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+SygusUnif::~SygusUnif() {}
+
+void SygusUnif::initialize(Node candidate,
+ std::vector<Node>& lemmas,
+ std::vector<Node>& enums)
+{
+ d_candidate = candidate;
+ // TODO
+}
+
+void SygusUnif::resetExamples()
+{
+ // TODO
+}
+
+void SygusUnif::addExample(const std::vector<Node>& input, Node output)
+{
+ // TODO
+}
+
+void SygusUnif::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
+{
+ // TODO
+}
+
+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())
+ {
+ // already has a solution
+ return itc->second.d_solution;
+ }
+ else
+ {
+ // only check if an enumerator updated
+ if (itc->second.d_check_sol)
+ {
+ Trace("sygus-pbe") << "Construct solution, #iterations = "
+ << itc->second.d_cond_count << std::endl;
+ itc->second.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++)
+ {
+ Trace("sygus-pbe-dt")
+ << "ConstructPBE for candidate: " << c << std::endl;
+ Node e = itc->second.getRootEnumerator();
+ UnifContext x;
+ x.initialize(this, c);
+ Node vcc = constructSolution(c, e, role_equal, x, 1);
+ if (!vcc.isNull())
+ {
+ if (vc.isNull() || (!vc.isNull()
+ && d_tds->getSygusTermSize(vcc)
+ < d_tds->getSygusTermSize(vc)))
+ {
+ Trace("sygus-pbe")
+ << "**** PBE SOLVED : " << c << " = " << vcc << std::endl;
+ Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
+ vc = vcc;
+ }
+ }
+ }
+ if (!vc.isNull())
+ {
+ itc->second.d_solution = vc;
+ return vc;
+ }
+ Trace("sygus-pbe") << "...failed to solve." << std::endl;
+ }
+ return Node::null();
+ }
+}
+
+// ----------------------------- establishing enumeration types
+
+void SygusUnif::registerEnumerator(
+ Node et, Node c, 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(c, 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[c].d_search_enum.find(tn);
+ if (itn == d_cinfo[c].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_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(Node e, TypeNode tn, NodeRole nrole)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ if (d_cinfo[e].d_tinfo.find(tn) == d_cinfo[e].d_tinfo.end())
+ {
+ // register type
+ Trace("sygus-unif") << "Register enumerating type : " << tn << std::endl;
+ d_cinfo[e].initializeType(tn);
+ }
+ EnumTypeInfo& eti = d_cinfo[e].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, e, 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, e, 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, e, 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(e, 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];
+ }
+ 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(Node c, std::vector<Node>& lemmas)
+{
+ for (unsigned i = 0; i < d_cinfo[c].d_esym_list.size(); i++)
+ {
+ Node e = d_cinfo[c].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 " << c
+ << " 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);
+ // 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 c,
+ 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[c].d_tinfo.find(etn);
+ Assert(itt != d_cinfo[c].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(c,
+ 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())
+ {
+ 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
+
+void SygusUnif::addEnumeratedValue(Node x, Node v, std::vector<Node>& lems)
+{
+ std::map<Node, EnumInfo>::iterator it = d_einfo.find(x);
+ 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());
+ Node c = it->second.d_parent_candidate;
+ // The explanation for why the current value should be excluded in future
+ // iterations.
+ Node exp_exc;
+
+ std::map<Node, CandidateInfo>::iterator itc = d_cinfo.find(c);
+ Assert(itc != d_cinfo.end());
+ TypeNode xtn = x.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++)
+ {
+ Node res = d_tds->evaluateBuiltin(xtn, bv, itx->second[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, x, v, base_results, it->second, exp_exc_vec))
+ {
+ Assert(!exp_exc_vec.empty());
+ exp_exc = exp_exc_vec.size() == 1
+ ? exp_exc_vec[0]
+ : NodeManager::currentNM()->mkNode(AND, exp_exc_vec);
+ Trace("sygus-pbe-enum")
+ << " ...fail : term is excluded (domain-specific)" << std::endl;
+ }
+ else
+ {
+ // notify all slaves
+ Assert(!it->second.d_enum_slave.empty());
+ // explanation for why this value should be excluded
+ for (unsigned s = 0; s < it->second.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());
+ Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl;
+ // bool prevIsCover = false;
+ if (itv->second.getRole() == enum_io)
+ {
+ Trace("sygus-pbe-enum") << " IO-Eval of ";
+ // prevIsCover = itv->second.isFeasible();
+ }
+ else
+ {
+ Trace("sygus-pbe-enum") << "Evaluation of ";
+ }
+ 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;
+ std::map<Node, bool> cond_vals;
+ for (unsigned j = 0, size = base_results.size(); j < size; j++)
+ {
+ Node res = base_results[j];
+ Assert(res.isConst());
+ if (!templ.isNull())
+ {
+ TNode tres = res;
+ res = templ.substitute(templ_var, res);
+ res = Rewriter::rewrite(res);
+ Assert(res.isConst());
+ }
+ Node resb;
+ if (itv->second.getRole() == enum_io)
+ {
+ Node out = itxo->second[j];
+ Assert(out.isConst());
+ resb = res == out ? d_true : d_false;
+ }
+ else
+ {
+ resb = res;
+ }
+ cond_vals[resb] = true;
+ results.push_back(resb);
+ if (Trace.isOn("sygus-pbe-enum"))
+ {
+ if (resb.getType().isBoolean())
+ {
+ Trace("sygus-pbe-enum") << (resb == d_true ? "1" : "0");
+ }
+ else
+ {
+ Trace("sygus-pbe-enum") << "?";
+ }
+ }
+ }
+ bool keep = false;
+ if (itv->second.getRole() == enum_io)
+ {
+ // latter is the degenerate case of no examples
+ if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty())
+ {
+ // check subsumbed/subsuming
+ std::vector<Node> subsume;
+ if (cond_vals.find(d_false) == cond_vals.end())
+ {
+ // it is the entire solution, we are done
+ Trace("sygus-pbe-enum")
+ << " ...success, full solution added to PBE pool : "
+ << d_tds->sygusToBuiltin(v) << std::endl;
+ if (!itv->second.isSolved())
+ {
+ itv->second.setSolved(v);
+ // it subsumes everything
+ itv->second.d_term_trie.clear();
+ itv->second.d_term_trie.addTerm(v, results, true, subsume);
+ }
+ keep = true;
+ }
+ else
+ {
+ Node val =
+ itv->second.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());
+ Trace("sygus-pbe-enum")
+ << " and subsumed " << subsume.size() << " terms";
+ }
+ Trace("sygus-pbe-enum")
+ << "! add to PBE pool : " << d_tds->sygusToBuiltin(v)
+ << std::endl;
+ keep = true;
+ }
+ else
+ {
+ Assert(subsume.empty());
+ Trace("sygus-pbe-enum") << " ...fail : subsumed" << std::endl;
+ }
+ }
+ }
+ else
+ {
+ Trace("sygus-pbe-enum")
+ << " ...fail : it does not satisfy examples." << std::endl;
+ }
+ }
+ else
+ {
+ // must be unique up to examples
+ Node val = itv->second.d_term_trie.addCond(v, results, true);
+ if (val == v)
+ {
+ Trace("sygus-pbe-enum") << " ...success! add to PBE pool : "
+ << d_tds->sygusToBuiltin(v) << std::endl;
+ keep = true;
+ }
+ else
+ {
+ Trace("sygus-pbe-enum")
+ << " ...fail : term is not unique" << std::endl;
+ }
+ itc->second.d_cond_count++;
+ }
+ if (keep)
+ {
+ // notify the parent to retry the build of PBE
+ itc->second.d_check_sol = true;
+ itv->second.addEnumValue(this, v, results);
+ }
+ }
+ }
+
+ // exclude this value on subsequent iterations
+ if (exp_exc.isNull())
+ {
+ // if we did not already explain why this should be excluded, use default
+ exp_exc = d_tds->getExplain()->getExplanationForEquality(x, v);
+ }
+ exp_exc = exp_exc.negate();
+ Trace("sygus-pbe-enum-lemma")
+ << "SygusUnif : enumeration exclude lemma : " << exp_exc << std::endl;
+ lems.push_back(exp_exc);
+}
+
+bool SygusUnif::useStrContainsEnumeratorExclude(Node x, EnumInfo& ei)
+{
+ TypeNode xbt = d_tds->sygusToBuiltinType(x.getType());
+ if (xbt.isString())
+ {
+ std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(x);
+ 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;
+ for (const Node& sn : ei.d_enum_slave)
+ {
+ std::map<Node, EnumInfo>::iterator itv = d_einfo.find(sn);
+ EnumRole er = itv->second.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;
+ return false;
+ }
+ if (itv->second.isConditional())
+ {
+ Trace("sygus-pbe-enum-debug")
+ << " conditional slave : " << sn << std::endl;
+ d_use_str_contains_eexc[x] = false;
+ return false;
+ }
+ }
+ Trace("sygus-pbe-enum-debug")
+ << "...can use str.contains exclusion." << std::endl;
+ return d_use_str_contains_eexc[x];
+ }
+ return false;
+}
+
+bool SygusUnif::getExplanationForEnumeratorExclude(Node c,
+ Node x,
+ Node v,
+ std::vector<Node>& results,
+ EnumInfo& ei,
+ std::vector<Node>& exp)
+{
+ if (useStrContainsEnumeratorExclude(x, ei))
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ // This check whether the example evaluates to something that is larger than
+ // the output for some input/output pair. If so, then this term is never
+ // useful. We generalize its explanation below.
+
+ if (Trace.isOn("sygus-pbe-cterm-debug"))
+ {
+ Trace("sygus-pbe-enum") << std::endl;
+ }
+ // check if all examples had longer length that the output
+ 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());
+ Trace("sygus-pbe-cterm-debug")
+ << "Check enumerator exclusion for " << x << " -> "
+ << d_tds->sygusToBuiltin(v) << " based on str.contains." << std::endl;
+ std::vector<unsigned> cmp_indices;
+ for (unsigned i = 0, size = results.size(); i < size; i++)
+ {
+ Assert(results[i].isConst());
+ Assert(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]);
+ Node contr = Rewriter::rewrite(cont);
+ if (contr == d_false)
+ {
+ cmp_indices.push_back(i);
+ Trace("sygus-pbe-cterm-debug") << "...not contained." << std::endl;
+ }
+ else
+ {
+ Trace("sygus-pbe-cterm-debug") << "...contained." << std::endl;
+ }
+ }
+ /* FIXME
+ if (!cmp_indices.empty())
+ {
+ // we check invariance with respect to a negative contains test
+ NegContainsSygusInvarianceTest ncset;
+ ncset.init(d_parent, x, itxo->second, cmp_indices);
+ // construct the generalized explanation
+ d_tds->getExplain()->getExplanationFor(x, v, exp, ncset);
+ Trace("sygus-pbe-cterm")
+ << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin(v)
+ << " due to negative containment." << std::endl;
+ return true;
+ }
+ */
+ }
+ return false;
+}
+
+void SygusUnif::EnumInfo::addEnumValue(SygusUnif* pbe,
+ Node v,
+ std::vector<Node>& results)
+{
+ d_enum_val_to_index[v] = d_enum_vals.size();
+ d_enum_vals.push_back(v);
+ d_enum_vals_res.push_back(results);
+}
+
+void SygusUnif::EnumInfo::initialize(Node c, EnumRole role)
+{
+ d_parent_candidate = c;
+ 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)
+{
+ Assert(!solved.empty());
+ return solved[0];
+}
+
+Node SygusUnif::constructBestStringSolvedTerm(std::vector<Node>& solved,
+ UnifContext& x)
+{
+ Assert(!solved.empty());
+ return solved[0];
+}
+
+Node SygusUnif::constructBestSolvedConditional(std::vector<Node>& solved,
+ UnifContext& x)
+{
+ Assert(!solved.empty());
+ return solved[0];
+}
+
+Node SygusUnif::constructBestConditional(std::vector<Node>& conds,
+ UnifContext& x)
+{
+ Assert(!conds.empty());
+ double r = Random::getRandom().pickDouble(0.0, 1.0);
+ unsigned cindex = r * conds.size();
+ if (cindex > conds.size())
+ {
+ cindex = conds.size() - 1;
+ }
+ return conds[cindex];
+}
+
+Node SygusUnif::constructBestStringToConcat(
+ std::vector<Node> strs,
+ std::map<Node, unsigned> total_inc,
+ std::map<Node, std::vector<unsigned> > incr,
+ UnifContext& x)
+{
+ Assert(!strs.empty());
+ std::random_shuffle(strs.begin(), strs.end());
+ // prefer one that has incremented by more than 0
+ for (const Node& ns : strs)
+ {
+ if (total_inc[ns] > 0)
+ {
+ return ns;
+ }
+ }
+ return strs[0];
+}
+
+Node SygusUnif::constructSolution(
+ Node c, Node e, NodeRole nrole, UnifContext& x, int ind)
+{
+ TypeNode etn = e.getType();
+ if (Trace.isOn("sygus-pbe-dt-debug"))
+ {
+ indent("sygus-pbe-dt-debug", ind);
+ Trace("sygus-pbe-dt-debug") << "ConstructPBE: (" << e << ", " << nrole
+ << ") for type " << etn << " in context ";
+ print_val("sygus-pbe-dt-debug", x.d_vals);
+ if (x.d_has_string_pos != role_invalid)
+ {
+ Trace("sygus-pbe-dt-debug") << ", string context [" << x.d_has_string_pos;
+ for (unsigned i = 0, size = x.d_str_pos.size(); i < size; i++)
+ {
+ Trace("sygus-pbe-dt-debug") << " " << x.d_str_pos[i];
+ }
+ Trace("sygus-pbe-dt-debug") << "]";
+ }
+ Trace("sygus-pbe-dt-debug") << std::endl;
+ }
+ // enumerator type info
+ std::map<TypeNode, EnumTypeInfo>::iterator itt = d_cinfo[c].d_tinfo.find(etn);
+ Assert(itt != d_cinfo[c].d_tinfo.end());
+ EnumTypeInfo& tinfo = itt->second;
+
+ // get the enumerator information
+ std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e);
+ Assert(itn != d_einfo.end());
+ EnumInfo& einfo = itn->second;
+
+ Node ret_dt;
+ if (nrole == role_equal)
+ {
+ if (!x.isReturnValueModified())
+ {
+ if (einfo.isSolved())
+ {
+ // this type has a complete solution
+ ret_dt = einfo.getSolved();
+ indent("sygus-pbe-dt", ind);
+ Trace("sygus-pbe-dt") << "return PBE: success : solved "
+ << d_tds->sygusToBuiltin(ret_dt) << std::endl;
+ Assert(!ret_dt.isNull());
+ }
+ else
+ {
+ // could be conditionally solved
+ std::vector<Node> subsumed_by;
+ einfo.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by);
+ if (!subsumed_by.empty())
+ {
+ ret_dt = constructBestSolvedTerm(subsumed_by, x);
+ indent("sygus-pbe-dt", ind);
+ Trace("sygus-pbe-dt") << "return PBE: success : conditionally solved"
+ << d_tds->sygusToBuiltin(ret_dt) << std::endl;
+ }
+ else
+ {
+ indent("sygus-pbe-dt-debug", ind);
+ Trace("sygus-pbe-dt-debug")
+ << " ...not currently conditionally solved." << std::endl;
+ }
+ }
+ }
+ if (ret_dt.isNull())
+ {
+ if (d_tds->sygusToBuiltinType(e.getType()).isString())
+ {
+ // check if a current value that closes all examples
+ // get the term enumerator for this type
+ 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())
+ {
+ Node et = itnt->second;
+ itet = d_einfo.find(et);
+ Assert(itet != d_einfo.end());
+ }
+ else
+ {
+ success = false;
+ }
+ 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);
+ Assert(itn->second.d_enum_vals.size()
+ == itn->second.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++)
+ {
+ if (x.isStringSolved(
+ this, ex_vals, itet->second.d_enum_vals_res[i]))
+ {
+ str_solved.push_back(itet->second.d_enum_vals[i]);
+ }
+ }
+ if (!str_solved.empty())
+ {
+ ret_dt = constructBestStringSolvedTerm(str_solved, x);
+ indent("sygus-pbe-dt", ind);
+ Trace("sygus-pbe-dt") << "return PBE: success : string solved "
+ << d_tds->sygusToBuiltin(ret_dt) << std::endl;
+ }
+ else
+ {
+ indent("sygus-pbe-dt-debug", ind);
+ Trace("sygus-pbe-dt-debug")
+ << " ...not currently string solved." << std::endl;
+ }
+ }
+ }
+ }
+ }
+ else if (nrole == role_string_prefix || nrole == role_string_suffix)
+ {
+ // check if each return value is a prefix/suffix of all open examples
+ if (!x.isReturnValueModified() || x.d_has_string_pos == nrole)
+ {
+ std::map<Node, std::vector<unsigned> > incr;
+ bool isPrefix = nrole == role_string_prefix;
+ std::map<Node, unsigned> total_inc;
+ std::vector<Node> inc_strs;
+ 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);
+ if (Trace.isOn("sygus-pbe-dt-debug"))
+ {
+ indent("sygus-pbe-dt-debug", ind);
+ Trace("sygus-pbe-dt-debug") << "current strings : " << std::endl;
+ for (unsigned i = 0, size = ex_vals.size(); i < size; i++)
+ {
+ indent("sygus-pbe-dt-debug", ind + 1);
+ Trace("sygus-pbe-dt-debug") << ex_vals[i] << std::endl;
+ }
+ }
+
+ // check if there is a value for which is a prefix/suffix of all active
+ // examples
+ Assert(einfo.d_enum_vals.size() == einfo.d_enum_vals_res.size());
+
+ for (unsigned i = 0, size = einfo.d_enum_vals.size(); i < size; i++)
+ {
+ Node val_t = einfo.d_enum_vals[i];
+ 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());
+ unsigned tot = 0;
+ bool exsuccess = x.getStringIncrement(this,
+ isPrefix,
+ ex_vals,
+ einfo.d_enum_vals_res[i],
+ incr[val_t],
+ tot);
+ if (!exsuccess)
+ {
+ incr.erase(val_t);
+ Trace("sygus-pbe-dt-debug") << "...fail" << std::endl;
+ }
+ else
+ {
+ total_inc[val_t] = tot;
+ inc_strs.push_back(val_t);
+ Trace("sygus-pbe-dt-debug")
+ << "...success, total increment = " << tot << std::endl;
+ }
+ }
+
+ if (!incr.empty())
+ {
+ ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr, x);
+ Assert(!ret_dt.isNull());
+ indent("sygus-pbe-dt", ind);
+ Trace("sygus-pbe-dt")
+ << "PBE: CONCAT strategy : choose " << (isPrefix ? "pre" : "suf")
+ << "fix value " << d_tds->sygusToBuiltin(ret_dt) << std::endl;
+ // update the context
+ bool ret = x.updateStringPosition(this, incr[ret_dt]);
+ AlwaysAssert(ret == (total_inc[ret_dt] > 0));
+ x.d_has_string_pos = nrole;
+ }
+ else
+ {
+ indent("sygus-pbe-dt", ind);
+ Trace("sygus-pbe-dt") << "PBE: failed CONCAT strategy, no values are "
+ << (isPrefix ? "pre" : "suf")
+ << "fix of all examples." << std::endl;
+ }
+ }
+ else
+ {
+ indent("sygus-pbe-dt", ind);
+ Trace("sygus-pbe-dt")
+ << "PBE: failed CONCAT strategy, prefix/suffix mismatch."
+ << std::endl;
+ }
+ }
+ if (ret_dt.isNull() && !einfo.isTemplated())
+ {
+ // we will try a single strategy
+ EnumTypeInfoStrat* etis = nullptr;
+ std::map<NodeRole, StrategyNode>::iterator itsn =
+ tinfo.d_snodes.find(nrole);
+ if (itsn != tinfo.d_snodes.end())
+ {
+ // strategy info
+ StrategyNode& snode = itsn->second;
+ if (x.d_visit_role[e].find(nrole) == x.d_visit_role[e].end())
+ {
+ x.d_visit_role[e][nrole] = true;
+ // try a random strategy
+ if (snode.d_strats.size() > 1)
+ {
+ std::random_shuffle(snode.d_strats.begin(), snode.d_strats.end());
+ }
+ // get an eligible strategy index
+ unsigned sindex = 0;
+ while (sindex < snode.d_strats.size()
+ && !snode.d_strats[sindex]->isValid(this, x))
+ {
+ sindex++;
+ }
+ // if we found a eligible strategy
+ if (sindex < snode.d_strats.size())
+ {
+ etis = snode.d_strats[sindex];
+ }
+ }
+ }
+ if (etis != nullptr)
+ {
+ StrategyType strat = etis->d_this;
+ indent("sygus-pbe-dt", ind + 1);
+ Trace("sygus-pbe-dt")
+ << "...try STRATEGY " << strat << "..." << std::endl;
+
+ std::map<unsigned, Node> look_ahead_solved_children;
+ std::vector<Node> dt_children_cons;
+ bool success = true;
+
+ // for ITE
+ Node split_cond_enum;
+ int split_cond_res_index = -1;
+
+ for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++)
+ {
+ indent("sygus-pbe-dt", ind + 1);
+ Trace("sygus-pbe-dt")
+ << "construct PBE child #" << sc << "..." << std::endl;
+ Node rec_c;
+ std::map<unsigned, Node>::iterator itla =
+ look_ahead_solved_children.find(sc);
+ if (itla != look_ahead_solved_children.end())
+ {
+ rec_c = itla->second;
+ indent("sygus-pbe-dt-debug", ind + 1);
+ Trace("sygus-pbe-dt-debug")
+ << "ConstructPBE: look ahead solved : "
+ << d_tds->sygusToBuiltin(rec_c) << std::endl;
+ }
+ else
+ {
+ std::pair<Node, NodeRole>& cenum = etis->d_cenum[sc];
+
+ // update the context
+ std::vector<Node> prev;
+ if (strat == strat_ITE && sc > 0)
+ {
+ std::map<Node, EnumInfo>::iterator itnc =
+ d_einfo.find(split_cond_enum);
+ Assert(itnc != d_einfo.end());
+ Assert(split_cond_res_index >= 0);
+ Assert(split_cond_res_index
+ < (int)itnc->second.d_enum_vals_res.size());
+ prev = x.d_vals;
+ bool ret = x.updateContext(
+ this,
+ itnc->second.d_enum_vals_res[split_cond_res_index],
+ sc == 1);
+ AlwaysAssert(ret);
+ }
+
+ // recurse
+ if (strat == strat_ITE && sc == 0)
+ {
+ 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;
+
+ // only used if the return value is not modified
+ if (!x.isReturnValueModified())
+ {
+ if (x.d_uinfo.find(ce) == x.d_uinfo.end())
+ {
+ Trace("sygus-pbe-dt-debug2")
+ << " reg : PBE: Look for direct solutions for conditional "
+ "enumerator "
+ << ce << " ... " << std::endl;
+ Assert(einfo_child.d_enum_vals.size()
+ == einfo_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());
+ 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();
+ k < size;
+ k++)
+ {
+ Node cond = einfo_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);
+ Trace("sygus-pbe-dt-debug2")
+ << " reg : PBE: " << d_tds->sygusToBuiltin(cond)
+ << " has " << solved.size() << " solutions in branch "
+ << i << std::endl;
+ if (!solved.empty())
+ {
+ Node slv = constructBestSolvedTerm(solved, x);
+ Trace("sygus-pbe-dt-debug2")
+ << " reg : PBE: ..." << d_tds->sygusToBuiltin(slv)
+ << " is a solution under branch " << i;
+ Trace("sygus-pbe-dt-debug2")
+ << " of condition " << d_tds->sygusToBuiltin(cond)
+ << std::endl;
+ x.d_uinfo[ce].d_look_ahead_sols[cond][i] = slv;
+ }
+ }
+ }
+ }
+ }
+
+ // get the conditionals in the current context : they must be
+ // distinguishable
+ std::map<int, std::vector<Node> > possible_cond;
+ std::map<Node, int> solved_cond; // stores branch
+ einfo_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond);
+
+ std::map<int, std::vector<Node> >::iterator itpc =
+ possible_cond.find(0);
+ if (itpc != possible_cond.end())
+ {
+ if (Trace.isOn("sygus-pbe-dt-debug"))
+ {
+ indent("sygus-pbe-dt-debug", ind + 1);
+ Trace("sygus-pbe-dt-debug")
+ << "PBE : We have " << itpc->second.size()
+ << " distinguishable conditionals:" << std::endl;
+ for (Node& cond : itpc->second)
+ {
+ indent("sygus-pbe-dt-debug", ind + 2);
+ Trace("sygus-pbe-dt-debug")
+ << d_tds->sygusToBuiltin(cond) << std::endl;
+ }
+ }
+
+ // static look ahead conditional : choose conditionals that have
+ // solved terms in at least one branch
+ // only applicable if we have not modified the return value
+ std::map<int, std::vector<Node> > solved_cond;
+ if (!x.isReturnValueModified())
+ {
+ Assert(x.d_uinfo.find(ce) != x.d_uinfo.end());
+ int solve_max = 0;
+ for (Node& cond : itpc->second)
+ {
+ std::map<Node, std::map<unsigned, Node> >::iterator itla =
+ x.d_uinfo[ce].d_look_ahead_sols.find(cond);
+ if (itla != x.d_uinfo[ce].d_look_ahead_sols.end())
+ {
+ int nsolved = itla->second.size();
+ solve_max = nsolved > solve_max ? nsolved : solve_max;
+ solved_cond[nsolved].push_back(cond);
+ }
+ }
+ int n = solve_max;
+ while (n > 0)
+ {
+ if (!solved_cond[n].empty())
+ {
+ rec_c = constructBestSolvedConditional(solved_cond[n], x);
+ indent("sygus-pbe-dt", ind + 1);
+ Trace("sygus-pbe-dt")
+ << "PBE: ITE strategy : choose solved conditional "
+ << d_tds->sygusToBuiltin(rec_c) << " with " << n
+ << " solved children..." << std::endl;
+ std::map<Node, std::map<unsigned, Node> >::iterator itla =
+ x.d_uinfo[ce].d_look_ahead_sols.find(rec_c);
+ Assert(itla != x.d_uinfo[ce].d_look_ahead_sols.end());
+ for (std::pair<const unsigned, Node>& las : itla->second)
+ {
+ look_ahead_solved_children[las.first] = las.second;
+ }
+ break;
+ }
+ n--;
+ }
+ }
+
+ // otherwise, guess a conditional
+ if (rec_c.isNull())
+ {
+ rec_c = constructBestConditional(itpc->second, x);
+ Assert(!rec_c.isNull());
+ indent("sygus-pbe-dt", ind);
+ Trace("sygus-pbe-dt")
+ << "PBE: ITE strategy : choose random conditional "
+ << d_tds->sygusToBuiltin(rec_c) << std::endl;
+ }
+ }
+ else
+ {
+ // TODO (#1250) : degenerate case where children have different
+ // types?
+ indent("sygus-pbe-dt", ind);
+ Trace("sygus-pbe-dt") << "return PBE: failed ITE strategy, "
+ "cannot find a distinguishable condition"
+ << std::endl;
+ }
+ if (!rec_c.isNull())
+ {
+ Assert(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];
+ split_cond_enum = ce;
+ Assert(split_cond_res_index >= 0);
+ Assert(split_cond_res_index
+ < (int)einfo_child.d_enum_vals_res.size());
+ }
+ }
+ else
+ {
+ rec_c = constructSolution(c, cenum.first, cenum.second, x, ind + 2);
+ }
+
+ // undo update the context
+ if (strat == strat_ITE && sc > 0)
+ {
+ x.d_vals = prev;
+ }
+ }
+ if (!rec_c.isNull())
+ {
+ dt_children_cons.push_back(rec_c);
+ }
+ else
+ {
+ success = false;
+ break;
+ }
+ }
+ if (success)
+ {
+ Assert(dt_children_cons.size() == etis->d_sol_templ_args.size());
+ // ret_dt = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR,
+ // dt_children );
+ ret_dt = etis->d_sol_templ;
+ ret_dt = ret_dt.substitute(etis->d_sol_templ_args.begin(),
+ etis->d_sol_templ_args.end(),
+ dt_children_cons.begin(),
+ dt_children_cons.end());
+ indent("sygus-pbe-dt-debug", ind);
+ Trace("sygus-pbe-dt-debug")
+ << "PBE: success : constructed for strategy " << strat << std::endl;
+ }
+ else
+ {
+ indent("sygus-pbe-dt-debug", ind);
+ Trace("sygus-pbe-dt-debug")
+ << "PBE: failed for strategy " << strat << std::endl;
+ }
+ }
+ }
+
+ if (!ret_dt.isNull())
+ {
+ Assert(ret_dt.getType() == e.getType());
+ }
+ indent("sygus-pbe-dt", ind);
+ Trace("sygus-pbe-dt") << "ConstructPBE: returned " << ret_dt << std::endl;
+ return ret_dt;
+}
+
+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))
+ {
+ for (int i = 0; i < ind; i++)
+ {
+ Trace(c) << " ";
+ }
+ }
+}
+
+void SygusUnif::print_val(const char* c, std::vector<Node>& vals, bool pol)
+{
+ if (Trace.isOn(c))
+ {
+ for (unsigned i = 0; i < vals.size(); i++)
+ {
+ Trace(c) << ((pol ? vals[i].getConst<bool>() : !vals[i].getConst<bool>())
+ ? "1"
+ : "0");
+ }
+ }
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file sygus_unif.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief sygus_unif
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H
+
+#include <map>
+#include "expr/node.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** roles for enumerators
+ *
+ * This indicates the role of an enumerator that is allocated by approaches
+ * for synthesis-by-unification (see details below).
+ * io : the enumerator should enumerate values that are overall solutions
+ * for the function-to-synthesize,
+ * ite_condition : the enumerator should enumerate values that are useful
+ * in ite conditions in the ITE strategy,
+ * concat_term : the enumerator should enumerate values that are used as
+ * components of string concatenation solutions.
+ */
+enum EnumRole
+{
+ enum_invalid,
+ enum_io,
+ enum_ite_condition,
+ enum_concat_term,
+};
+std::ostream& operator<<(std::ostream& os, EnumRole r);
+
+/** roles for strategy nodes
+ *
+ * This indicates the role of a strategy node, which is a subprocedure of
+ * SygusUnif::constructSolution (see details below).
+ * equal : the node constructed must be equal to the overall solution for
+ * the function-to-synthesize,
+ * string_prefix/suffix : the node constructed must be a prefix/suffix
+ * of the function-to-synthesize,
+ * ite_condition : the node constructed must be a condition that makes some
+ * active input examples true and some input examples false.
+ */
+enum NodeRole
+{
+ role_invalid,
+ role_equal,
+ role_string_prefix,
+ role_string_suffix,
+ role_ite_condition,
+};
+std::ostream& operator<<(std::ostream& os, NodeRole r);
+
+/** enumerator role for node role */
+EnumRole getEnumeratorRoleForNodeRole(NodeRole r);
+
+/** strategy types
+ *
+ * This indicates a strategy for synthesis-by-unification (see details below).
+ * ITE : strategy for constructing if-then-else solutions via decision
+ * tree learning techniques,
+ * CONCAT_PREFIX/SUFFIX : strategy for constructing string concatenation
+ * solutions via a divide and conquer approach,
+ * ID : identity strategy used for calling strategies on child type through
+ * an identity function.
+ */
+enum StrategyType
+{
+ strat_INVALID,
+ strat_ITE,
+ strat_CONCAT_PREFIX,
+ strat_CONCAT_SUFFIX,
+ strat_ID,
+};
+std::ostream& operator<<(std::ostream& os, StrategyType st);
+
+class SygusUnif;
+
+/** Unification context
+ *
+ * This class maintains state information during calls to
+ * SygusUnif::constructSolution, which implements unification-based
+ * approaches for construction solutions to synthesis conjectures.
+ */
+class UnifContext
+{
+ public:
+ UnifContext();
+ /** this intiializes this context for function-to-synthesize c */
+ void initialize(SygusUnif* pbe, Node c);
+
+ //----------for ITE strategy
+ /** the value of the context conditional
+ *
+ * This stores a list of Boolean constants that is the same length of the
+ * number of input/output example pairs we are considering. For each i,
+ * if d_vals[i] = true, i/o pair #i is active according to this context
+ * if d_vals[i] = false, i/o pair #i is inactive according to this context
+ */
+ std::vector<Node> d_vals;
+ /** update the examples
+ *
+ * if pol=true, this method updates d_vals to d_vals & vals
+ * if pol=false, this method updates d_vals to d_vals & ( ~vals )
+ */
+ bool updateContext(SygusUnif* pbe, std::vector<Node>& vals, bool pol);
+ //----------end for ITE strategy
+
+ //----------for CONCAT strategies
+ /** the position in the strings
+ *
+ * For each i/o example pair, this stores the length of the current solution
+ * for the input of the pair, where the solution for that input is a prefix
+ * or
+ * suffix of the output of the pair. For example, if our i/o pairs are:
+ * f( "abcd" ) = "abcdcd"
+ * f( "aa" ) = "aacd"
+ * If the solution we have currently constructed is str.++( x1, "c", ... ),
+ * then d_str_pos = ( 5, 3 ), where notice that
+ * str.++( "abc", "c" ) is a prefix of "abcdcd" and
+ * str.++( "aa", "c" ) is a prefix of "aacd".
+ */
+ std::vector<unsigned> d_str_pos;
+ /** has string position
+ *
+ * Whether the solution positions indicate a prefix or suffix of the output
+ * examples. If this is role_invalid, then we have not updated the string
+ * position.
+ */
+ NodeRole d_has_string_pos;
+ /** update the string examples
+ *
+ * This method updates d_str_pos to d_str_pos + pos.
+ */
+ bool updateStringPosition(SygusUnif* pbe, std::vector<unsigned>& pos);
+ /** get current strings
+ *
+ * This returns the prefix/suffix of the string constants stored in vals
+ * of size d_str_pos, and stores the result in ex_vals. For example, if vals
+ * is (abcdcd", "aacde") and d_str_pos = ( 5, 3 ), then we add
+ * "d" and "de" to ex_vals.
+ */
+ void getCurrentStrings(SygusUnif* pbe,
+ const std::vector<Node>& vals,
+ std::vector<String>& ex_vals);
+ /** get string increment
+ *
+ * If this method returns true, then inc and tot are updated such that
+ * for all active indices i,
+ * vals[i] is a prefix (or suffix if isPrefix=false) of ex_vals[i], and
+ * inc[i] = str.len(vals[i])
+ * for all inactive indices i, inc[i] = 0
+ * We set tot to the sum of inc[i] for i=1,...,n. This indicates the total
+ * number of characters incremented across all examples.
+ */
+ bool getStringIncrement(SygusUnif* pbe,
+ bool isPrefix,
+ const std::vector<String>& ex_vals,
+ const std::vector<Node>& vals,
+ std::vector<unsigned>& inc,
+ unsigned& tot);
+ /** returns true if ex_vals[i] = vals[i] for all active indices i. */
+ bool isStringSolved(SygusUnif* pbe,
+ const std::vector<String>& ex_vals,
+ const std::vector<Node>& vals);
+ //----------end for CONCAT strategies
+
+ /** is return value modified?
+ *
+ * This returns true if we are currently in a state where the return value
+ * of the solution has been modified, e.g. by a previous node that solved
+ * for a prefix.
+ */
+ bool isReturnValueModified();
+ /** visited role
+ *
+ * This is the current set of enumerator/node role pairs we are currently
+ * visiting. This set is cleared when the context is updated.
+ */
+ std::map<Node, std::map<NodeRole, bool> > d_visit_role;
+
+ /** unif context enumerator information */
+ class UEnumInfo
+ {
+ public:
+ UEnumInfo() {}
+ /** map from conditions and branch positions to a solved node
+ *
+ * For example, if we have:
+ * f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1
+ * Then, valid entries in this map is:
+ * d_look_ahead_sols[x>0][1] = x+1
+ * d_look_ahead_sols[x>0][2] = 1
+ * For the first entry, notice that for all input examples such that x>0
+ * evaluates to true, which are (1) and (3), we have that their output
+ * values for x+1 under the substitution that maps x to the input value,
+ * resulting in 2 and 4, are equal to the output value for the respective
+ * pairs.
+ */
+ std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols;
+ };
+ /** map from enumerators to the above info class */
+ std::map<Node, UEnumInfo> d_uinfo;
+
+ private:
+ /** true and false nodes */
+ Node d_true;
+ Node d_false;
+};
+
+/** Subsumption trie
+*
+* This class manages a set of terms for a PBE sygus enumerator.
+*
+* In PBE sygus, we are interested in, for each term t, the set of I/O examples
+* that it satisfies, which can be represented by a vector of Booleans.
+* For example, given conjecture:
+* f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 ^ f( 5 ) = 5
+* If solutions for f are of the form (lambda x. [term]), then:
+* Term x satisfies 0001,
+* Term x+1 satisfies 1100,
+* Term 2 satisfies 0100.
+* Above, term 2 is subsumed by term x+1, since the set of I/O examples that
+* x+1 satisfies are a superset of those satisfied by 2.
+*/
+class SubsumeTrie
+{
+ public:
+ SubsumeTrie() {}
+ /**
+ * Adds term t to the trie, removes all terms that are subsumed by t from the
+ * trie and adds them to subsumed. The set of I/O examples that t satisfies
+ * is given by (pol ? vals : !vals).
+ */
+ Node addTerm(Node t,
+ const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed);
+ /**
+ * Adds term c to the trie, without calculating/updating based on
+ * subsumption. This is useful for using this class to store conditionals
+ * in ITE strategies, where any conditional whose set of vals is unique
+ * (as opposed to not subsumed) is useful.
+ */
+ Node addCond(Node c, const std::vector<Node>& vals, bool pol);
+ /**
+ * Returns the set of terms that are subsumed by (pol ? vals : !vals).
+ */
+ void getSubsumed(const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed);
+ /**
+ * Returns the set of terms that subsume (pol ? vals : !vals). This
+ * is for instance useful when determining whether there exists a term
+ * that satisfies all active examples in the decision tree learning
+ * algorithm.
+ */
+ void getSubsumedBy(const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed_by);
+ /**
+ * Get the leaves of the trie, which we store in the map v.
+ * v[-1] stores the children that always evaluate to !pol,
+ * v[1] stores the children that always evaluate to pol,
+ * v[0] stores the children that both evaluate to true and false for at least
+ * one example.
+ */
+ void getLeaves(const std::vector<Node>& vals,
+ bool pol,
+ std::map<int, std::vector<Node> >& v);
+ /** is this trie empty? */
+ bool isEmpty() { return d_term.isNull() && d_children.empty(); }
+ /** clear this trie */
+ void clear()
+ {
+ d_term = Node::null();
+ d_children.clear();
+ }
+
+ private:
+ /** the term at this node */
+ Node d_term;
+ /** the children nodes of this trie */
+ std::map<Node, SubsumeTrie> d_children;
+ /** helper function for above functions */
+ Node addTermInternal(Node t,
+ const std::vector<Node>& vals,
+ bool pol,
+ std::vector<Node>& subsumed,
+ bool spol,
+ unsigned index,
+ int status,
+ bool checkExistsOnly,
+ bool checkSubsume);
+ /** helper function for above functions */
+ void getLeavesInternal(const std::vector<Node>& vals,
+ bool pol,
+ std::map<int, std::vector<Node> >& v,
+ unsigned index,
+ int status);
+};
+
+/** Sygus unification utility
+ *
+ * This utility implements synthesis-by-unification style approaches for a
+ * single function to synthesize f.
+ * These approaches include a combination of:
+ * (1) Decision tree learning, inspired by Alur et al TACAS 2017,
+ * (2) Divide-and-conquer via string concatenation.
+ *
+ * This class maintains:
+ * (1) A "strategy tree" based on the syntactic restrictions for f that is
+ * constructed during initialize,
+ * (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.
+ *
+ * Based on the above, solutions can be constructed via calls to
+ * constructSolution.
+ */
+class SygusUnif
+{
+ friend class UnifContext;
+
+ public:
+ SygusUnif(QuantifiersEngine* qe);
+ ~SygusUnif();
+
+ /** initialize
+ *
+ * This initializes this class with function-to-synthesize f. We also call
+ * f the candidate variable.
+ *
+ * This call constructs a set of enumerators for the relevant subfields of
+ * the grammar of f and adds them to enums. These enumerators are those that
+ * should be later given to calls to notifyEnumeration below.
+ *
+ * This also may result in lemmas being added to lemmas,
+ * which correspond to static symmetry breaking predicates (for example,
+ * those that exclude ITE from enumerators whose role is enum_io when the
+ * strategy is ITE_strat).
+ */
+ void initialize(Node f, std::vector<Node>& enums, std::vector<Node>& lemmas);
+ /** reset examples
+ *
+ * Reset the specification for f.
+ *
+ * Notice that this does not reset the
+ */
+ void resetExamples();
+ /** add example
+ *
+ * This adds input -> output to the specification for f. The arity of
+ * input should be equal to the number of arguments in the sygus variable
+ * list of the grammar of f. That is, if we are searching for solutions for f
+ * of the form (lambda v1...vn. t), then the arity of input should be n.
+ */
+ void addExample(const std::vector<Node>& input, Node output);
+
+ /**
+ * Notify that the value v has been enumerated for enumerator e. This call
+ * will add lemmas L to lemmas such that L entails e^M != v for all future
+ * models M.
+ */
+ void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas);
+ /** construct solution
+ *
+ * This attempts to construct a solution based on the current set of
+ * enumerated values. Returns null if it cannot (for example, if the
+ * set of enumerated values is insufficient, or if a non-deterministic
+ * strategy aborts).
+ */
+ Node constructSolution();
+
+ //-----------------------debug printing
+ /** print ind indentations on trace c */
+ static void indent(const char* c, int ind);
+ /** print (pol ? vals : !vals) as a bit-string on trace c */
+ static void print_val(const char* c,
+ std::vector<Node>& vals,
+ bool pol = true);
+ //-----------------------end debug printing
+ private:
+ /** reference to quantifier engine */
+ QuantifiersEngine* d_qe;
+ /** sygus term database of d_qe */
+ quantifiers::TermDbSygus* d_tds;
+ /** true and false nodes */
+ Node d_true;
+ Node d_false;
+ /** input of I/O examples */
+ std::map<Node, std::vector<std::vector<Node> > > d_examples;
+ /** output of I/O examples */
+ std::map<Node, std::vector<Node> > d_examples_out;
+
+ //------------------------------ 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.
+ */
+ class EnumInfo
+ {
+ 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(Node c, 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; }
+ /**
+ * The candidate variable that this enumerator is for (see sygus_pbe.h).
+ */
+ Node d_parent_candidate;
+ /** 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
+ /**
+ * 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);
+ /**
+ * 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);
+ /** Have we been notified that a complete solution exists? */
+ bool isSolved() { return !d_enum_solved.isNull(); }
+ /** Get the complete solution to the synthesis conjecture. */
+ Node getSolved() { return d_enum_solved; }
+ /** Values that have been enumerated for this enumerator */
+ std::vector<Node> d_enum_vals;
+ /**
+ * This either stores the values of f( I ) for inputs
+ * or the value of f( I ) = O if d_role==enum_io
+ */
+ std::vector<std::vector<Node> > d_enum_vals_res;
+ /**
+ * The set of values in d_enum_vals that have been "subsumed" by others
+ * (see SubsumeTrie for explanation of subsumed).
+ */
+ std::vector<Node> d_enum_subsume;
+ /** Map from values to their index in d_enum_vals. */
+ std::map<Node, unsigned> d_enum_val_to_index;
+ /**
+ * A subsumption trie containing the values in d_enum_vals. Depending on the
+ * role of this enumerator, values may either be added to d_term_trie with
+ * subsumption (if role=enum_io), or without (if role=enum_ite_condition or
+ * enum_concat_term).
+ */
+ SubsumeTrie d_term_trie;
+ //---------------------------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;
+
+ 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
+ */
+ 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();
+ };
+ /** the candidate for this class */
+ Node d_candidate;
+ /** maps a function-to-synthesize to the above information */
+ std::map<Node, CandidateInfo> d_cinfo;
+
+ //------------------------------ representation of an enumeration strategy
+ /** add enumerated value
+ *
+ * We have enumerated the value v for x. This function adds x->v to the
+ * relevant data structures that are used for strategy-specific construction
+ * of solutions when necessary, and returns a set of lemmas, which are added
+ * to the input argument lems. These lemmas are used to rule out models where
+ * x = v, to force that a new value is enumerated for x.
+ */
+ void addEnumeratedValue(Node x, Node v, std::vector<Node>& lems);
+ /** 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,
+ * 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,
+ 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
+ *
+ * Values v for x 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
+ * 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);
+ /** 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 c.
+ */
+ void collectEnumeratorTypes(Node c, 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.
+ *
+ * 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);
+ /** 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 c, and stores these into lemmas.
+ */
+ void staticLearnRedundantOps(Node c, 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 c,
+ 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
+
+ /** helper function for construct solution.
+ *
+ * Construct a solution based on enumerator e for function-to-synthesize c
+ * 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);
+ /** Heuristically choose the best solved term from solved in context x,
+ * currently return the first. */
+ Node constructBestSolvedTerm(std::vector<Node>& solved, UnifContext& x);
+ /** Heuristically choose the best solved string term from solved in context
+ * x, currently return the first. */
+ Node constructBestStringSolvedTerm(std::vector<Node>& solved, UnifContext& x);
+ /** Heuristically choose the best solved conditional term from solved in
+ * context x, currently random */
+ Node constructBestSolvedConditional(std::vector<Node>& solved,
+ UnifContext& x);
+ /** Heuristically choose the best conditional term from conds in context x,
+ * currently random */
+ Node constructBestConditional(std::vector<Node>& conds, UnifContext& x);
+ /** Heuristically choose the best string to concatenate from strs to the
+ * solution in context x, currently random
+ * incr stores the vector of indices that are incremented by this solution in
+ * example outputs.
+ * total_inc[x] is the sum of incr[x] for each x in strs.
+ */
+ Node constructBestStringToConcat(std::vector<Node> strs,
+ std::map<Node, unsigned> total_inc,
+ std::map<Node, std::vector<unsigned> > incr,
+ UnifContext& x);
+ //------------------------------ 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( c, d_cenum[1], ... ) = t1,
+ * ...,
+ * constructSolution( c, 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 */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
projects / cvc5.git / commitdiff