--- /dev/null
+/********************* */
+/*! \file sygus_unif_strat.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_strat
+ **/
+
+#include "theory/quantifiers/sygus/sygus_unif_strat.h"
+
+#include "theory/datatypes/datatypes_rewriter.h"
+#include "theory/quantifiers/sygus/sygus_unif.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_util.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;
+}
+
+void SygusUnifStrategy::initialize(QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& enums,
+ std::vector<Node>& lemmas)
+{
+ Assert(d_candidate.isNull());
+ d_candidate = f;
+ d_root = f.getType();
+ d_qe = qe;
+
+ // collect the enumerator types and form the strategy
+ collectEnumeratorTypes(d_root, role_equal);
+ // add the enumerators
+ enums.insert(enums.end(), d_esym_list.begin(), d_esym_list.end());
+ // learn redundant ops
+ staticLearnRedundantOps(lemmas);
+}
+
+void SygusUnifStrategy::initializeType(TypeNode tn)
+{
+ d_tinfo[tn].d_this_type = tn;
+}
+
+Node SygusUnifStrategy::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;
+}
+
+// ----------------------------- establishing enumeration types
+
+void SygusUnifStrategy::registerEnumerator(Node et,
+ TypeNode tn,
+ EnumRole enum_role,
+ bool inSearch)
+{
+ if (d_einfo.find(et) == d_einfo.end())
+ {
+ Trace("sygus-unif-debug")
+ << "...register " << et << " for "
+ << static_cast<DatatypeType>(tn.toType()).getDatatype().getName();
+ Trace("sygus-unif-debug") << ", role = " << enum_role
+ << ", in search = " << inSearch << std::endl;
+ d_einfo[et].initialize(enum_role);
+ // if we are actually enumerating this (could be a compound node in the
+ // strategy)
+ if (inSearch)
+ {
+ std::map<TypeNode, Node>::iterator itn = d_master_enum.find(tn);
+ if (itn == d_master_enum.end())
+ {
+ // use this for the search
+ d_master_enum[tn] = et;
+ 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 SygusUnifStrategy::collectEnumeratorTypes(TypeNode tn, NodeRole nrole)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ if (d_tinfo.find(tn) == d_tinfo.end())
+ {
+ // register type
+ Trace("sygus-unif") << "Register enumerating type : " << tn << std::endl;
+ initializeType(tn);
+ }
+ EnumTypeInfo& eti = d_tinfo[tn];
+ std::map<NodeRole, StrategyNode>::iterator itsn = eti.d_snodes.find(nrole);
+ if (itsn != eti.d_snodes.end())
+ {
+ // already initialized
+ return;
+ }
+ StrategyNode& snode = eti.d_snodes[nrole];
+
+ // get the enumerator for this
+ EnumRole erole = getEnumeratorRoleForNodeRole(nrole);
+
+ Node ee;
+ std::map<EnumRole, Node>::iterator iten = eti.d_enum.find(erole);
+ if (iten == eti.d_enum.end())
+ {
+ ee = nm->mkSkolem("ee", tn);
+ eti.d_enum[erole] = ee;
+ Trace("sygus-unif-debug")
+ << "...enumerator " << ee << " for "
+ << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
+ << ", role = " << erole << std::endl;
+ }
+ else
+ {
+ ee = iten->second;
+ }
+
+ // roles that we do not recurse on
+ if (nrole == role_ite_condition)
+ {
+ Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl;
+ registerEnumerator(ee, tn, erole, true);
+ return;
+ }
+
+ // look at information on how we will construct solutions for this type
+ Assert(tn.isDatatype());
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ Assert(dt.isSygus());
+
+ std::map<Node, std::vector<StrategyType> > cop_to_strat;
+ std::map<Node, unsigned> cop_to_cindex;
+ std::map<Node, std::map<unsigned, Node> > cop_to_child_templ;
+ std::map<Node, std::map<unsigned, Node> > cop_to_child_templ_arg;
+ std::map<Node, std::vector<unsigned> > cop_to_carg_list;
+ std::map<Node, std::vector<TypeNode> > cop_to_child_types;
+ std::map<Node, std::vector<Node> > cop_to_sks;
+
+ // whether we will enumerate the current type
+ bool search_this = false;
+ for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
+ {
+ Node cop = Node::fromExpr(dt[j].getConstructor());
+ Node op = Node::fromExpr(dt[j].getSygusOp());
+ Trace("sygus-unif-debug") << "--- Infer strategy from " << cop
+ << " with sygus op " << op << "..." << std::endl;
+
+ // expand the evaluation to see if this constuctor induces a strategy
+ std::vector<Node> utchildren;
+ utchildren.push_back(cop);
+ std::vector<Node> sks;
+ std::vector<TypeNode> sktns;
+ for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
+ {
+ Type t = dt[j][k].getRangeType();
+ TypeNode ttn = TypeNode::fromType(t);
+ Node kv = nm->mkSkolem("ut", ttn);
+ sks.push_back(kv);
+ cop_to_sks[cop].push_back(kv);
+ sktns.push_back(ttn);
+ utchildren.push_back(kv);
+ }
+ Node ut = nm->mkNode(APPLY_CONSTRUCTOR, utchildren);
+ std::vector<Node> echildren;
+ echildren.push_back(Node::fromExpr(dt.getSygusEvaluationFunc()));
+ echildren.push_back(ut);
+ Node sbvl = Node::fromExpr(dt.getSygusVarList());
+ for (const Node& sbv : sbvl)
+ {
+ echildren.push_back(sbv);
+ }
+ Node eut = nm->mkNode(APPLY_UF, echildren);
+ Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..."
+ << std::endl;
+ eut = d_qe->getTermDatabaseSygus()->unfold(eut);
+ Trace("sygus-unif-debug2") << " ...got " << eut;
+ Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl;
+
+ // candidate strategy
+ if (eut.getKind() == ITE)
+ {
+ cop_to_strat[cop].push_back(strat_ITE);
+ }
+ else if (eut.getKind() == STRING_CONCAT)
+ {
+ if (nrole != role_string_suffix)
+ {
+ cop_to_strat[cop].push_back(strat_CONCAT_PREFIX);
+ }
+ if (nrole != role_string_prefix)
+ {
+ cop_to_strat[cop].push_back(strat_CONCAT_SUFFIX);
+ }
+ }
+ else if (dt[j].isSygusIdFunc())
+ {
+ cop_to_strat[cop].push_back(strat_ID);
+ }
+
+ // the kinds for which there is a strategy
+ if (cop_to_strat.find(cop) != cop_to_strat.end())
+ {
+ // infer an injection from the arguments of the datatype
+ std::map<unsigned, unsigned> templ_injection;
+ std::vector<Node> vs;
+ std::vector<Node> ss;
+ std::map<Node, unsigned> templ_var_index;
+ for (unsigned k = 0, sksize = sks.size(); k < sksize; k++)
+ {
+ Assert(sks[k].getType().isDatatype());
+ const Datatype& cdt =
+ static_cast<DatatypeType>(sks[k].getType().toType()).getDatatype();
+ echildren[0] = Node::fromExpr(cdt.getSygusEvaluationFunc());
+ echildren[1] = sks[k];
+ Trace("sygus-unif-debug2") << "...set eval dt to " << sks[k]
+ << std::endl;
+ Node esk = nm->mkNode(APPLY_UF, echildren);
+ vs.push_back(esk);
+ Node tvar = nm->mkSkolem("templ", esk.getType());
+ templ_var_index[tvar] = k;
+ Trace("sygus-unif-debug2") << "* template inference : looking for "
+ << tvar << " for arg " << k << std::endl;
+ ss.push_back(tvar);
+ Trace("sygus-unif-debug2") << "* substitute : " << esk << " -> " << tvar
+ << std::endl;
+ }
+ eut = eut.substitute(vs.begin(), vs.end(), ss.begin(), ss.end());
+ Trace("sygus-unif-debug2") << "Constructor " << j << ", base term is "
+ << eut << std::endl;
+ std::map<unsigned, Node> test_args;
+ if (dt[j].isSygusIdFunc())
+ {
+ test_args[0] = eut;
+ }
+ else
+ {
+ for (unsigned k = 0, size = eut.getNumChildren(); k < size; k++)
+ {
+ test_args[k] = eut[k];
+ }
+ }
+
+ // TODO : prefix grouping prefix/suffix
+ bool isAssoc = TermUtil::isAssoc(eut.getKind());
+ Trace("sygus-unif-debug2") << eut.getKind() << " isAssoc = " << isAssoc
+ << std::endl;
+ std::map<unsigned, std::vector<unsigned> > assoc_combine;
+ std::vector<unsigned> assoc_waiting;
+ int assoc_last_valid_index = -1;
+ for (std::pair<const unsigned, Node>& ta : test_args)
+ {
+ unsigned k = ta.first;
+ Node eut_c = ta.second;
+ // success if we can find a injection from args to sygus args
+ if (!inferTemplate(k, eut_c, templ_var_index, templ_injection))
+ {
+ Trace("sygus-unif-debug")
+ << "...fail: could not find injection (range)." << std::endl;
+ cop_to_strat.erase(cop);
+ break;
+ }
+ std::map<unsigned, unsigned>::iterator itti = templ_injection.find(k);
+ if (itti != templ_injection.end())
+ {
+ // if associative, combine arguments if it is the same variable
+ if (isAssoc && assoc_last_valid_index >= 0
+ && itti->second == templ_injection[assoc_last_valid_index])
+ {
+ templ_injection.erase(k);
+ assoc_combine[assoc_last_valid_index].push_back(k);
+ }
+ else
+ {
+ assoc_last_valid_index = (int)k;
+ if (!assoc_waiting.empty())
+ {
+ assoc_combine[k].insert(assoc_combine[k].end(),
+ assoc_waiting.begin(),
+ assoc_waiting.end());
+ assoc_waiting.clear();
+ }
+ assoc_combine[k].push_back(k);
+ }
+ }
+ else
+ {
+ // a ground argument
+ if (!isAssoc)
+ {
+ Trace("sygus-unif-debug")
+ << "...fail: could not find injection (functional)."
+ << std::endl;
+ cop_to_strat.erase(cop);
+ break;
+ }
+ else
+ {
+ if (assoc_last_valid_index >= 0)
+ {
+ assoc_combine[assoc_last_valid_index].push_back(k);
+ }
+ else
+ {
+ assoc_waiting.push_back(k);
+ }
+ }
+ }
+ }
+ if (cop_to_strat.find(cop) != cop_to_strat.end())
+ {
+ // construct the templates
+ if (!assoc_waiting.empty())
+ {
+ // could not find a way to fit some arguments into injection
+ cop_to_strat.erase(cop);
+ }
+ else
+ {
+ for (std::pair<const unsigned, Node>& ta : test_args)
+ {
+ unsigned k = ta.first;
+ Trace("sygus-unif-debug2") << "- processing argument " << k << "..."
+ << std::endl;
+ if (templ_injection.find(k) != templ_injection.end())
+ {
+ unsigned sk_index = templ_injection[k];
+ if (std::find(cop_to_carg_list[cop].begin(),
+ cop_to_carg_list[cop].end(),
+ sk_index)
+ == cop_to_carg_list[cop].end())
+ {
+ cop_to_carg_list[cop].push_back(sk_index);
+ }
+ else
+ {
+ Trace("sygus-unif-debug") << "...fail: duplicate argument used"
+ << std::endl;
+ cop_to_strat.erase(cop);
+ break;
+ }
+ // also store the template information, if necessary
+ Node teut;
+ if (isAssoc)
+ {
+ std::vector<unsigned>& ac = assoc_combine[k];
+ Assert(!ac.empty());
+ std::vector<Node> children;
+ for (unsigned ack = 0, size_ac = ac.size(); ack < size_ac;
+ ack++)
+ {
+ children.push_back(eut[ac[ack]]);
+ }
+ teut = children.size() == 1
+ ? children[0]
+ : nm->mkNode(eut.getKind(), children);
+ teut = Rewriter::rewrite(teut);
+ }
+ else
+ {
+ teut = ta.second;
+ }
+
+ if (!teut.isVar())
+ {
+ cop_to_child_templ[cop][k] = teut;
+ cop_to_child_templ_arg[cop][k] = ss[sk_index];
+ Trace("sygus-unif-debug")
+ << " Arg " << k << " (template : " << teut << " arg "
+ << ss[sk_index] << "), index " << sk_index << std::endl;
+ }
+ else
+ {
+ Trace("sygus-unif-debug") << " Arg " << k << ", index "
+ << sk_index << std::endl;
+ Assert(teut == ss[sk_index]);
+ }
+ }
+ else
+ {
+ Assert(isAssoc);
+ }
+ }
+ }
+ }
+ }
+ if (cop_to_strat.find(cop) == cop_to_strat.end())
+ {
+ Trace("sygus-unif") << "...constructor " << cop
+ << " does not correspond to a strategy." << std::endl;
+ search_this = true;
+ }
+ else
+ {
+ Trace("sygus-unif") << "-> constructor " << cop
+ << " matches strategy for " << eut.getKind() << "..."
+ << std::endl;
+ // collect children types
+ for (unsigned k = 0, size = cop_to_carg_list[cop].size(); k < size; k++)
+ {
+ TypeNode tn = sktns[cop_to_carg_list[cop][k]];
+ Trace("sygus-unif-debug")
+ << " Child type " << k << " : "
+ << static_cast<DatatypeType>(tn.toType()).getDatatype().getName()
+ << std::endl;
+ cop_to_child_types[cop].push_back(tn);
+ }
+ }
+ }
+
+ // check whether we should also enumerate the current type
+ Trace("sygus-unif-debug2") << " register this enumerator..." << std::endl;
+ registerEnumerator(ee, tn, erole, search_this);
+
+ if (cop_to_strat.empty())
+ {
+ Trace("sygus-unif") << "...consider " << dt.getName() << " a basic type"
+ << std::endl;
+ }
+ else
+ {
+ for (std::pair<const Node, std::vector<StrategyType> >& cstr : cop_to_strat)
+ {
+ Node cop = cstr.first;
+ Trace("sygus-unif-debug") << "Constructor " << cop << " has "
+ << cstr.second.size() << " strategies..."
+ << std::endl;
+ for (unsigned s = 0, ssize = cstr.second.size(); s < ssize; s++)
+ {
+ EnumTypeInfoStrat* cons_strat = new EnumTypeInfoStrat;
+ StrategyType strat = cstr.second[s];
+
+ cons_strat->d_this = strat;
+ cons_strat->d_cons = cop;
+ Trace("sygus-unif-debug") << "Process strategy #" << s
+ << " for operator : " << cop << " : " << strat
+ << std::endl;
+ Assert(cop_to_child_types.find(cop) != cop_to_child_types.end());
+ std::vector<TypeNode>& childTypes = cop_to_child_types[cop];
+ Assert(cop_to_carg_list.find(cop) != cop_to_carg_list.end());
+ std::vector<unsigned>& cargList = cop_to_carg_list[cop];
+
+ std::vector<Node> sol_templ_children;
+ sol_templ_children.resize(cop_to_sks[cop].size());
+
+ for (unsigned j = 0, csize = childTypes.size(); j < csize; j++)
+ {
+ // calculate if we should allocate a new enumerator : should be true
+ // if we have a new role
+ NodeRole nrole_c = nrole;
+ if (strat == strat_ITE)
+ {
+ if (j == 0)
+ {
+ nrole_c = role_ite_condition;
+ }
+ }
+ else if (strat == strat_CONCAT_PREFIX)
+ {
+ if ((j + 1) < childTypes.size())
+ {
+ nrole_c = role_string_prefix;
+ }
+ }
+ else if (strat == strat_CONCAT_SUFFIX)
+ {
+ if (j > 0)
+ {
+ nrole_c = role_string_suffix;
+ }
+ }
+ // in all other cases, role is same as parent
+
+ // register the child type
+ TypeNode ct = childTypes[j];
+ Node csk = cop_to_sks[cop][cargList[j]];
+ cons_strat->d_sol_templ_args.push_back(csk);
+ sol_templ_children[cargList[j]] = csk;
+
+ EnumRole erole_c = getEnumeratorRoleForNodeRole(nrole_c);
+ // make the enumerator
+ Node et;
+ if (cop_to_child_templ[cop].find(j) != cop_to_child_templ[cop].end())
+ {
+ // it is templated, allocate a fresh variable
+ et = nm->mkSkolem("et", ct);
+ Trace("sygus-unif-debug")
+ << "...enumerate " << et << " of type "
+ << ((DatatypeType)ct.toType()).getDatatype().getName();
+ Trace("sygus-unif-debug") << " for arg " << j << " of "
+ << static_cast<DatatypeType>(tn.toType())
+ .getDatatype()
+ .getName()
+ << std::endl;
+ registerEnumerator(et, ct, erole_c, true);
+ d_einfo[et].d_template = cop_to_child_templ[cop][j];
+ d_einfo[et].d_template_arg = cop_to_child_templ_arg[cop][j];
+ Assert(!d_einfo[et].d_template.isNull());
+ Assert(!d_einfo[et].d_template_arg.isNull());
+ }
+ else
+ {
+ Trace("sygus-unif-debug")
+ << "...child type enumerate "
+ << ((DatatypeType)ct.toType()).getDatatype().getName()
+ << ", node role = " << nrole_c << std::endl;
+ collectEnumeratorTypes(ct, nrole_c);
+ // otherwise use the previous
+ Assert(d_tinfo[ct].d_enum.find(erole_c)
+ != d_tinfo[ct].d_enum.end());
+ et = 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 SygusUnifStrategy::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 SygusUnifStrategy::staticLearnRedundantOps(std::vector<Node>& lemmas)
+{
+ for (unsigned i = 0; i < d_esym_list.size(); i++)
+ {
+ Node e = d_esym_list[i];
+ std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e);
+ Assert(itn != d_einfo.end());
+ // see if there is anything we can eliminate
+ Trace("sygus-unif")
+ << "* Search enumerator #" << i << " : type "
+ << ((DatatypeType)e.getType().toType()).getDatatype().getName()
+ << " : ";
+ Trace("sygus-unif") << e << " has " << itn->second.d_enum_slave.size()
+ << " slaves:" << std::endl;
+ for (unsigned j = 0; j < itn->second.d_enum_slave.size(); j++)
+ {
+ Node es = itn->second.d_enum_slave[j];
+ std::map<Node, EnumInfo>::iterator itns = d_einfo.find(es);
+ Assert(itns != d_einfo.end());
+ Trace("sygus-unif") << " " << es << ", role = " << itns->second.getRole()
+ << std::endl;
+ }
+ }
+ Trace("sygus-unif") << std::endl;
+ Trace("sygus-unif") << "Strategy for candidate " << d_candidate
+ << " is : " << std::endl;
+ std::map<Node, std::map<NodeRole, bool> > visited;
+ std::map<Node, std::map<unsigned, bool> > needs_cons;
+ staticLearnRedundantOps(
+ 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 SygusUnifStrategy::staticLearnRedundantOps(
+ Node e,
+ NodeRole nrole,
+ std::map<Node, std::map<NodeRole, bool> >& visited,
+ std::map<Node, std::map<unsigned, bool> >& needs_cons,
+ int ind,
+ bool isCond)
+{
+ std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e);
+ Assert(itn != d_einfo.end());
+
+ if (visited[e].find(nrole) == visited[e].end()
+ || (isCond && !itn->second.isConditional()))
+ {
+ visited[e][nrole] = true;
+ // if conditional
+ if (isCond)
+ {
+ itn->second.setConditional();
+ }
+ indent("sygus-unif", ind);
+ Trace("sygus-unif") << e << " :: node role : " << nrole;
+ Trace("sygus-unif")
+ << ", type : "
+ << ((DatatypeType)e.getType().toType()).getDatatype().getName();
+ if (isCond)
+ {
+ Trace("sygus-unif") << ", conditional";
+ }
+ Trace("sygus-unif") << ", enum role : " << itn->second.getRole();
+
+ if (itn->second.isTemplated())
+ {
+ Trace("sygus-unif") << ", templated : (lambda "
+ << itn->second.d_template_arg << " "
+ << itn->second.d_template << ")" << std::endl;
+ }
+ else
+ {
+ Trace("sygus-unif") << std::endl;
+ TypeNode etn = e.getType();
+
+ // enumerator type info
+ std::map<TypeNode, EnumTypeInfo>::iterator itt = d_tinfo.find(etn);
+ Assert(itt != d_tinfo.end());
+ EnumTypeInfo& tinfo = itt->second;
+
+ // strategy info
+ std::map<NodeRole, StrategyNode>::iterator itsn =
+ tinfo.d_snodes.find(nrole);
+ Assert(itsn != tinfo.d_snodes.end());
+ StrategyNode& snode = itsn->second;
+
+ if (snode.d_strats.empty())
+ {
+ return;
+ }
+ std::map<unsigned, bool> needs_cons_curr;
+ // various strategies
+ for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
+ {
+ EnumTypeInfoStrat* etis = snode.d_strats[j];
+ StrategyType strat = etis->d_this;
+ bool newIsCond = isCond || strat == strat_ITE;
+ indent("sygus-unif", ind + 1);
+ Trace("sygus-unif") << "Strategy : " << strat
+ << ", from cons : " << etis->d_cons << std::endl;
+ int cindex = Datatype::indexOf(etis->d_cons.toExpr());
+ Assert(cindex != -1);
+ needs_cons_curr[static_cast<unsigned>(cindex)] = false;
+ for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
+ {
+ // recurse
+ staticLearnRedundantOps(
+ cec.first, cec.second, visited, needs_cons, ind + 2, newIsCond);
+ }
+ }
+ // get the master enumerator for the type of this enumerator
+ std::map<TypeNode, Node>::iterator itse = d_master_enum.find(etn);
+ if (itse == d_master_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;
+ }
+}
+
+void EnumInfo::initialize(EnumRole role) { d_role = role; }
+bool EnumTypeInfoStrat::isValid(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;
+}
+
+StrategyNode::~StrategyNode()
+{
+ for (unsigned j = 0, size = d_strats.size(); j < size; j++)
+ {
+ delete d_strats[j];
+ }
+ d_strats.clear();
+}
+
+void SygusUnifStrategy::indent(const char* c, int ind)
+{
+ if (Trace.isOn(c))
+ {
+ for (int i = 0; i < ind; i++)
+ {
+ Trace(c) << " ";
+ }
+ }
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file sygus_unif_strat.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_strat
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_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 UnifContext;
+
+/**
+* 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.
+*
+* 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. When
+* constructing a sygus unifciation strategy, 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
+ *
+ * role is the "role" the enumerator plays in the high-level strategy,
+ * which is one of enum_* above.
+ */
+ void initialize(EnumRole role);
+ /** is this enumerator associated with a template? */
+ bool isTemplated() { return !d_template.isNull(); }
+ /** set conditional
+ *
+ * This flag is set to true if this enumerator may not apply to all
+ * input/output examples. For example, if this enumerator is used
+ * as an output value beneath a conditional in an instance of strat_ITE,
+ * then this enumerator is conditional.
+ */
+ void setConditional() { d_is_conditional = true; }
+ /** returns if this enumerator is conditional */
+ bool isConditional() { return d_is_conditional; }
+ /** get the role of this enumerator */
+ EnumRole getRole() { return d_role; }
+ /** enumerator template
+ *
+ * If d_template non-null, enumerated values V are immediately transformed to
+ * d_template { d_template_arg -> V }.
+ */
+ Node d_template;
+ Node d_template_arg;
+ /**
+ * Slave enumerators of this enumerator. These are other enumerators that
+ * have the same type, but a different role in the strategy tree. We
+ * generally
+ * only use one enumerator per type, and hence these slaves are notified when
+ * values are enumerated for this enumerator.
+ */
+ std::vector<Node> d_enum_slave;
+
+ 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;
+};
+
+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 all enumerators and strategies for a SyGuS datatype type.
+ */
+class EnumTypeInfo
+{
+ public:
+ EnumTypeInfo() {}
+ /** 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;
+};
+
+/** represents a strategy for a SyGuS datatype type
+ *
+ * This represents a possible strategy to apply when processing a strategy
+ * node in constructSolution. When applying the strategy represented by this
+ * class, we may make recursive calls to the children of the strategy,
+ * given in d_cenum. If all recursive calls to constructSolution for these
+ * children are successful, say:
+ * constructSolution( d_cenum[1], ... ) = t1,
+ * ...,
+ * constructSolution( d_cenum[n], ... ) = tn,
+ * Then, the solution returned by this strategy is
+ * d_sol_templ * { d_sol_templ_args -> (t1,...,tn) }
+ * where * is application of substitution.
+ */
+class EnumTypeInfoStrat
+{
+ public:
+ /** the type of strategy this represents */
+ StrategyType d_this;
+ /** the sygus datatype constructor that induced this strategy
+ *
+ * For example, this may be a sygus datatype whose sygus operator is ITE,
+ * if the strategy type above is strat_ITE.
+ */
+ Node d_cons;
+ /** children of this strategy */
+ std::vector<std::pair<Node, NodeRole> > d_cenum;
+ /** the arguments for the (templated) solution */
+ std::vector<Node> d_sol_templ_args;
+ /** the template for the solution */
+ Node d_sol_templ;
+ /** Returns true if argument is valid strategy in unification context x */
+ bool isValid(UnifContext* x);
+};
+
+/**
+ * Stores strategy and enumeration information for a function-to-synthesize.
+ *
+ * When this class is initialized, we construct a "strategy tree" based on
+ * the grammar of the function to synthesize f. This tree is represented by
+ * the above classes.
+ */
+class SygusUnifStrategy
+{
+ public:
+ SygusUnifStrategy() {}
+ /** 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.
+ *
+ * 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(QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& enums,
+ std::vector<Node>& lemmas);
+ /** Get the root enumerator for this class */
+ Node getRootEnumerator();
+ /** maps enumerators to relevant information */
+ std::map<Node, EnumInfo> d_einfo;
+ /** list of all enumerators for the function-to-synthesize */
+ std::vector<Node> d_esym_list;
+ /** Info for sygus datatype type occurring in a field of d_root */
+ std::map<TypeNode, EnumTypeInfo> d_tinfo;
+
+ private:
+ /** reference to quantifier engine */
+ QuantifiersEngine* d_qe;
+ /** The candidate variable this strategy is for */
+ Node d_candidate;
+ /**
+ * The root sygus datatype for the function-to-synthesize,
+ * which encodes the overall syntactic restrictions on the space
+ * of solutions.
+ */
+ TypeNode d_root;
+ /**
+ * Maps sygus datatypes to their master enumerator. This is the (single)
+ * enumerator of that type that we enumerate values for.
+ */
+ std::map<TypeNode, Node> d_master_enum;
+ /** Initialize necessary information for (sygus) type tn */
+ void initializeType(TypeNode tn);
+
+ //-----------------------debug printing
+ /** print ind indentations on trace c */
+ static void indent(const char* c, int ind);
+ //-----------------------end debug printing
+
+ //------------------------------ strategy registration
+ /** collect enumerator types
+ *
+ * This builds the strategy for enumerated values of type tn for the given
+ * role of nrole, for solutions to function-to-synthesize of this class.
+ */
+ void collectEnumeratorTypes(TypeNode tn, NodeRole nrole);
+ /** register enumerator
+ *
+ * This registers that et is an enumerator of type tn, having enumerator
+ * role enum_role.
+ *
+ * inSearch is whether we will enumerate values based on this enumerator.
+ * A strategy node is represented by a (enumerator, node role) pair. Hence,
+ * we may use enumerators for which this flag is false to represent strategy
+ * nodes that have child strategies.
+ */
+ void registerEnumerator(Node et,
+ TypeNode tn,
+ EnumRole enum_role,
+ bool inSearch);
+ /** infer template */
+ bool inferTemplate(unsigned k,
+ Node n,
+ std::map<Node, unsigned>& templ_var_index,
+ std::map<unsigned, unsigned>& templ_injection);
+ /** static learn redundant operators
+ *
+ * This learns static lemmas for pruning enumerative space based on the
+ * strategy for the function-to-synthesize of this class, and stores these
+ * into lemmas.
+ */
+ void staticLearnRedundantOps(std::vector<Node>& lemmas);
+ /** helper for static learn redundant operators
+ *
+ * (e, nrole) specify the strategy node in the graph we are currently
+ * analyzing, visited stores the nodes we have already visited.
+ *
+ * This method builds the mapping needs_cons, which maps (master) enumerators
+ * to a map from the constructors that it needs.
+ *
+ * ind is the depth in the strategy graph we are at (for debugging).
+ *
+ * isCond is whether the current enumerator is conditional (beneath a
+ * conditional of an strat_ITE strategy).
+ */
+ void staticLearnRedundantOps(
+ Node e,
+ NodeRole nrole,
+ std::map<Node, std::map<NodeRole, bool> >& visited,
+ std::map<Node, std::map<unsigned, bool> >& needs_cons,
+ int ind,
+ bool isCond);
+ //------------------------------ end strategy registration
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
projects / cvc5.git / commitdiff