From: Andrew Reynolds Date: Fri, 1 Dec 2017 15:07:42 +0000 (-0600) Subject: Refactor and generalize PBE strategies (#1410) X-Git-Tag: cvc5-1.0.0~5437 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f40d813048599b58327fc968344301d39f156da2;p=cvc5.git Refactor and generalize PBE strategies (#1410) --- diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c542e5917..3e8d5f0bb 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -985,7 +985,8 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl; Debug("parser-sygus") << " add constructors..." << std::endl; - for (unsigned i = 0, size = cnames.size(); i < size; i++) + // size of cnames changes, this loop must check size + for (unsigned i = 0; i < cnames.size(); i++) { bool is_dup = false; bool is_dup_op = false; @@ -1121,8 +1122,12 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, std::stringstream ss; ss << dt.getName() << "_" << i << "_" << cnames[i]; cnames[i] = ss.str(); + Debug("parser-sygus") << " construct the datatype " << cnames[i] << "..." + << std::endl; // add the sygus constructor dt.addSygusConstructor(ops[i], cnames[i], cargs[i], spc); + Debug("parser-sygus") << " finished constructing the datatype" + << std::endl; } } diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/ce_guided_pbe.cpp index 97cded35c..d46fed686 100644 --- a/src/theory/quantifiers/ce_guided_pbe.cpp +++ b/src/theory/quantifiers/ce_guided_pbe.cpp @@ -23,11 +23,10 @@ using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace std; namespace CVC4 { +namespace theory { +namespace quantifiers { void indent( const char * c, int ind ) { if( Trace.isOn(c) ){ @@ -46,26 +45,55 @@ void print_val( const char * c, std::vector< Node >& vals, bool pol = true ){ } } -void CegConjecturePbe::print_role(const char* c, unsigned r) +std::ostream& operator<<(std::ostream& os, EnumRole r) { switch(r){ - case CegConjecturePbe::enum_io:Trace(c) << "IO";break; - case CegConjecturePbe::enum_ite_condition:Trace(c) << "CONDITION";break; - case CegConjecturePbe::enum_concat_term:Trace(c) << "CTERM";break; - case CegConjecturePbe::enum_any:Trace(c) << "ANY";break; - default:Trace(c) << "role_" << r;break; + case enum_invalid: os << "INVALID"; break; + case enum_io: os << "IO"; break; + case enum_ite_condition: os << "CONDITION"; break; + case enum_concat_term: os << "CTERM"; break; + default: os << "enum_" << static_cast(r); break; } + return os; } -void CegConjecturePbe::print_strat(const char* c, unsigned s) +std::ostream& operator<<(std::ostream& os, NodeRole r) { - switch (s) + switch (r) { - case CegConjecturePbe::strat_ITE: Trace(c) << "ITE"; break; - case CegConjecturePbe::strat_CONCAT: Trace(c) << "CONCAT"; break; - case CegConjecturePbe::strat_ID: Trace(c) << "ID"; break; - default: Trace(c) << "strat_" << s; break; + case role_equal: os << "equal"; break; + case role_string_prefix: os << "string_prefix"; break; + case role_string_suffix: os << "string_suffix"; break; + case role_ite_condition: os << "ite_condition"; break; + default: os << "role_" << static_cast(r); break; } + return os; +} + +EnumRole getEnumeratorRoleForNodeRole(NodeRole r) +{ + switch (r) + { + case role_equal: return enum_io; break; + case role_string_prefix: return enum_concat_term; break; + case role_string_suffix: return enum_concat_term; break; + case role_ite_condition: return enum_ite_condition; break; + default: break; + } + return enum_invalid; +} + +std::ostream& operator<<(std::ostream& os, StrategyType st) +{ + switch (st) + { + case strat_ITE: os << "ITE"; break; + case strat_CONCAT_PREFIX: os << "CONCAT_PREFIX"; break; + case strat_CONCAT_SUFFIX: os << "CONCAT_SUFFIX"; break; + case strat_ID: os << "ID"; break; + default: os << "strat_" << static_cast(st); break; + } + return os; } CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p) @@ -196,7 +224,7 @@ void CegConjecturePbe::initialize(Node n, TypeNode ctn = c.getType(); d_cinfo[c].initialize( c ); // collect the enumerator types / form the strategy - collectEnumeratorTypes( c, ctn, enum_io ); + collectEnumeratorTypes(c, ctn, role_equal); // if we have non-trivial strategies, then use pbe if( d_cinfo[c].isNonTrivial() ){ // static learning of redundant constructors @@ -340,289 +368,514 @@ Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, // ----------------------------- establishing enumeration types - -void CegConjecturePbe::registerEnumerator( Node et, Node c, TypeNode tn, unsigned enum_role, bool inSearch ) { - Trace("sygus-unif-debug") << "...register " << et << " for " << ((DatatypeType)tn.toType()).getDatatype().getName(); - Trace("sygus-unif-debug") << ", role = "; - print_role( "sygus-unif-debug", enum_role ); - Trace("sygus-unif-debug") << ", in search = " << inSearch << std::endl; - d_einfo[et].initialize(c, enum_role); - // if we are actually enumerating this (could be a compound node in the strategy) - if( inSearch ){ - std::map< TypeNode, Node >::iterator itn = d_cinfo[c].d_search_enum.find( tn ); - if( itn==d_cinfo[c].d_search_enum.end() ){ - // use this for the search - d_cinfo[c].d_search_enum[tn] = et; - d_cinfo[c].d_esym_list.push_back( et ); - d_einfo[et].d_enum_slave.push_back( et ); - //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::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, unsigned enum_role ) { - if( d_cinfo[e].d_tinfo.find( tn )==d_cinfo[e].d_tinfo.end() ){ +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 ); } - if( d_cinfo[e].d_tinfo[tn].d_enum.find( enum_role )==d_cinfo[e].d_tinfo[tn].d_enum.end() ){ - - Node ee = NodeManager::currentNM()->mkSkolem( "ee", tn ); - d_cinfo[e].d_tinfo[tn].d_enum[enum_role] = ee; - Trace("sygus-unif-debug") << "...enumerator " << ee << " for " << ((DatatypeType)tn.toType()).getDatatype().getName() << ", role = "; - print_role( "sygus-unif-debug", enum_role ); - Trace("sygus-unif-debug") << std::endl; - // wait to register : may or may not actually be enumerating it - - if( enum_role==enum_io ){ - // look at information on how we will construct solutions for this type - Assert( tn.isDatatype() ); - const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); - Assert( dt.isSygus() ); - std::map< Node, std::vector< TypeNode > > cop_to_child_types; - std::map< Node, std::map< unsigned, Node > > cop_to_child_templ; - std::map< Node, std::map< unsigned, Node > > cop_to_child_templ_arg; - std::map< Node, unsigned > cop_to_strat; - std::map< Node, unsigned > cop_to_cindex; - - // look at builtin operartors first (when r=0), then defined operators - // (when r=1) - for( unsigned r=0; r<2; r++ ){ - for( unsigned j=0; j::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(); } - }else if( cop_to_strat.find( cop )==cop_to_strat.end() ){ - // could be a defined function (this handles the ICFP benchmarks) - std::vector< Node > utchildren; - utchildren.push_back( cop ); - std::vector< Node > sks; - std::vector< TypeNode > sktns; - for( unsigned k=0; kmkSkolem( "ut", ttn ); - sks.push_back( kv ); - sktns.push_back( ttn ); - utchildren.push_back( kv ); + 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); } - Node ut = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, utchildren ); - std::vector< Node > echildren; - echildren.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) ); - echildren.push_back( ut ); - Node sbvl = Node::fromExpr( dt.getSygusVarList() ); - for( unsigned k=0; kmkNode( kind::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 << std::endl; - Trace("sygus-unif-debug2") << "Type : " << eut.getType() << std::endl; - - if( eut.getKind()==kind::ITE ){ - if( dt[j].getNumArgs()>=eut.getNumChildren() ){ - cop_to_strat[cop] = strat_ITE; - } - }else if( eut.getKind()==kind::STRING_CONCAT ){ - if (dt[j].getNumArgs() >= eut.getNumChildren() - && eut.getNumChildren() == 2) + } + } + } + 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_strat[cop] = strat_CONCAT; - } - }else if( eut.getKind()==kind::APPLY_UF ){ - // identity operator? - if( dt[j].getNumArgs()==1 ){ - cop_to_strat[cop] = strat_ID; - } - } - - if( cop_to_strat.find( cop )!=cop_to_strat.end() ){ - std::map< unsigned, unsigned > templ_injection; - std::vector< Node > vs; - std::vector< Node > ss; - std::map< Node, unsigned > templ_var_index; - for( unsigned k=0; kmkNode( kind::APPLY_UF, echildren ); - vs.push_back( esk ); - Node tvar = NodeManager::currentNM()->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") << "Defined constructor " << j << ", base term is " << eut << std::endl; - std::map< unsigned, Node > test_args; - if( cop_to_strat[cop] == strat_ID ){ - test_args[0] = eut; + cop_to_carg_list[cop].push_back(sk_index); }else{ - for( unsigned k=0; k::iterator it = test_args.begin(); it != test_args.end(); ++it ){ - unsigned k = it->first; - Node eut_c = it->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-debug2") << "...failed to find injection (range)." << std::endl; - cop_to_strat.erase( cop ); - break; - } - if( templ_injection.find( k )==templ_injection.end() ){ - Trace("sygus-unif-debug2") << "...failed to find injection (domain)." << 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); } - if( cop_to_strat.find( cop )!=cop_to_strat.end() ){ - Trace("sygus-unif") << "...type " << dt.getName() << " has defined constructor matching strategy "; - print_strat("sygus-unif", cop_to_strat[cop]); - Trace("sygus-unif") << "..." << std::endl; - for( unsigned k=0; k::iterator itc = cop_to_strat.begin(); itc != cop_to_strat.end(); ++itc ){ - if( itc->second==strat_CONCAT || ( itc->second==strat_ID && dt.getNumConstructors()==1 ) ){ - search_this = false; - break; - } + } + 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); } - Trace("sygus-unif-debug2") << "...this register..." << std::endl; - registerEnumerator( ee, e, tn, enum_role, search_this ); - - if( cop_to_child_types.empty() ){ - Trace("sygus-unif") << "...consider " << dt.getName() << " a basic type" << std::endl; - }else{ - for( std::map< Node, std::vector< TypeNode > >::iterator itct = cop_to_child_types.begin(); itct != cop_to_child_types.end(); ++itct ){ - Node cop = itct->first; - Assert( cop_to_strat.find( cop )!=cop_to_strat.end() ); - unsigned strat = cop_to_strat[cop]; - d_cinfo[e].d_tinfo[tn].d_strat[cop].d_this = strat; - Trace("sygus-unif-debug") << "Process strategy for operator : " << cop << " : "; - print_strat("sygus-unif-debug", strat ); - Trace("sygus-unif-debug") << std::endl; - - for( unsigned j=0; jsecond.size(); j++ ){ - //calculate if we should allocate a new enumerator : should be true if we have a new role - unsigned enum_role_c = enum_role; - if( strat==strat_ITE ){ - if( j==0 ){ - enum_role_c = enum_ite_condition; - }else{ - // role is the same as parent - } - }else if( strat==strat_CONCAT ){ - enum_role_c = enum_concat_term; - }else if( strat==strat_ID ){ - // role is the same as parent + } + } + + // 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; } - - // register the child type - TypeNode ct = itct->second[j]; - d_cinfo[e].d_tinfo[tn].d_strat[cop].d_csol_cts.push_back( ct ); - - // 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 = NodeManager::currentNM()->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, enum_role_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() << ", role = "; - print_role( "sygus-unif-debug", enum_role_c ); - Trace("sygus-unif-debug") << std::endl; - collectEnumeratorTypes( e, ct, enum_role_c ); - // otherwise use the previous - Assert( d_cinfo[e].d_tinfo[ct].d_enum.find( enum_role_c )!=d_cinfo[e].d_tinfo[ct].d_enum.end() ); - et = d_cinfo[e].d_tinfo[ct].d_enum[enum_role_c]; + } + 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; } - Trace("sygus-unif-debug") << "Register child enumerator " << et << ", arg " << j << " of " << cop << ", role = "; - print_role( "sygus-unif-debug", enum_role_c ); - Trace("sygus-unif-debug") << std::endl; - Assert( !et.isNull() ); - d_cinfo[e].d_tinfo[tn].d_strat[cop].d_cenum.push_back( et ); } - Trace("sygus-unif") << "Initialized strategy "; - print_strat( "sygus-unif", strat ); + // 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 = " << d_cinfo[e].d_tinfo[tn].d_strat[cop].d_cenum.size() << std::endl; - Assert( d_cinfo[e].d_tinfo[tn].d_strat[cop].d_cenum.size()==d_cinfo[e].d_tinfo[tn].d_strat[cop].d_csol_cts.size() ); + 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); } - }else{ - Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl; - registerEnumerator( ee, e, tn, enum_role, true ); } } } @@ -637,6 +890,7 @@ bool CegConjecturePbe::inferTemplate( unsigned k, Node n, std::map< Node, unsign 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; } } @@ -663,112 +917,137 @@ void CegConjecturePbe::staticLearnRedundantOps( Node c, std::vector< Node >& lem 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 = "; - print_role("sygus-unif", itns->second.getRole()); - Trace("sygus-unif") << std::endl; + Trace("sygus-unif") << " " << es << ", role = " << itns->second.getRole() + << std::endl; } } Trace("sygus-unif") << std::endl; Trace("sygus-unif") << "Strategy for candidate " << c << " is : " << std::endl; - std::map< Node, bool > visited; - std::vector< Node > redundant; - staticLearnRedundantOps( c, d_cinfo[c].getRootEnumerator(), visited, redundant, lemmas, 0 ); - for( unsigned i=0; i > visited; + std::map > needs_cons; + staticLearnRedundantOps( + c, d_cinfo[c].getRootEnumerator(), role_equal, visited, needs_cons, 0); + // 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, std::map< Node, bool >& visited, std::vector< Node >& redundant, - std::vector< Node >& lemmas, int ind ) { - +void CegConjecturePbe::staticLearnRedundantOps( + Node c, + Node e, + NodeRole nrole, + std::map >& visited, + std::map >& needs_cons, + int ind) +{ std::map< Node, EnumInfo >::iterator itn = d_einfo.find( e ); - Assert( itn!=d_einfo.end() ); - if( visited.find( e )==visited.end() ){ - visited[e] = true; + Assert( itn!=d_einfo.end() ); + if (visited[e].find(nrole) == visited[e].end()) + { + visited[e][nrole] = true; indent("sygus-unif", ind); - Trace("sygus-unif") << e << " : role : "; - print_role("sygus-unif", itn->second.getRole()); - Trace("sygus-unif") << " : "; + Trace("sygus-unif") << e << " :: node role : " << nrole; + Trace("sygus-unif") + << ", type : " + << ((DatatypeType)e.getType().toType()).getDatatype().getName(); + Trace("sygus-unif") << ", enum role : " << itn->second.getRole(); if( itn->second.isTemplated() ){ - Trace("sygus-unif") << "basic, templated : \\ " << itn->second.d_template_arg << ". " << itn->second.d_template << std::endl; + 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() ); - if( itt->second.d_strat.empty() ){ - Trace("sygus-unif") << "basic" << std::endl; - }else{ - Trace("sygus-unif") << "compound" << std::endl; - // various strategies - for( std::map< Node, EnumTypeInfoStrat >::iterator itts = itt->second.d_strat.begin(); itts!=itt->second.d_strat.end(); ++itts ){ + 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()) + { + 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; indent("sygus-unif", ind+1); - Trace("sygus-unif") << "Strategy : "; - unsigned strat = itts->second.d_this; - print_strat("sygus-unif", strat); - Trace("sygus-unif") << std::endl; - for( unsigned i=0; isecond.d_cenum.size(); i++ ){ - std::vector< Node > redundant_c; - bool no_repeat_op = false; - // do not repeat operators that the strategy uses - if( itts->second.d_csol_cts[i]==etn ){ - if( strat==strat_ITE && i!=0 ){ - no_repeat_op = true; - }else if( strat==strat_CONCAT || strat==strat_ID ){ - no_repeat_op = true; - } - } - if( no_repeat_op ){ - redundant_c.push_back( itts->first ); + 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); + } + } + // 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()) + { + 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; } - //do not use standard Boolean connectives in ITE conditions - if( strat==strat_ITE && i==0 && itts->second.d_csol_cts[1]==itts->second.d_csol_cts[2] ){ - TypeNode ctn = itts->second.d_csol_cts[0]; - const Datatype& cdt = ((DatatypeType)ctn.toType()).getDatatype(); - for( unsigned j=0; jgetConsNumKind( ctn, j ); - if( ck!=UNDEFINED_KIND && TermUtil::isBoolConnective( ck ) ){ - bool typeCorrect = true; - for( unsigned k=0; kgetArgType( cdt[j], k )!=ctn ){ - typeCorrect = false; - break; - } - } - if( typeCorrect ){ - Trace("sygus-unif-debug") << "Exclude Boolean connective in ITE conditional : " << ck << " in conditional type " << cdt.getName() << std::endl; - Node exc_cons = Node::fromExpr( cdt[j].getConstructor() ); - if( std::find( redundant_c.begin(), redundant_c.end(), exc_cons )==redundant_c.end() ){ - redundant_c.push_back( exc_cons ); - } - } - } - } + } + // 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]; } - // recurse - staticLearnRedundantOps( c, itts->second.d_cenum[i], visited, redundant_c, lemmas, ind+2 ); } } } } }else{ indent("sygus-unif", ind); - Trace("sygus-unif") << e << std::endl; - } - if( !redundant.empty() ){ - // TODO : if this becomes more general, must get master enumerator here - if( itn->second.d_enum_slave.size()==1 ){ - for( unsigned i=0; i& std::vector< Node > exp_exc_vec; if( getExplanationForEnumeratorExclude( c, x, v, 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( kind::AND, exp_exc_vec ); + 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{ //if( cond_vals.size()!=2 ){ @@ -981,7 +1262,8 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& // if we did not already explain why this should be excluded, use default exp_exc = d_tds->getExplain()->getExplanationForConstantEquality(x, v); } - Node exlem = NodeManager::currentNM()->mkNode( kind::OR, g.negate(), exp_exc.negate() ); + 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 ); }else{ @@ -1017,7 +1299,8 @@ bool CegConjecturePbe::getExplanationForEnumeratorExclude( Node c, Node x, Node cmp_indices[index].push_back( i ); */ Trace("sygus-pbe-cterm-debug") << " " << results[i] << " <> " << itxo->second[i]; - Node cont = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, itxo->second[i], results[i] ); + Node cont = NodeManager::currentNM()->mkNode( + STRING_STRCTN, itxo->second[i], results[i]); Node contr = Rewriter::rewrite( cont ); if( contr==d_false ){ cmp_indices.push_back( i ); @@ -1067,6 +1350,12 @@ void CegConjecturePbe::EnumInfo::addEnumValue( CegConjecturePbe * pbe, Node v, s */ } +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; @@ -1083,7 +1372,7 @@ void CegConjecturePbe::CandidateInfo::initializeType( TypeNode tn ) { } Node CegConjecturePbe::CandidateInfo::getRootEnumerator() { - std::map< unsigned, Node >::iterator it = d_tinfo[d_root].d_enum.find( enum_io ); + 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; } @@ -1346,7 +1635,7 @@ Node CegConjecturePbe::constructSolution( Node c ){ Node e = itc->second.getRootEnumerator(); UnifContext x; x.initialize( this, c ); - Node vcc = constructSolution( c, e, x, 1 ); + 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; @@ -1399,409 +1688,509 @@ Node CegConjecturePbe::constructBestStringToConcat( std::vector< Node > strs, std::map< Node, std::vector< unsigned > > incr, UnifContext& x ) { Assert( !strs.empty() ); - // TODO - double r = Random::getRandom().pickDouble(0.0, 1.0); - unsigned cindex = r*strs.size(); - if( cindex>strs.size() ){ - cindex = strs.size() - 1; - } - return strs[cindex]; -} - -Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int ind ) { - indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") << "ConstructPBE: enum: " << e << " in context "; - print_val("sygus-pbe-dt-debug", x.d_vals); - Trace("sygus-pbe-dt-debug") << std::endl; + 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")) + { + indent("sygus-pbe-dt-debug", ind); + Trace("sygus-pbe-dt-debug") << "ConstructPBE: (" << e << ", " << nrole + << ") for type " << etn << " in context "; + print_val("sygus-pbe-dt-debug", x.d_vals); + if (x.d_has_string_pos != role_invalid) + { + Trace("sygus-pbe-dt-debug") << ", string context [" << x.d_has_string_pos; + for (unsigned i = 0, size = x.d_str_pos.size(); i < size; i++) + { + Trace("sygus-pbe-dt-debug") << " " << x.d_str_pos[i]; + } + Trace("sygus-pbe-dt-debug") << "]"; + } + Trace("sygus-pbe-dt-debug") << std::endl; + } + // enumerator type info + std::map::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 (itn->second.getRole() == enum_any) - { - indent("sygus-pbe-dt", ind); - ret_dt = constructBestSolvedTerm( itn->second.d_enum_vals, x ); - Trace("sygus-pbe-dt") << "return PBE: success : use any " << d_tds->sygusToBuiltin( ret_dt ) << std::endl; - Assert( !ret_dt.isNull() ); - } - else if (itn->second.getRole() == enum_io && !x.isReturnValueModified() - && itn->second.isSolved()) + if (nrole == role_equal) { - // this type has a complete solution - ret_dt = itn->second.getSolved(); - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "return PBE: success : solved " << d_tds->sygusToBuiltin( ret_dt ) << std::endl; - Assert( !ret_dt.isNull() ); - }else{ - TypeNode etn = e.getType(); - std::map< TypeNode, EnumTypeInfo >::iterator itt = d_cinfo[c].d_tinfo.find( etn ); - Assert( itt!=d_cinfo[c].d_tinfo.end() ); - if( d_tds->sygusToBuiltinType( e.getType() ).isString() ){ - // check if a current value that closes all examples - - // get the term enumerator for this type - bool success = true; - std::map< Node, EnumInfo >::iterator itet; - if (itn->second.getRole() == enum_concat_term) + if (!x.isReturnValueModified()) + { + if (einfo.isSolved()) { - itet = itn; - }else{ - std::map< unsigned, Node >::iterator itnt = itt->second.d_enum.find( enum_concat_term ); + // this type has a complete solution + ret_dt = einfo.getSolved(); + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") << "return PBE: success : solved " + << d_tds->sygusToBuiltin(ret_dt) << std::endl; + Assert(!ret_dt.isNull()); + } + else + { + // could be conditionally solved + std::vector subsumed_by; + einfo.d_term_trie.getSubsumedBy(this, x.d_vals, true, subsumed_by); + if (!subsumed_by.empty()) + { + ret_dt = constructBestSolvedTerm(subsumed_by, x); + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") << "return PBE: success : conditionally solved" + << d_tds->sygusToBuiltin(ret_dt) << std::endl; + } + else + { + indent("sygus-pbe-dt-debug", ind); + Trace("sygus-pbe-dt-debug") + << " ...not currently conditionally solved." << std::endl; + } + } + } + if (ret_dt.isNull()) + { + if (d_tds->sygusToBuiltinType(e.getType()).isString()) + { + // check if a current value that closes all examples + // get the term enumerator for this type + bool success = true; + std::map::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 ){ - Assert( itet!=d_einfo.end() ); - - // get the current examples - std::map< Node, std::vector< Node > >::iterator itx = d_examples_out.find( c ); - Assert( itx!=d_examples_out.end() ); - std::vector< CVC4::String > ex_vals; - x.getCurrentStrings( this, itx->second, ex_vals ); - Assert( itn->second.d_enum_vals.size()==itn->second.d_enum_vals_res.size() ); - - // test each example in the term enumerator for the type - std::vector< Node > str_solved; - for( unsigned i=0; isecond.d_enum_vals.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 (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); + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") << "return PBE: success : string solved " + << d_tds->sygusToBuiltin(ret_dt) << std::endl; + } + else + { + indent("sygus-pbe-dt-debug", ind); + Trace("sygus-pbe-dt-debug") << " ...not currently string solved." + << std::endl; } - } - if( !str_solved.empty() ){ - ret_dt = constructBestStringSolvedTerm( str_solved, x ); - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "return PBE: success : string solved " << d_tds->sygusToBuiltin( ret_dt ) << std::endl; - }else{ - indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") << " ...not currently string solved." << std::endl; } } } - else if (itn->second.getRole() == enum_io && !x.isReturnValueModified()) + } + 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) { - // it has an enumerated value that is conditionally correct under the current assumptions - std::vector< Node > subsumed_by; - itn->second.d_term_trie.getSubsumedBy( this, x.d_vals, true, subsumed_by ); - if( !subsumed_by.empty() ){ - ret_dt = constructBestSolvedTerm( subsumed_by, x ); + 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")) + { + indent("sygus-pbe-dt-debug", ind); + Trace("sygus-pbe-dt-debug") << "current strings : " << std::endl; + for (unsigned i = 0, size = ex_vals.size(); i < size; i++) + { + indent("sygus-pbe-dt-debug", ind + 1); + Trace("sygus-pbe-dt-debug") << ex_vals[i] << std::endl; + } + } + + // check if there is a value for which is a prefix/suffix of all active + // examples + Assert(einfo.d_enum_vals.size() == einfo.d_enum_vals_res.size()); + + for (unsigned i = 0, size = einfo.d_enum_vals.size(); i < size; i++) + { + Node val_t = einfo.d_enum_vals[i]; + indent("sygus-pbe-dt-debug", ind); + Trace("sygus-pbe-dt-debug") << "increment string values : " << val_t + << " : "; + Assert(einfo.d_enum_vals_res[i].size() == itx->second.size()); + unsigned tot = 0; + bool exsuccess = x.getStringIncrement(this, + isPrefix, + ex_vals, + einfo.d_enum_vals_res[i], + incr[val_t], + tot); + if (!exsuccess) + { + incr.erase(val_t); + Trace("sygus-pbe-dt-debug") << "...fail" << std::endl; + } + else + { + total_inc[val_t] = tot; + inc_strs.push_back(val_t); + Trace("sygus-pbe-dt-debug") << "...success, total increment = " << tot + << std::endl; + } + } + + if (!incr.empty()) + { + ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr, x); + Assert(!ret_dt.isNull()); indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "return PBE: success : conditionally solved" << d_tds->sygusToBuiltin( ret_dt ) << std::endl; + Trace("sygus-pbe-dt") << "PBE: CONCAT strategy : choose " + << (isPrefix ? "pre" : "suf") << "fix value " + << d_tds->sygusToBuiltin(ret_dt) << std::endl; + // update the context + bool ret = x.updateStringPosition(this, incr[ret_dt]); + AlwaysAssert(ret == (total_inc[ret_dt] > 0)); + x.d_has_string_pos = nrole; }else{ - indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") << " ...not currently conditionally solved." << std::endl; + 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; } } - if( ret_dt.isNull() ){ - if( !itn->second.isTemplated() ){ - // try to construct a compound solution, if strategies are available - - // do various strategies - for( std::map< Node, EnumTypeInfoStrat >::iterator itts = itt->second.d_strat.begin(); itts!=itt->second.d_strat.end(); ++itts ){ - std::map< unsigned, Node > dt_children_cons; - unsigned strat = itts->second.d_this; - - bool success = true; - - // for ITE - std::map< unsigned, Node > look_ahead_solved_children; - Node split_cond_enum; - int split_cond_res_index = -1; - - //for CONCAT - Node incr_val; - int incr_type = 0; - std::map< Node, std::vector< unsigned > > incr; - - // construct the child order based on heuristics - std::vector< unsigned > corder; - std::unordered_set cused; - if( strat==strat_CONCAT ){ - for( unsigned r=0; r<2; r++ ){ - // Concatenate strategy can only be applied from the endpoints. - // This chooses the appropriate endpoint for which we stay within - // the same SyGuS type. - // In other words, if we are synthesizing based on a production - // rule ( T -> str.++( T1, ..., Tn ) ), then we - // prefer recursing on the 1st argument of the concat if T1 = T, - // and the last argument if Tn = T. - unsigned sc = r==0 ? 0 : itts->second.d_cenum.size()-1; - Node ce = itts->second.d_cenum[sc]; - if( ce.getType()==etn ){ - // prefer simple recursion (self type) - Assert( d_einfo.find( ce )!=d_einfo.end() ); - Assert(d_einfo[ce].getRole() == enum_concat_term); - corder.push_back( sc ); - cused.insert(sc); - break; - } - } + else + { + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") + << "PBE: failed CONCAT strategy, prefix/suffix mismatch." + << std::endl; + } + } + if (ret_dt.isNull() && !einfo.isTemplated()) + { + // we will try a single strategy + EnumTypeInfoStrat* etis = nullptr; + std::map::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() + && !x.isValidStrategy(snode.d_strats[sindex])) + { + sindex++; + } + // if we found a eligible strategy + if (sindex < snode.d_strats.size()) + { + etis = snode.d_strats[sindex]; + } + } + } + if (etis != nullptr) + { + StrategyType strat = etis->d_this; + indent("sygus-pbe-dt", ind + 1); + Trace("sygus-pbe-dt") << "...try STRATEGY " << strat << "..." + << std::endl; + + std::map 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++) + { + 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; + 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); } - // fill remaining children for which there is no preference - for (unsigned sc = 0; sc < itts->second.d_cenum.size(); sc++) + + // recurse + if (strat == strat_ITE && sc == 0) { - if (cused.find(sc) == cused.end()) + 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()) { - corder.push_back( sc ); - } - } - Assert( corder.size()==itts->second.d_cenum.size() ); - - - for( unsigned scc=0; scc::iterator itla = look_ahead_solved_children.find( sc ); - if( itla!=look_ahead_solved_children.end() ){ - rec_c = itla->second; - indent("sygus-pbe-dt-debug", ind+1); - Trace("sygus-pbe-dt-debug") << "ConstructPBE: look ahead solved : " << d_tds->sygusToBuiltin( rec_c ) << std::endl; - }else{ - // get the child enumerator - Node ce = itts->second.d_cenum[sc]; - if( strat==strat_ITE && scc==0 ){ - Assert( itts->second.d_cenum.size()==3 ); // for now, fix to 3 child ITEs - // choose a condition - - // register the condition enumerator - std::map< Node, EnumInfo >::iterator itnc = d_einfo.find( ce ); - Assert( itnc!=d_einfo.end() ); - // 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; - x.d_uinfo[ce].d_status = 0; - Assert( itnc->second.d_enum_vals.size()==itnc->second.d_enum_vals_res.size() ); - for( unsigned i=1; i<=2; i++ ){ - Node te = itts->second.d_cenum[i]; - std::map< Node, EnumInfo >::iterator itnt = d_einfo.find( te ); - Assert( itnt!=d_einfo.end() ); - bool branch_pol = ( i==1 ); - // for each condition, get terms that satisfy it in this branch - for( unsigned k=0; ksecond.d_enum_vals.size(); k++ ){ - Node cond = itnc->second.d_enum_vals[k]; - std::vector< Node > solved; - itnt->second.d_term_trie.getSubsumedBy( this, itnc->second.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-debug") << " reg : PBE: ..." << d_tds->sygusToBuiltin( slv ) << " is a solution under branch " << i; - Trace("sygus-pbe-dt-debug") << " of condition " << d_tds->sygusToBuiltin( cond ) << std::endl; - x.d_uinfo[ce].d_look_ahead_sols[cond][i] = slv; - } - } - } - } - } - - // get the conditionals in the current context : they must be distinguishable - std::map< int, std::vector< Node > > possible_cond; - std::map< Node, int > solved_cond; //stores branch - itnc->second.d_term_trie.getLeaves( this, x.d_vals, true, possible_cond ); - - std::map< int, std::vector< Node > >::iterator itpc = possible_cond.find( 0 ); - if( itpc!=possible_cond.end() ){ - indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") << "PBE : We have " << itpc->second.size() << " distinguishable conditionals:" << std::endl; - for( unsigned k=0; ksecond.size(); k++ ){ - indent("sygus-pbe-dt-debug", ind+1); - Trace("sygus-pbe-dt-debug") << d_tds->sygusToBuiltin( itpc->second[k] ) << std::endl; - } - - - // static look ahead conditional : choose conditionals that have solved terms in at least one branch - // only applicable if we have not modified the return value - std::map< int, std::vector< Node > > solved_cond; - if( !x.isReturnValueModified() ){ - Assert( x.d_uinfo.find( ce )!=x.d_uinfo.end() ); - int solve_max = 0; - for( unsigned k=0; ksecond.size(); k++ ){ - Node cond = itpc->second[k]; - std::map< Node, std::map< unsigned, Node > >::iterator itla = x.d_uinfo[ce].d_look_ahead_sols.find( cond ); - if( itla!=x.d_uinfo[ce].d_look_ahead_sols.end() ){ - int nsolved = itla->second.size(); - solve_max = nsolved > solve_max ? nsolved : solve_max; - solved_cond[nsolved].push_back( cond ); - } - } - int n = solve_max; - while( n>0 ){ - if( !solved_cond[n].empty() ){ - rec_c = constructBestSolvedConditional( solved_cond[n], x ); - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "PBE: ITE strategy : choose solved conditional " << d_tds->sygusToBuiltin( rec_c ) << " with " << n << " solved children..." << std::endl; - std::map< Node, std::map< unsigned, Node > >::iterator itla = x.d_uinfo[ce].d_look_ahead_sols.find( rec_c ); - Assert( itla!=x.d_uinfo[ce].d_look_ahead_sols.end() ); - for( std::map< unsigned, Node >::iterator itla2 = itla->second.begin(); itla2 != itla->second.end(); ++itla2 ){ - look_ahead_solved_children[ itla2->first ] = itla2->second; - } - break; - } - n--; + 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( + this, + 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; } } - - // dynamic look ahead conditional : compute if there are any solved terms in this branch TODO - if( ind>0 ){ - - } - - // otherwise, guess a conditional - if( rec_c.isNull() ){ - rec_c = constructBestConditional( itpc->second, x ); - Assert( !rec_c.isNull() ); - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "PBE: ITE strategy : choose random conditional " << d_tds->sygusToBuiltin( rec_c ) << std::endl; - } - }else{ - // TODO : degenerate case where children have different types - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "return PBE: failed ITE strategy, cannot find a distinguishable condition" << std::endl; } - if( !rec_c.isNull() ){ - Assert( itnc->second.d_enum_val_to_index.find( rec_c )!=itnc->second.d_enum_val_to_index.end() ); - split_cond_res_index = itnc->second.d_enum_val_to_index[rec_c]; - split_cond_enum = ce; - Assert( split_cond_res_index>=0 ); - Assert( split_cond_res_index<(int)itnc->second.d_enum_vals_res.size() ); + } + } + + // 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( + this, 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")) + { + indent("sygus-pbe-dt-debug", ind + 1); + Trace("sygus-pbe-dt-debug") + << "PBE : We have " << itpc->second.size() + << " distinguishable conditionals:" << std::endl; + for (Node& cond : itpc->second) + { + indent("sygus-pbe-dt-debug", ind + 2); + Trace("sygus-pbe-dt-debug") << d_tds->sygusToBuiltin(cond) + << std::endl; } - }else if( strat==strat_CONCAT && scc==0 ){ - std::map< Node, EnumInfo >::iterator itsc = d_einfo.find( ce ); - Assert( itsc!=d_einfo.end() ); - // ensured by the child order we set above - Assert(itsc->second.getRole() == enum_concat_term); - // check if each return value is a prefix/suffix of all open examples - incr_type = sc==0 ? -1 : 1; - if( x.d_has_string_pos==0 || x.d_has_string_pos==incr_type ){ - bool isPrefix = incr_type==-1; - std::map< Node, unsigned > total_inc; - std::vector< Node > inc_strs; - std::map< Node, std::vector< Node > >::iterator itx = d_examples_out.find( c ); - Assert( itx!=d_examples_out.end() ); - // make the value of the examples - std::vector< CVC4::String > ex_vals; - x.getCurrentStrings( this, itx->second, ex_vals ); - - // check if there is a value for which is a prefix/suffix of all active examples - Assert( itsc->second.d_enum_vals.size()==itsc->second.d_enum_vals_res.size() ); - - for( unsigned i=0; isecond.d_enum_vals.size(); i++ ){ - Node val_t = itsc->second.d_enum_vals[i]; - indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") << "increment string values : " << val_t << " : "; - Assert( itsc->second.d_enum_vals_res[i].size()==itx->second.size() ); - unsigned tot = 0; - bool exsuccess = x.getStringIncrement( this, isPrefix, ex_vals, itsc->second.d_enum_vals_res[i], incr[val_t], tot ); - if( tot==0 ){ - exsuccess = false; - } - 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() ){ - rec_c = constructBestStringToConcat( inc_strs, total_inc, incr, x ); - incr_val = rec_c; - Assert( !rec_c.isNull() ); - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "PBE: CONCAT strategy : choose " << ( isPrefix ? "pre" : "suf" ) << "fix value " << d_tds->sygusToBuiltin( rec_c ) << std::endl; - }else{ - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "PBE: failed CONCAT strategy, no values are " << ( isPrefix ? "pre" : "suf" ) << "fix of all examples." << std::endl; + // 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); } - }else{ - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "PBE: failed CONCAT strategy, prefix/suffix mismatch." << std::endl; - } - }else{ - // a standard term - - // store previous values - std::vector< Node > prev; - std::vector< unsigned > prev_str_pos; - int prev_has_str_pos = false; - // update the context - bool ret = false; - if( strat==strat_ITE ){ - std::map< Node, EnumInfo >::iterator itnc = d_einfo.find( split_cond_enum ); - Assert( itnc!=d_einfo.end() ); - Assert( split_cond_res_index>=0 ); - Assert( split_cond_res_index<(int)itnc->second.d_enum_vals_res.size() ); - prev = x.d_vals; - ret = x.updateContext( this, itnc->second.d_enum_vals_res[split_cond_res_index], sc==1 ); - }else if( strat==strat_CONCAT ){ - prev_str_pos = x.d_str_pos; - prev_has_str_pos = x.d_has_string_pos; - Assert( incr.find( incr_val )!=incr.end() ); - ret = x.updateStringPosition( this, incr[incr_val] ); - x.d_has_string_pos = incr_type; - }else if( strat==strat_ID ){ - ret = true; } - // must have updated the context - AlwaysAssert( ret ); - // recurse - rec_c = constructSolution( c, ce, x, ind+1 ); - if( !rec_c.isNull() ){ - //revert context - if( strat==strat_ITE ){ - x.d_vals = prev; - }else if( strat==strat_CONCAT ){ - x.d_str_pos = prev_str_pos; - x.d_has_string_pos = prev_has_str_pos; + int n = solve_max; + while (n > 0) + { + if (!solved_cond[n].empty()) + { + rec_c = constructBestSolvedConditional(solved_cond[n], x); + indent("sygus-pbe-dt", ind + 1); + Trace("sygus-pbe-dt") + << "PBE: ITE strategy : choose solved conditional " + << d_tds->sygusToBuiltin(rec_c) << " with " << n + << " solved children..." << std::endl; + std::map >::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()); + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") + << "PBE: ITE strategy : choose random conditional " + << d_tds->sygusToBuiltin(rec_c) << std::endl; + } + } + else + { + // TODO (#1250) : degenerate case where children have different + // types? + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") << "return PBE: failed ITE strategy, " + "cannot find a distinguishable condition" + << std::endl; } if( !rec_c.isNull() ){ - dt_children_cons[sc] = rec_c; - }else{ - success = false; - break; + 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()); } } - if( success ){ - std::vector< Node > dt_children; - Assert( !itts->first.isNull() ); - dt_children.push_back( itts->first ); - for( unsigned sc=0; scsecond.d_cenum.size(); sc++ ){ - std::map< unsigned, Node >::iterator itdc = dt_children_cons.find( sc ); - Assert( itdc!=dt_children_cons.end() ); - dt_children.push_back( itdc->second ); - } - ret_dt = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, dt_children ); - indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") << "PBE: success : constructed for strategy "; - print_strat( "sygus-pbe-dt-debug", strat ); - Trace("sygus-pbe-dt-debug") << std::endl; - break; - }else{ - indent("sygus-pbe-dt-debug", ind); - Trace("sygus-pbe-dt-debug") << "PBE: failed for strategy "; - print_strat( "sygus-pbe-dt-debug", strat ); - Trace("sygus-pbe-dt-debug") << std::endl; + 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( ret_dt.isNull() ){ - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "return PBE: fail : all strategies failed " << std::endl; + if (!rec_c.isNull()) + { + dt_children_cons.push_back(rec_c); + } + else + { + success = false; + break; } + } + if (success) + { + Assert(dt_children_cons.size() == etis->d_sol_templ_args.size()); + // ret_dt = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, + // dt_children ); + ret_dt = etis->d_sol_templ; + ret_dt = ret_dt.substitute(etis->d_sol_templ_args.begin(), + etis->d_sol_templ_args.end(), + dt_children_cons.begin(), + dt_children_cons.end()); + indent("sygus-pbe-dt-debug", ind); + Trace("sygus-pbe-dt-debug") + << "PBE: success : constructed for strategy " << strat << std::endl; }else{ - indent("sygus-pbe-dt", ind); - Trace("sygus-pbe-dt") << "return PBE: fail : non-basic" << std::endl; + 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() ); } @@ -1822,6 +2211,10 @@ bool CegConjecturePbe::UnifContext::updateContext( CegConjecturePbe * pbe, std:: } } } + if (changed) + { + d_visit_role.clear(); + } return changed; } @@ -1834,16 +2227,35 @@ bool CegConjecturePbe::UnifContext::updateStringPosition( CegConjecturePbe * pbe changed = true; } } + if (changed) + { + d_visit_role.clear(); + } return changed; } bool CegConjecturePbe::UnifContext::isReturnValueModified() { - if( d_has_string_pos!=0 ){ + if (d_has_string_pos != role_invalid) + { return true; } return false; } +bool CegConjecturePbe::UnifContext::isValidStrategy(EnumTypeInfoStrat* etis) +{ + StrategyType st = etis->d_this; + if (d_has_string_pos == role_string_prefix && st == strat_CONCAT_SUFFIX) + { + return false; + } + if (d_has_string_pos == role_string_suffix && st == strat_CONCAT_PREFIX) + { + return false; + } + return true; +} + void CegConjecturePbe::UnifContext::initialize( CegConjecturePbe * pbe, Node c ) { Assert( d_vals.empty() ); Assert( d_str_pos.empty() ); @@ -1865,19 +2277,23 @@ void CegConjecturePbe::UnifContext::initialize( CegConjecturePbe * pbe, Node c ) } } } + d_visit_role.clear(); } - -void CegConjecturePbe::UnifContext::getCurrentStrings( CegConjecturePbe * pbe, std::vector< Node >& vals, std::vector< CVC4::String >& ex_vals ) { - bool isPrefix = d_has_string_pos==-1; - CVC4::String dummy; +void CegConjecturePbe::UnifContext::getCurrentStrings( + CegConjecturePbe* pbe, + const std::vector& 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!=0 ); - CVC4::String s = vals[i].getConst(); + 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 ) ); @@ -1891,13 +2307,20 @@ void CegConjecturePbe::UnifContext::getCurrentStrings( CegConjecturePbe * pbe, s } } -bool CegConjecturePbe::UnifContext::getStringIncrement( CegConjecturePbe * pbe, bool isPrefix, std::vector< CVC4::String >& ex_vals, std::vector< Node >& vals, std::vector< unsigned >& inc, unsigned& tot ) { +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() ); - CVC4::String mystr = vals[j].getConst(); + 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) ) ){ @@ -1915,12 +2338,16 @@ bool CegConjecturePbe::UnifContext::getStringIncrement( CegConjecturePbe * pbe, } return true; } -bool CegConjecturePbe::UnifContext::isStringSolved( CegConjecturePbe * pbe, std::vector< CVC4::String >& ex_vals, std::vector< Node >& vals ) { +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() ); - CVC4::String mystr = vals[j].getConst(); + String mystr = vals[j].getConst(); if( ex_vals[j]!=mystr ){ return false; } @@ -1942,4 +2369,14 @@ int CegConjecturePbe::getGuardStatus( Node g ) { } } +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/ce_guided_pbe.h b/src/theory/quantifiers/ce_guided_pbe.h index b357e4d15..1abdda6a6 100644 --- a/src/theory/quantifiers/ce_guided_pbe.h +++ b/src/theory/quantifiers/ce_guided_pbe.h @@ -25,6 +25,70 @@ namespace CVC4 { namespace theory { namespace quantifiers { +/** roles for enumerators + * + * This indicates the role of an enumerator that is allocated by approaches + * for synthesis-by-unification (see details below). + * io : the enumerator should enumerate values that are overall solutions + * for the function-to-synthesize, + * ite_condition : the enumerator should enumerate values that are useful + * in ite conditions in the ITE strategy, + * concat_term : the enumerator should enumerate values that are used as + * components of string concatenation solutions. + */ +enum EnumRole +{ + enum_invalid, + enum_io, + enum_ite_condition, + enum_concat_term, +}; +std::ostream& operator<<(std::ostream& os, EnumRole r); + +/** roles for strategy nodes + * + * This indicates the role of a strategy node, which is a subprocedure of + * CegConjecturePbe::constructSolution (see details below). + * equal : the node constructed must be equal to the overall solution for + * the function-to-synthesize, + * string_prefix/suffix : the node constructed must be a prefix/suffix + * of the function-to-synthesize, + * ite_condition : the node constructed must be a condition that makes some + * active input examples true and some input examples false. + */ +enum NodeRole +{ + role_invalid, + role_equal, + role_string_prefix, + role_string_suffix, + role_ite_condition, +}; +std::ostream& operator<<(std::ostream& os, NodeRole r); + +/** enumerator role for node role */ +EnumRole getEnumeratorRoleForNodeRole(NodeRole r); + +/** strategy types + * + * This indicates a strategy for synthesis-by-unification (see details below). + * ITE : strategy for constructing if-then-else solutions via decision + * tree learning techniques, + * CONCAT_PREFIX/SUFFIX : strategy for constructing string concatenation + * solutions via a divide and conquer approach, + * ID : identity strategy used for calling strategies on child type through + * an identity function. + */ +enum StrategyType +{ + strat_INVALID, + strat_ITE, + strat_CONCAT_PREFIX, + strat_CONCAT_SUFFIX, + strat_ID, +}; +std::ostream& operator<<(std::ostream& os, StrategyType st); + class CegConjecture; /** CegConjecturePbe @@ -316,26 +380,12 @@ class CegConjecturePbe { //------------------------------ representation of a enumeration strategy - /** roles for enumerators */ - enum { - enum_io, - enum_ite_condition, - enum_concat_term, - enum_any, - }; - /** print the role with Trace c. */ - static void print_role(const char* c, unsigned r); - /** strategies for SyGuS datatype types */ - enum - { - strat_ITE, - strat_CONCAT, - strat_ID, - }; - /** print the strategy with Trace c. */ - static void print_strat(const char* c, unsigned s); - - /** information about an enumerator */ + /** information about an 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, + */ class EnumInfo { public: EnumInfo() : d_role( enum_io ){} @@ -344,11 +394,7 @@ class CegConjecturePbe { * role is the "role" the enumerator plays in the high-level strategy, * which is one of enum_* above. */ - void initialize(Node c, unsigned role) - { - d_parent_candidate = c; - d_role = role; - } + void initialize(Node c, EnumRole role); bool isTemplated() { return !d_template.isNull(); } void addEnumValue(CegConjecturePbe* pbe, Node v, @@ -356,7 +402,7 @@ class CegConjecturePbe { void setSolved(Node slv); bool isSolved() { return !d_enum_solved.isNull(); } Node getSolved() { return d_enum_solved; } - unsigned getRole() { return d_role; } + EnumRole getRole() { return d_role; } Node d_parent_candidate; // for template Node d_template; @@ -366,9 +412,10 @@ class CegConjecturePbe { std::vector< Node > d_enum_slave; /** values we have enumerated */ std::vector< Node > d_enum_vals; - /** this either stores the values of f( I ) for inputs - or the value of f( I ) = O if d_role==enum_io - */ + /** + * This either stores the values of f( I ) for inputs + * or the value of f( I ) = O if d_role==enum_io + */ std::vector< std::vector< Node > > d_enum_vals_res; std::vector< Node > d_enum_subsume; std::map< Node, unsigned > d_enum_val_to_index; @@ -379,32 +426,70 @@ class CegConjecturePbe { * conjecture */ Node d_enum_solved; /** the role of this enumerator (one of enum_* above). */ - unsigned d_role; + EnumRole d_role; }; /** maps enumerators to the information above */ std::map< Node, EnumInfo > d_einfo; class CandidateInfo; - /** represents a strategy for a SyGuS datatype type */ + + /** 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 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) } + */ class EnumTypeInfoStrat { - public: - unsigned d_this; - /** conditional solutions */ - std::vector< TypeNode > d_csol_cts; - std::vector< Node > d_cenum; + 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; + }; + + /** 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; - // role -> _ - std::map< unsigned, Node > d_enum; + /** the type that this information is for */ TypeNode d_this_type; - // strategies for enum_io role - std::map< Node, EnumTypeInfoStrat > d_strat; - bool isSolved( CegConjecturePbe * pbe ); + /** 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 @@ -413,17 +498,20 @@ class CegConjecturePbe { public: CandidateInfo() : d_check_sol( false ), d_cond_count( 0 ){} Node d_this_candidate; - /** root SyGuS datatype for the function-to-synthesize, - * which encodes the overall syntactic restrictions on the space - * of solutions. - */ - TypeNode d_root; - /** Information for each SyGuS datatype type occurring in a field of d_root + /** + * 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 enumerator */ + /** + * 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; @@ -442,76 +530,208 @@ class CegConjecturePbe { bool getExplanationForEnumeratorExclude( Node c, Node x, Node v, std::vector< Node >& results, EnumInfo& ei, std::vector< Node >& exp ); //------------------------------ strategy registration - void collectEnumeratorTypes(Node c, TypeNode tn, unsigned enum_role); + /** 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, unsigned enum_role, bool inSearch); - void staticLearnRedundantOps(Node c, std::vector& lemmas); - void staticLearnRedundantOps(Node c, - Node e, - std::map& visited, - std::vector& redundant, - std::vector& lemmas, - int ind); - - /** register candidate conditional */ + 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). + */ + void staticLearnRedundantOps( + Node c, + Node e, + NodeRole nrole, + std::map >& visited, + std::map >& needs_cons, + int ind); //------------------------------ end strategy registration //------------------------------ constructing solutions class UnifContext { public: - UnifContext() : d_has_string_pos(0) {} - //IndexFilter d_filter; - // the value of the context conditional - std::vector< Node > d_vals; - // update the examples - bool updateContext( CegConjecturePbe * pbe, std::vector< Node >& vals, bool pol ); - // the position in the strings - std::vector< unsigned > d_str_pos; - // 0 : pos not modified, 1 : pos indicates suffix incremented, -1 : pos indicates prefix incremented - int d_has_string_pos; - // update the string examples - bool updateStringPosition( CegConjecturePbe * pbe, std::vector< unsigned >& pos ); - // is return value modified - bool isReturnValueModified(); - class UEnumInfo { + UnifContext() : d_has_string_pos(role_invalid) {} + /** 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(); + /** returns true if argument is valid strategy in this context */ + bool isValidStrategy(EnumTypeInfoStrat* etis); + /** 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() : d_status(-1){} - int d_status; - // enum val -> polarity -> solved - std::map< Node, std::map< unsigned, Node > > d_look_ahead_sols; + 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; }; - // enumerator -> info + /** map from enumerators to the above info class */ std::map< Node, UEnumInfo > d_uinfo; - void initialize( CegConjecturePbe * pbe, Node c ); - void getCurrentStrings( CegConjecturePbe * pbe, std::vector< Node >& vals, std::vector< CVC4::String >& ex_vals ); - bool getStringIncrement( CegConjecturePbe * pbe, bool isPrefix, std::vector< CVC4::String >& ex_vals, - std::vector< Node >& vals, std::vector< unsigned >& inc, unsigned& tot ); - bool isStringSolved( CegConjecturePbe * pbe, std::vector< CVC4::String >& ex_vals, std::vector< Node >& vals ); }; - /** construct solution */ + + /** 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, - * in context x, where ind is the term depth of the context. - */ - Node constructSolution( Node c, Node e, UnifContext& x, int ind ); + * + * 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 + /** 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, + /** 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 + /** 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. @@ -524,14 +744,14 @@ class CegConjecturePbe { //------------------------------ end constructing solutions /** get guard status - * Returns 1 if g is asserted true in the SAT solver. - * Returns -1 if g is asserted false in the SAT solver. - * Returns 0 otherwise. - */ + * + * Returns 1 if g is asserted true in the SAT solver. + * Returns -1 if g is asserted false in the SAT solver. + * Returns 0 otherwise. + */ int getGuardStatus(Node g); }; - }/* namespace CVC4::theory::quantifiers */ }/* namespace CVC4::theory */ }/* namespace CVC4 */ diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 82c2c2458..b2cf8a069 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -71,7 +71,12 @@ TESTS = commutative.sy \ process-10-vars-2fun.sy \ inv-unused.sy \ ccp16.lus.sy \ - Base16_1.sy + Base16_1.sy \ + icfp_14.12-flip-args.sy \ + strings-template-infer-unused.sy \ + strings-trivial-two-type.sy \ + strings-double-rec.sy \ + hd-19-d1-prog-dup-op.sy # sygus tests currently taking too long for make regress @@ -79,6 +84,8 @@ EXTRA_DIST = $(TESTS) \ max.smt2 \ sygus-uf.sl \ enum-test.sy + +# strings-concat-3-args.sy #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy b/test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy new file mode 100644 index 000000000..abcfc2217 --- /dev/null +++ b/test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy @@ -0,0 +1,32 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status + +(set-logic BV) + +(define-fun hd19 ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32) + (bvxor x (bvxor (bvshl (bvand (bvxor (bvlshr x k) x) m) k) (bvand (bvxor (bvlshr x k) x) m)))) + +; bvand is a duplicate +(synth-fun f ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32) + ((Start (BitVec 32) ((bvand Start Start) + (bvsub Start Start) + (bvxor Start Start) + (bvor Start Start) + (bvand Start Start) + (bvshl Start Start) + (bvlshr Start Start) + (bvashr Start Start) + (bvnot Start) + (bvneg Start) + x + m + k)))) + + +(declare-var x (BitVec 32)) +(declare-var m (BitVec 32)) +(declare-var k (BitVec 32)) + +(constraint (= (hd19 x m k) (f x m k))) +(check-synth) + diff --git a/test/regress/regress0/sygus/icfp_14.12-flip-args.sy b/test/regress/regress0/sygus/icfp_14.12-flip-args.sy new file mode 100644 index 000000000..a1e93cc44 --- /dev/null +++ b/test/regress/regress0/sygus/icfp_14.12-flip-args.sy @@ -0,0 +1,55 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic BV) + +(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001)) +(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004)) +(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010)) +(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001)) +(define-fun if0 ((y (BitVec 64)) (x (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z)) + +(synth-fun f ( (x (BitVec 64))) (BitVec 64) +( + +(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) + (shl1 Start) + (shr1 Start) + (shr4 Start) + (shr16 Start) + (bvand Start Start) + (bvor Start Start) + (bvxor Start Start) + (bvadd Start Start) + (if0 Start Start Start) + )) +) +) +(constraint (= (f #x6E393354DFFAAB51) #xC8E366559002AA57)) +(constraint (= (f #xFDA75AD598A27135) #x812C529533AEC765)) +(constraint (= (f #x58682C0FA4F8DB6D) #xD3CBE9F82D839249)) +(constraint (= (f #x58FDC0941A7E079F) #xD3811FB5F2C0FC30)) +(constraint (= (f #xBDC9B88103ECB0C9) #xA11B23BF7E09A79B)) +(constraint (= (f #x000000000001502F) #xFFFFFFFFFFFF57E8)) +(constraint (= (f #x0000000000010999) #xFFFFFFFFFFFF7B33)) +(constraint (= (f #x0000000000013169) #xFFFFFFFFFFFF674B)) +(constraint (= (f #x000000000001B1A9) #xFFFFFFFFFFFF272B)) +(constraint (= (f #x0000000000016D77) #xFFFFFFFFFFFF4944)) +(constraint (= (f #x0000000000000001) #xFFFFFFFFFFFFFFFF)) +(constraint (= (f #x1ED2E25068744C80) #x0000000000000000)) +(constraint (= (f #x2D2144F9D8CDCBD6) #x0000000000000000)) +(constraint (= (f #xF0F0F0F0F0F0F0F2) #x0000000000000000)) +(constraint (= (f #x83163CFD5DDCCCFB) #xBE74E18151119982)) +(constraint (= (f #xEA31B6A50EF4E399) #x8AE724AD78858E33)) +(constraint (= (f #xE0B1EF549BB6D4B9) #x8FA70855B22495A3)) +(constraint (= (f #x086F9E13A16C363D) #xFBC830F62F49E4E1)) +(constraint (= (f #x2426824D3E67E342) #x0000000000000000)) +(constraint (= (f #xDD518DEFFF18308A) #x0000000000000000)) +(constraint (= (f #x21ECDADB06B3CB03) #xEF0992927CA61A7E)) +(constraint (= (f #x72B1976FBB63A82B) #xC6A73448224E2BEA)) +(constraint (= (f #x16CB47AE0281B27F) #xF49A5C28FEBF26C0)) +(constraint (= (f #x82DE7A1FCA0C0B8F) #xBE90C2F01AF9FA38)) +(constraint (= (f #x0000000000000001) #xFFFFFFFFFFFFFFFF)) +(constraint (= (f #xF0F0F0F0F0F0F0F2) #x0000000000000000)) +(constraint (= (f #x000000000001F0D4) #x0000000000000000)) +(constraint (= (f #x0000000000010067) #xFFFFFFFFFFFF7FCC)) +(check-synth) diff --git a/test/regress/regress0/sygus/strings-double-rec.sy b/test/regress/regress0/sygus/strings-double-rec.sy new file mode 100644 index 000000000..ea9caadea --- /dev/null +++ b/test/regress/regress0/sygus/strings-double-rec.sy @@ -0,0 +1,16 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) + +(synth-fun f ((name String)) String + ((Start String (name "A" "B" "" (str.++ Start1 Start2))) + (Start1 String (name "A" "B" "")) + (Start2 String (name "B" "A" (str.++ Start2 Start))) +)) + + +(declare-var name String) + +(constraint (= (f "BB") "AAAAAAAAAAAA")) + +(check-synth) diff --git a/test/regress/regress0/sygus/strings-template-infer-unused.sy b/test/regress/regress0/sygus/strings-template-infer-unused.sy new file mode 100644 index 000000000..d0bee5564 --- /dev/null +++ b/test/regress/regress0/sygus/strings-template-infer-unused.sy @@ -0,0 +1,16 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) + +(define-fun cA ((x String) (w String) (y String) (z String)) String (str.++ (str.++ x "A") y)) + +(synth-fun f ((name String)) String + ((Start String (name "A" "B" "" + (cA Start Start Start Start))))) + + +(declare-var name String) + +(constraint (= (f "BB") "AAAAAAAAAAAA")) + +(check-synth) diff --git a/test/regress/regress0/sygus/strings-trivial-two-type.sy b/test/regress/regress0/sygus/strings-trivial-two-type.sy new file mode 100644 index 000000000..86c71aa3a --- /dev/null +++ b/test/regress/regress0/sygus/strings-trivial-two-type.sy @@ -0,0 +1,18 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic SLIA) + +(synth-fun f ((name String)) String + ((Start String (ntString)) + (ntString String (name "B" "" + (str.++ ntStringC ntString))) + (ntStringC String (name "A" "")) + + )) + + +(declare-var name String) + +(constraint (= (f "B") "AAAAAAAAAAAAAAAAAAAAAAAAA")) + +(check-synth)