From: Andrew Reynolds Date: Fri, 30 Mar 2018 18:36:04 +0000 (-0500) Subject: Split strategy representation from SygusUnif (#1730) X-Git-Tag: cvc5-1.0.0~5195 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a5ca16724eca73b5b0c679b2ee6bca4f3c23f870;p=cvc5.git Split strategy representation from SygusUnif (#1730) --- diff --git a/src/Makefile.am b/src/Makefile.am index 9b1b71efc..6693deaa5 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -474,6 +474,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/sygus/sygus_process_conj.h \ theory/quantifiers/sygus/sygus_unif.cpp \ theory/quantifiers/sygus/sygus_unif.h \ + theory/quantifiers/sygus/sygus_unif_strat.cpp \ + theory/quantifiers/sygus/sygus_unif_strat.h \ theory/quantifiers/sygus/term_database_sygus.cpp \ theory/quantifiers/sygus/term_database_sygus.h \ theory/quantifiers/sygus_sampler.cpp \ diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 4af63f12b..00658b6c4 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -26,58 +26,6 @@ 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(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(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(st); break; - } - return os; -} - UnifContext::UnifContext() : d_has_string_pos(role_invalid) { d_true = NodeManager::currentNM()->mkConst(true); diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 518a730a5..9bb321a09 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -19,76 +19,13 @@ #include #include "expr/node.h" +#include "theory/quantifiers/sygus/sygus_unif_strat.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 @@ -394,14 +331,6 @@ class SygusUnif */ 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& vals, - bool pol = true); - //-----------------------end debug printing private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; @@ -415,6 +344,15 @@ class SygusUnif /** output of I/O examples */ std::vector d_examples_out; + //-----------------------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& vals, + bool pol = true); + //-----------------------end debug printing + //------------------------------ representation of a enumeration strategy /** * This class stores information regarding an enumerator, including: diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp new file mode 100644 index 000000000..c5899128d --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -0,0 +1,872 @@ +/********************* */ +/*! \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(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(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(st); break; + } + return os; +} + +void SygusUnifStrategy::initialize(QuantifiersEngine* qe, + Node f, + std::vector& enums, + std::vector& 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::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(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::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::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::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(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(tn.toType()).getDatatype(); + Assert(dt.isSygus()); + + std::map > cop_to_strat; + std::map cop_to_cindex; + std::map > cop_to_child_templ; + std::map > cop_to_child_templ_arg; + std::map > cop_to_carg_list; + std::map > cop_to_child_types; + std::map > 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 utchildren; + utchildren.push_back(cop); + std::vector sks; + std::vector 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 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 templ_injection; + std::vector vs; + std::vector ss; + std::map templ_var_index; + for (unsigned k = 0, sksize = sks.size(); k < sksize; k++) + { + Assert(sks[k].getType().isDatatype()); + const Datatype& cdt = + static_cast(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 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 > assoc_combine; + std::vector assoc_waiting; + int assoc_last_valid_index = -1; + for (std::pair& 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::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& 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& ac = assoc_combine[k]; + Assert(!ac.empty()); + std::vector 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(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 >& 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& childTypes = cop_to_child_types[cop]; + Assert(cop_to_carg_list.find(cop) != cop_to_carg_list.end()); + std::vector& cargList = cop_to_carg_list[cop]; + + std::vector 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(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(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(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& templ_var_index, + std::map& templ_injection) +{ + if (n.getNumChildren() == 0) + { + std::map::iterator itt = templ_var_index.find(n); + if (itt != templ_var_index.end()) + { + unsigned kk = itt->second; + std::map::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& lemmas) +{ + for (unsigned i = 0; i < d_esym_list.size(); i++) + { + Node e = d_esym_list[i]; + std::map::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::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 > visited; + std::map > needs_cons; + staticLearnRedundantOps( + getRootEnumerator(), role_equal, visited, needs_cons, 0, false); + // now, check the needs_cons map + for (std::pair >& nce : needs_cons) + { + Node em = nce.first; + const Datatype& dt = + static_cast(em.getType().toType()).getDatatype(); + for (std::pair& 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 >& visited, + std::map >& needs_cons, + int ind, + bool isCond) +{ + std::map::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::iterator itt = d_tinfo.find(etn); + Assert(itt != d_tinfo.end()); + EnumTypeInfo& tinfo = itt->second; + + // strategy info + std::map::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 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(cindex)] = false; + for (std::pair& 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::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(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 */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h new file mode 100644 index 000000000..94eadbc68 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -0,0 +1,344 @@ +/********************* */ +/*! \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 +#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 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 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 d_enum; + /** map from node roles to strategy nodes */ + std::map 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 > d_cenum; + /** the arguments for the (templated) solution */ + std::vector 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& enums, + std::vector& lemmas); + /** Get the root enumerator for this class */ + Node getRootEnumerator(); + /** maps enumerators to relevant information */ + std::map d_einfo; + /** list of all enumerators for the function-to-synthesize */ + std::vector d_esym_list; + /** Info for sygus datatype type occurring in a field of d_root */ + std::map 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 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& templ_var_index, + std::map& 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& 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 >& visited, + std::map >& 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 */