From 0baee856785df0f018fa2a007f62299c45fd8e5d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Mar 2018 16:54:05 -0500 Subject: [PATCH] Make sygus pbe use sygus unif utility (#1724) --- src/theory/quantifiers/sygus/sygus_pbe.cpp | 2139 +------------------ src/theory/quantifiers/sygus/sygus_pbe.h | 608 +----- src/theory/quantifiers/sygus/sygus_unif.cpp | 451 ++-- src/theory/quantifiers/sygus/sygus_unif.h | 22 +- 4 files changed, 317 insertions(+), 2903 deletions(-) diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 347efac26..65b8ba133 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -149,20 +149,35 @@ bool CegConjecturePbe::initialize(Node n, if( candidates.size()==1 ){// conditional solutions for multiple function conjectures TODO? // collect a pool of types over which we will enumerate terms Node c = candidates[0]; - //the candidate must be input/output examples - if( d_examples_out_invalid.find( c )==d_examples_out_invalid.end() ){ + // specification must have at least one example, and must be in PBE form + if (!d_examples[c].empty() + && d_examples_out_invalid.find(c) == d_examples_out_invalid.end()) + { Assert( d_examples.find( c )!=d_examples.end() ); - Trace("sygus-unif") << "It is input/output examples..." << std::endl; - TypeNode ctn = c.getType(); - d_cinfo[c].initialize( c ); - // collect the enumerator types / form the strategy - collectEnumeratorTypes(c, ctn, role_equal); - // if we have non-trivial strategies, then use pbe - if( d_cinfo[c].isNonTrivial() ){ - // static learning of redundant constructors - staticLearnRedundantOps( c, lemmas ); - d_is_pbe = true; + Trace("sygus-pbe") << "Initialize unif utility for " << c << "..." + << std::endl; + d_sygus_unif[c].initialize(d_qe, c, d_candidate_to_enum[c], lemmas); + Assert(!d_candidate_to_enum[c].empty()); + Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size() + << " enumerators for " << c << "..." << std::endl; + // initialize the enumerators + for (unsigned i = 0, size = d_candidate_to_enum[c].size(); i < size; + i++) + { + Node e = d_candidate_to_enum[c][i]; + d_tds->registerEnumerator(e, c, d_parent, true); + Node g = d_tds->getActiveGuardForEnumerator(e); + d_enum_to_active_guard[e] = g; + d_enum_to_candidate[e] = c; + } + Trace("sygus-pbe") << "Initialize " << d_examples[c].size() + << " example points for " << c << "..." << std::endl; + // initialize the examples + for (unsigned i = 0, nex = d_examples[c].size(); i < nex; i++) + { + d_sygus_unif[c].addExample(d_examples[c][i], d_examples_out[c][i]); } + d_is_pbe = true; } } } @@ -292,715 +307,6 @@ Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, return Rewriter::rewrite(bn); } -// ----------------------------- establishing enumeration types - -void CegConjecturePbe::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 " - << ((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::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); - // register measured term with database - d_qe->getTermDatabaseSygus()->registerEnumerator(et, c, d_parent, true); - d_einfo[et].d_active_guard = - d_qe->getTermDatabaseSygus()->getActiveGuardForEnumerator(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 CegConjecturePbe::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::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 " - << ((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(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, 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 >& 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 " - << ((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(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 " << ((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 CegConjecturePbe::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& lemmas ) { - for( unsigned i=0; i::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; jsecond.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 > visited; - std::map > needs_cons; - staticLearnRedundantOps(c, - d_cinfo[c].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 CegConjecturePbe::staticLearnRedundantOps( - Node c, - Node e, - NodeRole nrole, - std::map >& visited, - std::map >& 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(); - } - SygusUnif::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::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; - SygusUnif::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(c, - 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_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(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{ - SygusUnif::indent("sygus-unif", ind); - Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl; - } -} - // ------------------------------------------- solution construction from enumeration void CegConjecturePbe::getTermList(const std::vector& candidates, @@ -1009,13 +315,19 @@ void CegConjecturePbe::getTermList(const std::vector& candidates, Valuation& valuation = d_qe->getValuation(); for( unsigned i=0; i::iterator it = d_cinfo.find( v ); - if( it!=d_cinfo.end() ){ - for( unsigned j=0; jsecond.d_esym_list.size(); j++ ){ - Node e = it->second.d_esym_list[j]; - std::map< Node, EnumInfo >::iterator it = d_einfo.find( e ); - Assert( it != d_einfo.end() ); - Node gstatus = valuation.getSatValue(it->second.d_active_guard); + std::map >::iterator it = + d_candidate_to_enum.find(v); + if (it != d_candidate_to_enum.end()) + { + for (unsigned j = 0; j < it->second.size(); j++) + { + Node e = it->second[j]; + Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); + Node g = d_enum_to_active_guard[e]; + // Get whether the active guard for this enumerator is true, + // if so, then there may exist more values for it, and hence we add it + // to terms. + Node gstatus = valuation.getSatValue(g); if (!gstatus.isNull() && gstatus.getConst()) { terms.push_back(e); @@ -1049,15 +361,30 @@ bool CegConjecturePbe::constructCandidates(const std::vector& enums, } // only consider the enumerators that are at minimum size (for fairness) Trace("sygus-pbe-enum") << "...register " << enum_consider.size() << " / " << enums.size() << std::endl; - for( unsigned i=0; i enum_lems; + d_sygus_unif[c].notifyEnumeration(e, v, enum_lems); + // the lemmas must be guarded by the active guard of the enumerator + Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); + Node g = d_enum_to_active_guard[e]; + for (unsigned j = 0, size = enum_lems.size(); j < size; j++) + { + enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]); + } + lems.insert(lems.end(), enum_lems.begin(), enum_lems.end()); } } for( unsigned i=0; i& enums, return true; } -void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& lems ) { - std::map< Node, EnumInfo >::iterator it = d_einfo.find( x ); - Assert( it != d_einfo.end() ); - Node gstatus = d_qe->getValuation().getSatValue(it->second.d_active_guard); - if (gstatus.isNull() || !gstatus.getConst()) - { - Trace("sygus-pbe-enum-debug") << " ...guard is inactive." << std::endl; - return; - } - 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; - if (d_examples_out_invalid.find(c) == d_examples_out_invalid.end()) - { - std::map::iterator itc = d_cinfo.find(c); - Assert(itc != d_cinfo.end()); - TypeNode xtn = x.getType(); - Node bv = d_tds->sygusToBuiltin(v, xtn); - std::map > >::iterator itx = - d_examples.find(c); - std::map >::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 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 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; ssecond.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 ); - } - } - } - }else{ - Trace("sygus-pbe-enum-debug") - << " ...examples do not have output." << std::endl; - } - // exclude this value on subsequent iterations - Node g = it->second.d_active_guard; - 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); - } - Node exlem = - NodeManager::currentNM()->mkNode(OR, g.negate(), exp_exc.negate()); - Trace("sygus-pbe-enum-lemma") - << "CegConjecturePbe : enumeration exclude lemma : " << exlem - << std::endl; - lems.push_back(exlem); -} - -bool CegConjecturePbe::useStrContainsEnumeratorExclude(Node x, EnumInfo& ei) -{ - TypeNode xbt = d_tds->sygusToBuiltinType(x.getType()); - if (xbt.isString()) - { - std::map::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::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 CegConjecturePbe::getExplanationForEnumeratorExclude( - Node c, - Node x, - Node v, - std::vector& results, - EnumInfo& ei, - std::vector& 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 >::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 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; - } - } - if (!cmp_indices.empty()) - { - // we check invariance with respect to a negative contains test - NegContainsSygusInvarianceTest ncset; - ncset.init(x, d_examples[c], 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 CegConjecturePbe::EnumInfo::addEnumValue( CegConjecturePbe * 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 ); - /* - if( getRole()==enum_io ){ - // compute - if( d_enum_total.empty() ){ - d_enum_total = results; - }else if( !d_enum_total_true ){ - d_enum_total_true = true; - Assert( d_enum_total.size()==results.size() ); - for( unsigned i=0; id_true || results[i]==pbe->d_true ){ - d_enum_total[i] = pbe->d_true; - }else{ - d_enum_total[i] = pbe->d_false; - d_enum_total_true = false; - } - } - } - } - */ -} - -void CegConjecturePbe::EnumInfo::initialize(Node c, EnumRole role) -{ - d_parent_candidate = c; - d_role = role; -} - -void CegConjecturePbe::EnumInfo::setSolved( Node slv ) { - d_enum_solved = slv; - //d_enum_total_true = true; -} - -void CegConjecturePbe::CandidateInfo::initialize( Node c ) { - d_this_candidate = c; - d_root = c.getType(); -} - -void CegConjecturePbe::CandidateInfo::initializeType( TypeNode tn ) { - d_tinfo[tn].d_this_type = tn; - d_tinfo[tn].d_parent = this; -} - -Node CegConjecturePbe::CandidateInfo::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; -} - -bool CegConjecturePbe::CandidateInfo::isNonTrivial() { - //TODO - return true; -} - -// status : 0 : exact, -1 : vals is subset, 1 : vals is superset -Node CegConjecturePbe::SubsumeTrie::addTermInternal( - Node t, - const std::vector& vals, - bool pol, - std::vector& 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()); - // 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 check_subsumed_by; - if (status == 0) - { - if (!cv.getConst()) - { - check_subsumed_by.push_back(spol); - } - } - else if (status == -1) - { - check_subsumed_by.push_back(spol); - if (!cv.getConst()) - { - 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::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 check_subsume; - if (status == 0) - { - if (checkExistsOnly) - { - std::map::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()) - { - 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()) - { - 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(check_subsume[i]); - std::map::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 CegConjecturePbe::SubsumeTrie::addTerm(Node t, - const std::vector& vals, - bool pol, - std::vector& subsumed) -{ - return addTermInternal(t, vals, pol, subsumed, true, 0, 0, false, true); -} - -Node CegConjecturePbe::SubsumeTrie::addCond(Node c, - const std::vector& vals, - bool pol) -{ - std::vector subsumed; - return addTermInternal(c, vals, pol, subsumed, true, 0, 0, false, false); -} - -void CegConjecturePbe::SubsumeTrie::getSubsumed(const std::vector& vals, - bool pol, - std::vector& subsumed) -{ - addTermInternal(Node::null(), vals, pol, subsumed, true, 0, 1, true, true); -} - -void CegConjecturePbe::SubsumeTrie::getSubsumedBy( - const std::vector& vals, bool pol, std::vector& subsumed_by) -{ - // flip polarities - addTermInternal( - Node::null(), vals, !pol, subsumed_by, false, 0, 1, true, true); -} - -void CegConjecturePbe::SubsumeTrie::getLeavesInternal( - const std::vector& vals, - bool pol, - std::map >& 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() == pol; - for (std::map::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() ? 1 : -1); - if (status != -2 && new_status != status) - { - new_status = 0; - } - } - } - it->second.getLeavesInternal(vals, pol, v, index + 1, new_status); - } - } -} - -void CegConjecturePbe::SubsumeTrie::getLeaves( - const std::vector& vals, - bool pol, - std::map >& v) -{ - getLeavesInternal(vals, pol, v, 0, -2); -} - -Node CegConjecturePbe::constructSolution( Node c ){ - 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 )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(); - } -} - -Node CegConjecturePbe::constructBestSolvedTerm( std::vector< Node >& solved, UnifContext& x ){ - Assert( !solved.empty() ); - // TODO - return solved[0]; -} - -Node CegConjecturePbe::constructBestStringSolvedTerm( std::vector< Node >& solved, UnifContext& x ) { - Assert( !solved.empty() ); - // TODO - return solved[0]; -} - -Node CegConjecturePbe::constructBestSolvedConditional( std::vector< Node >& solved, UnifContext& x ){ - Assert( !solved.empty() ); - // TODO - return solved[0]; -} - -Node CegConjecturePbe::constructBestConditional( std::vector< Node >& conds, UnifContext& x ) { - Assert( !conds.empty() ); - // TODO - 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 CegConjecturePbe::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 CegConjecturePbe::constructSolution( - Node c, Node e, NodeRole nrole, UnifContext& x, int ind) -{ - TypeNode etn = e.getType(); - if (Trace.isOn("sygus-pbe-dt-debug")) - { - SygusUnif::indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") << "ConstructPBE: (" << e << ", " << nrole - << ") for type " << etn << " in context "; - SygusUnif::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::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(); - SygusUnif::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 subsumed_by; - einfo.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by); - if (!subsumed_by.empty()) - { - ret_dt = constructBestSolvedTerm(subsumed_by, x); - SygusUnif::indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "return PBE: success : conditionally solved" - << d_tds->sygusToBuiltin(ret_dt) << std::endl; - } - else - { - SygusUnif::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::iterator itet; - std::map::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 >::iterator itx = - d_examples_out.find(c); - Assert(itx != d_examples_out.end()); - std::vector 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 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); - SygusUnif::indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "return PBE: success : string solved " - << d_tds->sygusToBuiltin(ret_dt) << std::endl; - } - else - { - SygusUnif::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 > incr; - bool isPrefix = nrole == role_string_prefix; - std::map total_inc; - std::vector inc_strs; - std::map >::iterator itx = d_examples_out.find(c); - Assert(itx != d_examples_out.end()); - // make the value of the examples - std::vector ex_vals; - x.getCurrentStrings(this, itx->second, ex_vals); - if (Trace.isOn("sygus-pbe-dt-debug")) - { - SygusUnif::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++) - { - SygusUnif::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]; - SygusUnif::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()); - SygusUnif::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{ - SygusUnif::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 - { - SygusUnif::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::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; - SygusUnif::indent("sygus-pbe-dt", ind + 1); - Trace("sygus-pbe-dt") << "...try STRATEGY " << strat << "..." - << std::endl; - - std::map look_ahead_solved_children; - std::vector 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++) - { - SygusUnif::indent("sygus-pbe-dt", ind + 1); - Trace("sygus-pbe-dt") << "construct PBE child #" << sc << "..." - << std::endl; - Node rec_c; - std::map::iterator itla = - look_ahead_solved_children.find(sc); - if (itla != look_ahead_solved_children.end()) - { - rec_c = itla->second; - SygusUnif::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& cenum = etis->d_cenum[sc]; - - // update the context - std::vector prev; - if (strat == strat_ITE && sc > 0) - { - std::map::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::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& te_pair = etis->d_cenum[i]; - Node te = te_pair.first; - std::map::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 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 > possible_cond; - std::map solved_cond; // stores branch - einfo_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond); - - std::map >::iterator itpc = - possible_cond.find(0); - if (itpc != possible_cond.end()) - { - if (Trace.isOn("sygus-pbe-dt-debug")) - { - SygusUnif::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) - { - SygusUnif::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 > 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 >::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); - SygusUnif::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 >::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& 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()); - SygusUnif::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? - SygusUnif::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()); - SygusUnif::indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") - << "PBE: success : constructed for strategy " << strat << std::endl; - }else{ - SygusUnif::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() ); - } - SygusUnif::indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "ConstructPBE: returned " << ret_dt << std::endl; - return ret_dt; -} - -bool CegConjecturePbe::EnumTypeInfoStrat::isValid(CegConjecturePbe* 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; -} - -CegConjecturePbe::UnifContext::UnifContext() : d_has_string_pos(role_invalid) -{ - d_true = NodeManager::currentNM()->mkConst(true); - d_false = NodeManager::currentNM()->mkConst(false); -} - -bool CegConjecturePbe::UnifContext::updateContext( CegConjecturePbe * 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& pos ) { - Assert( pos.size()==d_str_pos.size() ); - bool changed = false; - for( unsigned i=0; i0 ){ - d_str_pos[i] += pos[i]; - changed = true; - } - } - if (changed) - { - d_visit_role.clear(); - } - return changed; -} - -bool CegConjecturePbe::UnifContext::isReturnValueModified() { - if (d_has_string_pos != role_invalid) - { - return true; - } - return false; -} - -void CegConjecturePbe::UnifContext::initialize( CegConjecturePbe * 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; id_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& vals, - std::vector& ex_vals) -{ - bool isPrefix = d_has_string_pos == role_string_prefix; - String dummy; - for( unsigned i=0; id_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(); - 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() ); - } - }else{ - // irrelevant, add dummy - ex_vals.push_back( dummy ); - } - } -} - -bool CegConjecturePbe::UnifContext::getStringIncrement( - CegConjecturePbe* pbe, - bool isPrefix, - const std::vector& ex_vals, - const std::vector& vals, - std::vector& inc, - unsigned& tot) -{ - for( unsigned j=0; jd_true ){ - // example is active in this context - Assert( vals[j].isConst() ); - String mystr = vals[j].getConst(); - 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 CegConjecturePbe::UnifContext::isStringSolved( - CegConjecturePbe* pbe, - const std::vector& ex_vals, - const std::vector& vals) -{ - for( unsigned j=0; jd_true ){ - // example is active in this context - Assert( vals[j].isConst() ); - String mystr = vals[j].getConst(); - if( ex_vals[j]!=mystr ){ - return false; - } - } - } - return true; -} - -CegConjecturePbe::StrategyNode::~StrategyNode() -{ - for (unsigned j = 0, size = d_strats.size(); j < size; j++) - { - delete d_strats[j]; - } - d_strats.clear(); -} } } } diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index dd98dd0aa..fb353a102 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -47,10 +47,10 @@ class CegConjecture; * via Divide and Conquer" TACAS 2017. In particular, it may consider * strategies for constructing decision trees when the grammar permits ITEs * and a strategy for divide-and-conquer string synthesis when the grammar -* permits string concatenation. This is stored in a set of data structures -* within d_cinfo. +* permits string concatenation. This is managed through the SygusUnif +* utilities, d_sygus_unif. * (3) It makes (possibly multiple) calls to -* TermDatabaseSygus::registerMeasuredTerm(...) based +* TermDatabaseSygus::regstierEnumerator(...) based * on the strategy, which inform the rest of the system to enumerate values * of particular types in the grammar through use of fresh variables which * we call "enumerators". @@ -58,14 +58,14 @@ class CegConjecture; * Points (1)-(3) happen within a call to CegConjecturePbe::initialize(...). * * Notice that each enumerator is associated with a single -* function-to-synthesize, but a function-to-sythesize may be mapped to multiple -* enumerators. Some public functions of this class expect an enumerator as -* input, which we map to a function-to-synthesize via +* function-to-synthesize, but a function-to-sythesize may be mapped to multiple +* enumerators. Some public functions of this class expect an enumerator as +* input, which we map to a function-to-synthesize via * TermDatabaseSygus::getSynthFunFor(e). * * An enumerator is initially "active" but may become inactive if the enumeration * exhausts all possible values in the datatype corresponding to syntactic -* restrictions for it. The search may continue unless all enumerators become +* restrictions for it. The search may continue unless all enumerators become * inactive. * * (4) During search, the extension of quantifier-free datatypes procedure for @@ -73,7 +73,7 @@ class CegConjecture; * discarded based on * inferring when two candidate solutions are equivalent up to examples. * For example, the candidate solutions: -* f = \x ite( x<0, x+1, x ) and f = \x x +* f = \x ite( x < 0, x+1, x ) and f = \x x * are equivalent up to examples on the above conjecture, since they have the * same value on the points x = 0,5,6. Hence, we need only consider one of * them. The interface for querying this is @@ -216,6 +216,21 @@ class CegConjecturePbe : public SygusModule * search space pruning. */ std::map< Node, bool > d_examples_out_invalid; + /** + * Map from candidates to sygus unif utility. This class implements + * the core algorithm (e.g. decision tree learning) that this module relies + * upon. + */ + std::map d_sygus_unif; + /** + * map from candidates to the list of enumerators that are being used to + * build solutions for that candidate by the above utility. + */ + std::map > d_candidate_to_enum; + /** reverse map of above */ + std::map d_enum_to_candidate; + /** map from enumerators to active guards */ + std::map d_enum_to_active_guard; /** for each candidate variable (function-to-synthesize), input of I/O * examples */ std::map< Node, std::vector< std::vector< Node > > > d_examples; @@ -258,583 +273,6 @@ class CegConjecturePbe : public SygusModule std::map > d_pbe_trie; //--------------------------------- end PBE search values - // -------------------------------- decision tree learning - /** 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& vals, - bool pol, - std::vector& 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& vals, bool pol); - /** - * Returns the set of terms that are subsumed by (pol ? vals : !vals). - */ - void getSubsumed(const std::vector& vals, - bool pol, - std::vector& 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& vals, - bool pol, - std::vector& 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& vals, - bool pol, - std::map >& 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 d_children; - /** helper function for above functions */ - Node addTermInternal(Node t, - const std::vector& vals, - bool pol, - std::vector& subsumed, - bool spol, - unsigned index, - int status, - bool checkExistsOnly, - bool checkSubsume); - /** helper function for above functions */ - void getLeavesInternal(const std::vector& vals, - bool pol, - std::map >& v, - unsigned index, - int status); - }; - // -------------------------------- end decision tree learning - - //------------------------------ 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; - /** - * The active guard of this enumerator (see - * TermDbSygus::d_enum_to_active_guard). - */ - Node d_active_guard; - /** - * 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; - - //---------------------------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(CegConjecturePbe* pbe, - Node v, - std::vector& 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 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 > 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 d_enum_subsume; - /** Map from values to their index in d_enum_vals. */ - std::map 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 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 d_enum; - /** map from node roles to strategy nodes */ - std::map 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(); - bool isNonTrivial(); - }; - /** 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 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& 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 c, and stores these into lemmas. - */ - void staticLearnRedundantOps(Node c, 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 c, - Node e, - NodeRole nrole, - std::map >& visited, - std::map >& needs_cons, - int ind, - bool isCond); - //------------------------------ end strategy registration - - //------------------------------ constructing solutions - /** Unification context - * - * This class maintains state information during calls to - * CegConjecturePbe::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(CegConjecturePbe* 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 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(CegConjecturePbe* pbe, - std::vector& 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 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(CegConjecturePbe* pbe, - std::vector& 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(CegConjecturePbe* pbe, - const std::vector& vals, - std::vector& 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(CegConjecturePbe* pbe, - bool isPrefix, - const std::vector& ex_vals, - const std::vector& vals, - std::vector& inc, - unsigned& tot); - /** returns true if ex_vals[i] = vals[i] for all active indices i. */ - bool isStringSolved(CegConjecturePbe* pbe, - const std::vector& ex_vals, - const std::vector& 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 > 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 > d_look_ahead_sols; - }; - /** map from enumerators to the above info class */ - std::map d_uinfo; - - private: - /** true and false nodes */ - Node d_true; - Node d_false; - }; - - /** construct solution - * - * This method tries to construct a solution for function-to-synthesize c - * based on the strategy stored for c in d_cinfo, which may include - * synthesis-by-unification approaches for ite and string concatenation terms. - * These approaches include the work of Alur et al. TACAS 2017. - * If it cannot construct a solution, it returns the null node. - */ - Node constructSolution( Node c ); - /** 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 > 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 context x */ - bool isValid(CegConjecturePbe* pbe, UnifContext& x); - }; }; }/* namespace CVC4::theory::quantifiers */ diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index ee0590b6b..2250deb6f 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -514,36 +514,250 @@ void SubsumeTrie::getLeaves(const std::vector& vals, getLeavesInternal(vals, pol, v, 0, -2); } -SygusUnif::SygusUnif(QuantifiersEngine* qe) : d_qe(qe) +SygusUnif::SygusUnif() { - 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& lemmas, - std::vector& enums) +void SygusUnif::initialize(QuantifiersEngine* qe, + Node f, + std::vector& enums, + std::vector& lemmas) { - d_candidate = candidate; - // TODO + d_candidate = f; + d_qe = qe; + d_tds = qe->getTermDatabaseSygus(); + + TypeNode tn = f.getType(); + d_cinfo[f].initialize(f); + // collect the enumerator types and form the strategy + collectEnumeratorTypes(f, tn, role_equal); + // add the enumerators + enums.insert(enums.end(), + d_cinfo[f].d_esym_list.begin(), + d_cinfo[f].d_esym_list.end()); + // learn redundant ops + staticLearnRedundantOps(f, lemmas); } void SygusUnif::resetExamples() { + d_examples.clear(); + d_examples_out.clear(); + // also clear information in strategy tree // TODO } void SygusUnif::addExample(const std::vector& input, Node output) { - // TODO + d_examples[d_candidate].push_back(input); + d_examples_out[d_candidate].push_back(output); } void SygusUnif::notifyEnumeration(Node e, Node v, std::vector& lemmas) { - // TODO + Node c = d_candidate; + Assert(!d_examples.empty()); + Assert(d_examples.size() == d_examples_out.size()); + std::map::iterator it = d_einfo.find(e); + Assert(it != d_einfo.end()); + Assert( + std::find(it->second.d_enum_vals.begin(), it->second.d_enum_vals.end(), v) + == it->second.d_enum_vals.end()); + // The explanation for why the current value should be excluded in future + // iterations. + Node exp_exc; + + std::map::iterator itc = d_cinfo.find(c); + Assert(itc != d_cinfo.end()); + TypeNode xtn = e.getType(); + Node bv = d_tds->sygusToBuiltin(v, xtn); + std::map > >::iterator itx = + d_examples.find(c); + std::map >::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 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 exp_exc_vec; + if (getExplanationForEnumeratorExclude( + c, e, 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::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 results; + Node templ = itv->second.d_template; + TNode templ_var = itv->second.d_template_arg; + std::map 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 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(e, v); + } + exp_exc = exp_exc.negate(); + Trace("sygus-pbe-enum-lemma") + << "SygusUnif : enumeration exclude lemma : " << exp_exc << std::endl; + lemmas.push_back(exp_exc); } Node SygusUnif::constructSolution() @@ -611,7 +825,7 @@ void SygusUnif::registerEnumerator( << static_cast(tn.toType()).getDatatype().getName(); Trace("sygus-unif-debug") << ", role = " << enum_role << ", in search = " << inSearch << std::endl; - d_einfo[et].initialize(c, enum_role); + d_einfo[et].initialize(enum_role); // if we are actually enumerating this (could be a compound node in the // strategy) if (inSearch) @@ -1336,209 +1550,7 @@ void SygusUnif::staticLearnRedundantOps( } } -// ------------------------------------------- solution construction from -// enumeration - -void SygusUnif::addEnumeratedValue(Node x, Node v, std::vector& lems) -{ - std::map::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::iterator itc = d_cinfo.find(c); - Assert(itc != d_cinfo.end()); - TypeNode xtn = x.getType(); - Node bv = d_tds->sygusToBuiltin(v, xtn); - std::map > >::iterator itx = - d_examples.find(c); - std::map >::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 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 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::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 results; - Node templ = itv->second.d_template; - TNode templ_var = itv->second.d_template_arg; - std::map 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 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); -} +// ------------------------------------ solution construction from enumeration bool SygusUnif::useStrContainsEnumeratorExclude(Node x, EnumInfo& ei) { @@ -1623,12 +1635,11 @@ bool SygusUnif::getExplanationForEnumeratorExclude(Node c, 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); + ncset.init(x, d_examples[c], itxo->second, cmp_indices); // construct the generalized explanation d_tds->getExplain()->getExplanationFor(x, v, exp, ncset); Trace("sygus-pbe-cterm") @@ -1636,7 +1647,6 @@ bool SygusUnif::getExplanationForEnumeratorExclude(Node c, << " due to negative containment." << std::endl; return true; } - */ } return false; } @@ -1645,16 +1655,14 @@ void SygusUnif::EnumInfo::addEnumValue(SygusUnif* pbe, Node v, std::vector& results) { + // should not have been enumerated before + Assert(d_enum_val_to_index.find(v) == d_enum_val_to_index.end()); 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::initialize(EnumRole role) { d_role = role; } void SygusUnif::EnumInfo::setSolved(Node slv) { d_enum_solved = slv; } @@ -1886,6 +1894,7 @@ Node SygusUnif::constructSolution( for (unsigned i = 0, size = einfo.d_enum_vals.size(); i < size; i++) { Node val_t = einfo.d_enum_vals[i]; + Assert(incr.find(val_t) == incr.end()); indent("sygus-pbe-dt-debug", ind); Trace("sygus-pbe-dt-debug") << "increment string values : " << val_t << " : "; diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 68ed442a8..d46fb9c86 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -339,7 +339,7 @@ class SygusUnif friend class UnifContext; public: - SygusUnif(QuantifiersEngine* qe); + SygusUnif(); ~SygusUnif(); /** initialize @@ -356,7 +356,10 @@ class SygusUnif * those that exclude ITE from enumerators whose role is enum_io when the * strategy is ITE_strat). */ - void initialize(Node f, std::vector& enums, std::vector& lemmas); + void initialize(QuantifiersEngine* qe, + Node f, + std::vector& enums, + std::vector& lemmas); /** reset examples * * Reset the specification for f. @@ -432,7 +435,7 @@ class SygusUnif * role is the "role" the enumerator plays in the high-level strategy, * which is one of enum_* above. */ - void initialize(Node c, EnumRole role); + void initialize(EnumRole role); /** is this enumerator associated with a template? */ bool isTemplated() { return !d_template.isNull(); } /** set conditional @@ -447,10 +450,6 @@ class SygusUnif 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 @@ -586,15 +585,6 @@ class SygusUnif std::map 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& lems); /** domain-specific enumerator exclusion techniques * * Returns true if the value v for x can be excluded based on a -- 2.30.2