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) ){
}
}
-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<unsigned>(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<unsigned>(r); break;
}
+ return os;
+}
+
+EnumRole getEnumeratorRoleForNodeRole(NodeRole r)
+{
+ switch (r)
+ {
+ case role_equal: return enum_io; break;
+ case role_string_prefix: return enum_concat_term; break;
+ case role_string_suffix: return enum_concat_term; break;
+ case role_ite_condition: return enum_ite_condition; break;
+ default: break;
+ }
+ return enum_invalid;
+}
+
+std::ostream& operator<<(std::ostream& os, StrategyType st)
+{
+ switch (st)
+ {
+ case strat_ITE: os << "ITE"; break;
+ case strat_CONCAT_PREFIX: os << "CONCAT_PREFIX"; break;
+ case strat_CONCAT_SUFFIX: os << "CONCAT_SUFFIX"; break;
+ case strat_ID: os << "ID"; break;
+ default: os << "strat_" << static_cast<unsigned>(st); break;
+ }
+ return os;
}
CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p)
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
// ----------------------------- 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<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::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<dt.getNumConstructors(); j++ ){
- Node cop = Node::fromExpr( dt[j].getConstructor() );
- Node op = Node::fromExpr( dt[j].getSygusOp() );
- if( r==0 ){
- cop_to_cindex[cop] = j;
- if( op.getKind() == kind::BUILTIN ){
- Kind sk = NodeManager::operatorToKind( op );
- if( sk==kind::ITE ){
- // we can do unification
- Assert( dt[j].getNumArgs()==3 );
- cop_to_strat[cop] = strat_ITE;
- }else if( sk==kind::STRING_CONCAT ){
- if( dt[j].getNumArgs()==2 ) {
- cop_to_strat[cop] = strat_CONCAT;
- }
- }
- if( cop_to_strat.find( cop )!=cop_to_strat.end() ){
- Trace("sygus-unif") << "...type " << dt.getName()
- << " has strategy ";
- print_strat("sygus-unif", cop_to_strat[cop]);
- Trace("sygus-unif") << "..." << std::endl;
- // add child types
- for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
- TypeNode ct = TypeNode::fromType( dt[j][k].getRangeType() );
- Trace("sygus-unif") << " Child type " << k << " : " << ((DatatypeType)ct.toType()).getDatatype().getName() << std::endl;
- cop_to_child_types[cop].push_back( ct );
- }
- }
+ EnumTypeInfo& eti = d_cinfo[e].d_tinfo[tn];
+ std::map<NodeRole, StrategyNode>::iterator itsn = eti.d_snodes.find(nrole);
+ if (itsn != eti.d_snodes.end())
+ {
+ // already initialized
+ return;
+ }
+ StrategyNode& snode = eti.d_snodes[nrole];
+
+ // get the enumerator for this
+ EnumRole erole = getEnumeratorRoleForNodeRole(nrole);
+
+ Node ee;
+ std::map<EnumRole, Node>::iterator iten = eti.d_enum.find(erole);
+ if (iten == eti.d_enum.end())
+ {
+ ee = nm->mkSkolem("ee", tn);
+ eti.d_enum[erole] = ee;
+ Trace("sygus-unif-debug")
+ << "...enumerator " << ee << " for "
+ << ((DatatypeType)tn.toType()).getDatatype().getName()
+ << ", role = " << erole << std::endl;
+ }
+ else
+ {
+ ee = iten->second;
+ }
+
+ // roles that we do not recurse on
+ if (nrole == role_ite_condition)
+ {
+ Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl;
+ registerEnumerator(ee, e, tn, erole, true);
+ return;
+ }
+
+ // look at information on how we will construct solutions for this type
+ Assert(tn.isDatatype());
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ Assert(dt.isSygus());
+
+ std::map<Node, std::vector<StrategyType> > cop_to_strat;
+ std::map<Node, unsigned> cop_to_cindex;
+ std::map<Node, std::map<unsigned, Node> > cop_to_child_templ;
+ std::map<Node, std::map<unsigned, Node> > cop_to_child_templ_arg;
+ std::map<Node, std::vector<unsigned> > cop_to_carg_list;
+ std::map<Node, std::vector<TypeNode> > cop_to_child_types;
+ std::map<Node, std::vector<Node> > cop_to_sks;
+
+ // whether we will enumerate the current type
+ bool search_this = false;
+ for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
+ {
+ Node cop = Node::fromExpr(dt[j].getConstructor());
+ Node op = Node::fromExpr(dt[j].getSygusOp());
+ Trace("sygus-unif-debug") << "--- Infer strategy from " << cop
+ << " with sygus op " << op << "..." << std::endl;
+
+ // expand the evaluation to see if this constuctor induces a strategy
+ std::vector<Node> utchildren;
+ utchildren.push_back(cop);
+ std::vector<Node> sks;
+ std::vector<TypeNode> sktns;
+ for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
+ {
+ Type t = dt[j][k].getRangeType();
+ TypeNode ttn = TypeNode::fromType(t);
+ Node kv = nm->mkSkolem("ut", ttn);
+ sks.push_back(kv);
+ cop_to_sks[cop].push_back(kv);
+ sktns.push_back(ttn);
+ utchildren.push_back(kv);
+ }
+ Node ut = nm->mkNode(APPLY_CONSTRUCTOR, utchildren);
+ std::vector<Node> echildren;
+ echildren.push_back(Node::fromExpr(dt.getSygusEvaluationFunc()));
+ echildren.push_back(ut);
+ Node sbvl = Node::fromExpr(dt.getSygusVarList());
+ for (const Node& sbv : sbvl)
+ {
+ echildren.push_back(sbv);
+ }
+ Node eut = nm->mkNode(APPLY_UF, echildren);
+ Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..."
+ << std::endl;
+ eut = d_qe->getTermDatabaseSygus()->unfold(eut);
+ Trace("sygus-unif-debug2") << " ...got " << eut;
+ Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl;
+
+ // candidate strategy
+ if (eut.getKind() == ITE)
+ {
+ cop_to_strat[cop].push_back(strat_ITE);
+ }
+ else if (eut.getKind() == STRING_CONCAT)
+ {
+ if (nrole != role_string_suffix)
+ {
+ cop_to_strat[cop].push_back(strat_CONCAT_PREFIX);
+ }
+ if (nrole != role_string_prefix)
+ {
+ cop_to_strat[cop].push_back(strat_CONCAT_SUFFIX);
+ }
+ }
+ else if (dt[j].isSygusIdFunc())
+ {
+ cop_to_strat[cop].push_back(strat_ID);
+ }
+
+ // the kinds for which there is a strategy
+ if (cop_to_strat.find(cop) != cop_to_strat.end())
+ {
+ // infer an injection from the arguments of the datatype
+ std::map<unsigned, unsigned> templ_injection;
+ std::vector<Node> vs;
+ std::vector<Node> ss;
+ std::map<Node, unsigned> templ_var_index;
+ for (unsigned k = 0, sksize = sks.size(); k < sksize; k++)
+ {
+ Assert(sks[k].getType().isDatatype());
+ const Datatype& cdt =
+ static_cast<DatatypeType>(sks[k].getType().toType()).getDatatype();
+ echildren[0] = Node::fromExpr(cdt.getSygusEvaluationFunc());
+ echildren[1] = sks[k];
+ Trace("sygus-unif-debug2") << "...set eval dt to " << sks[k]
+ << std::endl;
+ Node esk = nm->mkNode(APPLY_UF, echildren);
+ vs.push_back(esk);
+ Node tvar = nm->mkSkolem("templ", esk.getType());
+ templ_var_index[tvar] = k;
+ Trace("sygus-unif-debug2") << "* template inference : looking for "
+ << tvar << " for arg " << k << std::endl;
+ ss.push_back(tvar);
+ Trace("sygus-unif-debug2") << "* substitute : " << esk << " -> " << tvar
+ << std::endl;
+ }
+ eut = eut.substitute(vs.begin(), vs.end(), ss.begin(), ss.end());
+ Trace("sygus-unif-debug2") << "Constructor " << j << ", base term is "
+ << eut << std::endl;
+ std::map<unsigned, Node> test_args;
+ if (dt[j].isSygusIdFunc())
+ {
+ test_args[0] = eut;
+ }
+ else
+ {
+ for (unsigned k = 0, size = eut.getNumChildren(); k < size; k++)
+ {
+ test_args[k] = eut[k];
+ }
+ }
+
+ // TODO : prefix grouping prefix/suffix
+ bool isAssoc = TermUtil::isAssoc(eut.getKind());
+ Trace("sygus-unif-debug2") << eut.getKind() << " isAssoc = " << isAssoc
+ << std::endl;
+ std::map<unsigned, std::vector<unsigned> > assoc_combine;
+ std::vector<unsigned> assoc_waiting;
+ int assoc_last_valid_index = -1;
+ for (std::pair<const unsigned, Node>& ta : test_args)
+ {
+ unsigned k = ta.first;
+ Node eut_c = ta.second;
+ // success if we can find a injection from args to sygus args
+ if (!inferTemplate(k, eut_c, templ_var_index, templ_injection))
+ {
+ Trace("sygus-unif-debug")
+ << "...fail: could not find injection (range)." << std::endl;
+ cop_to_strat.erase(cop);
+ break;
+ }
+ std::map<unsigned, unsigned>::iterator itti = templ_injection.find(k);
+ if (itti != templ_injection.end())
+ {
+ // if associative, combine arguments if it is the same variable
+ if (isAssoc && assoc_last_valid_index >= 0
+ && itti->second == templ_injection[assoc_last_valid_index])
+ {
+ templ_injection.erase(k);
+ assoc_combine[assoc_last_valid_index].push_back(k);
+ }
+ else
+ {
+ assoc_last_valid_index = (int)k;
+ if (!assoc_waiting.empty())
+ {
+ assoc_combine[k].insert(assoc_combine[k].end(),
+ assoc_waiting.begin(),
+ assoc_waiting.end());
+ assoc_waiting.clear();
}
- }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; k<dt[j].getNumArgs(); k++ ){
- Type t = dt[j][k].getRangeType();
- TypeNode ttn = TypeNode::fromType( t );
- Node kv = NodeManager::currentNM()->mkSkolem( "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; k<sbvl.getNumChildren(); k++ ){
- echildren.push_back( sbvl[k] );
+ else
+ {
+ assoc_waiting.push_back(k);
}
- Node eut = NodeManager::currentNM()->mkNode( 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<const unsigned, Node>& ta : test_args)
+ {
+ unsigned k = ta.first;
+ Trace("sygus-unif-debug2") << "- processing argument " << k << "..."
+ << std::endl;
+ if (templ_injection.find(k) != templ_injection.end())
+ {
+ unsigned sk_index = templ_injection[k];
+ if (std::find(cop_to_carg_list[cop].begin(),
+ cop_to_carg_list[cop].end(),
+ sk_index)
+ == cop_to_carg_list[cop].end())
{
- cop_to_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; k<sks.size(); k++ ){
- Assert( sks[k].getType().isDatatype() );
- const Datatype& cdt = ((DatatypeType)sks[k].getType().toType()).getDatatype();
- echildren[0] = Node::fromExpr( cdt.getSygusEvaluationFunc() );
- echildren[1] = sks[k];
- Trace("sygus-unif-debug2") << "...set eval dt to " << sks[k] << std::endl;
- Node esk = NodeManager::currentNM()->mkNode( 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<eut.getNumChildren(); k++ ){
- test_args[k] = eut[k];
- }
+ Trace("sygus-unif-debug") << "...fail: duplicate argument used"
+ << std::endl;
+ cop_to_strat.erase(cop);
+ break;
}
- for( std::map< unsigned, Node >::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<unsigned>& ac = assoc_combine[k];
+ Assert(!ac.empty());
+ std::vector<Node> children;
+ for (unsigned ack = 0, size_ac = ac.size(); ack < size_ac;
+ ack++)
+ {
+ children.push_back(eut[ac[ack]]);
}
+ teut = children.size() == 1
+ ? children[0]
+ : nm->mkNode(eut.getKind(), children);
+ teut = Rewriter::rewrite(teut);
}
- 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<eut.getNumChildren(); k++ ){
- Assert( templ_injection.find( k )!=templ_injection.end() );
- unsigned sk_index = templ_injection[k];
- //also store the template information, if necessary
- Node teut = eut[k];
- if( !teut.isVar() ){
- if( cop_to_strat[cop] == strat_ID ){
- Trace("sygus-unif-debug") << "...cannot use template with ID strategy." << std::endl;
- cop_to_strat.erase( cop );
- }else{
- cop_to_child_templ[cop][k] = teut;
- cop_to_child_templ_arg[cop][k] = ss[sk_index];
- Trace("sygus-unif") << " Arg " << k << " : template : " << teut << ", arg " << ss[sk_index] << std::endl;
- }
- }else{
- Assert( teut==ss[sk_index] );
- }
- }
- // collect children types
- for( unsigned k=0; k<dt[j].getNumArgs(); k++ ){
- Trace("sygus-unif") << " Child type " << k << " : " << ((DatatypeType)sktns[k].toType()).getDatatype().getName() << std::endl;
- cop_to_child_types[cop].push_back( sktns[k] );
- }
+ else
+ {
+ teut = ta.second;
+ }
+
+ if (!teut.isVar())
+ {
+ cop_to_child_templ[cop][k] = teut;
+ cop_to_child_templ_arg[cop][k] = ss[sk_index];
+ Trace("sygus-unif-debug")
+ << " Arg " << k << " (template : " << teut << " arg "
+ << ss[sk_index] << "), index " << sk_index << std::endl;
+ }
+ else
+ {
+ Trace("sygus-unif-debug") << " Arg " << k << ", index "
+ << sk_index << std::endl;
+ Assert(teut == ss[sk_index]);
}
}
+ else
+ {
+ Assert(isAssoc);
+ }
}
}
}
- bool search_this = true;
- for( std::map< Node, unsigned >::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<DatatypeType>(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; j<itct->second.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<const Node, std::vector<StrategyType> >& cstr : cop_to_strat)
+ {
+ Node cop = cstr.first;
+ Trace("sygus-unif-debug") << "Constructor " << cop << " has "
+ << cstr.second.size() << " strategies..."
+ << std::endl;
+ for (unsigned s = 0, ssize = cstr.second.size(); s < ssize; s++)
+ {
+ EnumTypeInfoStrat* cons_strat = new EnumTypeInfoStrat;
+ StrategyType strat = cstr.second[s];
+
+ cons_strat->d_this = strat;
+ cons_strat->d_cons = cop;
+ Trace("sygus-unif-debug") << "Process strategy #" << s
+ << " for operator : " << cop << " : " << strat
+ << std::endl;
+ Assert(cop_to_child_types.find(cop) != cop_to_child_types.end());
+ std::vector<TypeNode>& childTypes = cop_to_child_types[cop];
+ Assert(cop_to_carg_list.find(cop) != cop_to_carg_list.end());
+ std::vector<unsigned>& cargList = cop_to_carg_list[cop];
+
+ std::vector<Node> sol_templ_children;
+ sol_templ_children.resize(cop_to_sks[cop].size());
+
+ for (unsigned j = 0, csize = childTypes.size(); j < csize; j++)
+ {
+ // calculate if we should allocate a new enumerator : should be true
+ // if we have a new role
+ NodeRole nrole_c = nrole;
+ if (strat == strat_ITE)
+ {
+ if (j == 0)
+ {
+ nrole_c = role_ite_condition;
}
-
- // 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<Node, NodeRole>(et, nrole_c));
+ }
+ // children that are unused in the strategy can be arbitrary
+ for (unsigned j = 0, stsize = sol_templ_children.size(); j < stsize;
+ j++)
+ {
+ if (sol_templ_children[j].isNull())
+ {
+ sol_templ_children[j] = cop_to_sks[cop][j].getType().mkGroundTerm();
+ }
+ }
+ sol_templ_children.insert(sol_templ_children.begin(), cop);
+ cons_strat->d_sol_templ =
+ nm->mkNode(APPLY_CONSTRUCTOR, sol_templ_children);
+ if (strat == strat_CONCAT_SUFFIX)
+ {
+ std::reverse(cons_strat->d_cenum.begin(), cons_strat->d_cenum.end());
+ std::reverse(cons_strat->d_sol_templ_args.begin(),
+ cons_strat->d_sol_templ_args.end());
+ }
+ if (Trace.isOn("sygus-unif"))
+ {
+ Trace("sygus-unif") << "Initialized strategy " << strat;
Trace("sygus-unif") << " for " << ((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 );
}
}
}
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;
}
}
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<lemmas.size(); i++ ){
- Trace("sygus-unif") << "...can exclude based on : " << lemmas[i] << std::endl;
+ std::map<Node, std::map<NodeRole, bool> > visited;
+ std::map<Node, std::map<unsigned, bool> > needs_cons;
+ staticLearnRedundantOps(
+ c, d_cinfo[c].getRootEnumerator(), role_equal, visited, needs_cons, 0);
+ // now, check the needs_cons map
+ for (std::pair<const Node, std::map<unsigned, bool> >& nce : needs_cons)
+ {
+ Node em = nce.first;
+ const Datatype& dt =
+ static_cast<DatatypeType>(em.getType().toType()).getDatatype();
+ for (std::pair<const unsigned, bool>& nc : nce.second)
+ {
+ Assert(nc.first < dt.getNumConstructors());
+ if (!nc.second)
+ {
+ Node tst =
+ datatypes::DatatypesRewriter::mkTester(em, nc.first, dt).negate();
+ if (std::find(lemmas.begin(), lemmas.end(), tst) == lemmas.end())
+ {
+ Trace("sygus-unif") << "...can exclude based on : " << tst
+ << std::endl;
+ lemmas.push_back(tst);
+ }
+ }
+ }
}
}
-void 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<Node, std::map<NodeRole, bool> >& visited,
+ std::map<Node, std::map<unsigned, bool> >& 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<NodeRole, StrategyNode>::iterator itsn =
+ tinfo.d_snodes.find(nrole);
+ Assert(itsn != tinfo.d_snodes.end());
+ StrategyNode& snode = itsn->second;
+
+ if (!snode.d_strats.empty())
+ {
+ std::map<unsigned, bool> needs_cons_curr;
+ // various strategies
+ for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
+ {
+ EnumTypeInfoStrat* etis = snode.d_strats[j];
+ StrategyType strat = etis->d_this;
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; i<itts->second.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<unsigned>(cindex)] = false;
+ for (std::pair<Node, NodeRole>& 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<TypeNode, Node>::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<DatatypeType>(etn.toType()).getDatatype();
+ // all constructors that are not a part of a strategy are needed
+ for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
+ {
+ if (needs_cons_curr.find(j) == needs_cons_curr.end())
+ {
+ needs_cons_curr[j] = true;
}
- //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; j<cdt.getNumConstructors(); j++ ){
- Kind ck = d_tds->getConsNumKind( ctn, j );
- if( ck!=UNDEFINED_KIND && TermUtil::isBoolConnective( ck ) ){
- bool typeCorrect = true;
- for( unsigned k=0; k<cdt[j].getNumArgs(); k++ ){
- if( d_tds->getArgType( 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<redundant.size(); i++ ){
- int cindex = Datatype::indexOf( redundant[i].toExpr() );
- Assert( cindex!=-1 );
- const Datatype& dt = Datatype::datatypeOf( redundant[i].toExpr() );
- Node tst = datatypes::DatatypesRewriter::mkTester( e, cindex, dt ).negate();
- if( std::find( lemmas.begin(), lemmas.end(), tst )==lemmas.end() ){
- lemmas.push_back( tst );
- }
- }
- }
+ Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl;
}
}
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 ){
// 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{
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 );
*/
}
+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;
}
Node CegConjecturePbe::CandidateInfo::getRootEnumerator() {
- std::map< unsigned, Node >::iterator it = d_tinfo[d_root].d_enum.find( enum_io );
+ std::map<EnumRole, Node>::iterator it = d_tinfo[d_root].d_enum.find(enum_io);
Assert( it!=d_tinfo[d_root].d_enum.end() );
return it->second;
}
Node 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 )<d_tds->getSygusTermSize( vc ) ) ){
Trace("sygus-pbe") << "**** PBE SOLVED : " << c << " = " << vcc << std::endl;
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<TypeNode, EnumTypeInfo>::iterator itt = d_cinfo[c].d_tinfo.find(etn);
+ Assert(itt != d_cinfo[c].d_tinfo.end());
+ EnumTypeInfo& tinfo = itt->second;
+
+ // get the enumerator information
std::map< Node, EnumInfo >::iterator itn = d_einfo.find( e );
Assert( itn!=d_einfo.end() );
+ EnumInfo& einfo = itn->second;
+
Node ret_dt;
- if (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<Node> 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<Node, EnumInfo>::iterator itet;
+ std::map<EnumRole, Node>::iterator itnt =
+ tinfo.d_enum.find(enum_concat_term);
if( itnt != itt->second.d_enum.end() ){
Node et = itnt->second;
itet = d_einfo.find( et );
+ Assert(itet != d_einfo.end());
}else{
success = false;
}
- }
- if( success ){
- 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; i<itet->second.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<Node, std::vector<Node> >::iterator itx =
+ d_examples_out.find(c);
+ Assert(itx != d_examples_out.end());
+ std::vector<String> ex_vals;
+ x.getCurrentStrings(this, itx->second, ex_vals);
+ Assert(itn->second.d_enum_vals.size()
+ == itn->second.d_enum_vals_res.size());
+
+ // test each example in the term enumerator for the type
+ std::vector<Node> str_solved;
+ for (unsigned i = 0, size = itet->second.d_enum_vals.size(); i < size;
+ i++)
+ {
+ if (x.isStringSolved(
+ this, ex_vals, itet->second.d_enum_vals_res[i]))
+ {
+ str_solved.push_back(itet->second.d_enum_vals[i]);
+ }
+ }
+ if (!str_solved.empty())
+ {
+ ret_dt = constructBestStringSolvedTerm(str_solved, x);
+ indent("sygus-pbe-dt", ind);
+ Trace("sygus-pbe-dt") << "return PBE: success : string solved "
+ << d_tds->sygusToBuiltin(ret_dt) << std::endl;
+ }
+ else
+ {
+ indent("sygus-pbe-dt-debug", ind);
+ Trace("sygus-pbe-dt-debug") << " ...not currently string solved."
+ << std::endl;
}
- }
- 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<Node, std::vector<unsigned> > incr;
+ bool isPrefix = nrole == role_string_prefix;
+ std::map<Node, unsigned> total_inc;
+ std::vector<Node> inc_strs;
+ std::map<Node, std::vector<Node> >::iterator itx = d_examples_out.find(c);
+ Assert(itx != d_examples_out.end());
+ // make the value of the examples
+ std::vector<String> ex_vals;
+ x.getCurrentStrings(this, itx->second, ex_vals);
+ if (Trace.isOn("sygus-pbe-dt-debug"))
+ {
+ indent("sygus-pbe-dt-debug", ind);
+ Trace("sygus-pbe-dt-debug") << "current strings : " << std::endl;
+ for (unsigned i = 0, size = ex_vals.size(); i < size; i++)
+ {
+ indent("sygus-pbe-dt-debug", ind + 1);
+ Trace("sygus-pbe-dt-debug") << ex_vals[i] << std::endl;
+ }
+ }
+
+ // check if there is a value for which is a prefix/suffix of all active
+ // examples
+ Assert(einfo.d_enum_vals.size() == einfo.d_enum_vals_res.size());
+
+ for (unsigned i = 0, size = einfo.d_enum_vals.size(); i < size; i++)
+ {
+ Node val_t = einfo.d_enum_vals[i];
+ indent("sygus-pbe-dt-debug", ind);
+ Trace("sygus-pbe-dt-debug") << "increment string values : " << val_t
+ << " : ";
+ Assert(einfo.d_enum_vals_res[i].size() == itx->second.size());
+ unsigned tot = 0;
+ bool exsuccess = x.getStringIncrement(this,
+ isPrefix,
+ ex_vals,
+ einfo.d_enum_vals_res[i],
+ incr[val_t],
+ tot);
+ if (!exsuccess)
+ {
+ incr.erase(val_t);
+ Trace("sygus-pbe-dt-debug") << "...fail" << std::endl;
+ }
+ else
+ {
+ total_inc[val_t] = tot;
+ inc_strs.push_back(val_t);
+ Trace("sygus-pbe-dt-debug") << "...success, total increment = " << tot
+ << std::endl;
+ }
+ }
+
+ if (!incr.empty())
+ {
+ ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr, x);
+ Assert(!ret_dt.isNull());
indent("sygus-pbe-dt", ind);
- Trace("sygus-pbe-dt") << "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<unsigned> 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<NodeRole, StrategyNode>::iterator itsn =
+ tinfo.d_snodes.find(nrole);
+ if (itsn != tinfo.d_snodes.end())
+ {
+ // strategy info
+ StrategyNode& snode = itsn->second;
+ if (x.d_visit_role[e].find(nrole) == x.d_visit_role[e].end())
+ {
+ x.d_visit_role[e][nrole] = true;
+ // try a random strategy
+ if (snode.d_strats.size() > 1)
+ {
+ std::random_shuffle(snode.d_strats.begin(), snode.d_strats.end());
+ }
+ // get an eligible strategy index
+ unsigned sindex = 0;
+ while (sindex < snode.d_strats.size()
+ && !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<unsigned, Node> look_ahead_solved_children;
+ std::vector<Node> dt_children_cons;
+ bool success = true;
+
+ // for ITE
+ Node split_cond_enum;
+ int split_cond_res_index = -1;
+
+ for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++)
+ {
+ indent("sygus-pbe-dt", ind + 1);
+ Trace("sygus-pbe-dt") << "construct PBE child #" << sc << "..."
+ << std::endl;
+ Node rec_c;
+ std::map<unsigned, Node>::iterator itla =
+ look_ahead_solved_children.find(sc);
+ if (itla != look_ahead_solved_children.end())
+ {
+ rec_c = itla->second;
+ indent("sygus-pbe-dt-debug", ind + 1);
+ Trace("sygus-pbe-dt-debug") << "ConstructPBE: look ahead solved : "
+ << d_tds->sygusToBuiltin(rec_c)
+ << std::endl;
+ }
+ else
+ {
+ std::pair<Node, NodeRole>& cenum = etis->d_cenum[sc];
+
+ // update the context
+ std::vector<Node> prev;
+ if (strat == strat_ITE && sc > 0)
+ {
+ std::map<Node, EnumInfo>::iterator itnc =
+ d_einfo.find(split_cond_enum);
+ Assert(itnc != d_einfo.end());
+ Assert(split_cond_res_index >= 0);
+ Assert(split_cond_res_index
+ < (int)itnc->second.d_enum_vals_res.size());
+ prev = x.d_vals;
+ bool ret = x.updateContext(
+ this,
+ itnc->second.d_enum_vals_res[split_cond_res_index],
+ sc == 1);
+ AlwaysAssert(ret);
}
- // 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<Node, EnumInfo>::iterator itnc = d_einfo.find(ce);
+ Assert(itnc != d_einfo.end());
+ EnumInfo& einfo_child = itnc->second;
+
+ // only used if the return value is not modified
+ if (!x.isReturnValueModified())
{
- corder.push_back( sc );
- }
- }
- Assert( corder.size()==itts->second.d_cenum.size() );
-
-
- for( unsigned scc=0; scc<corder.size(); scc++ ){
- unsigned sc = corder[scc];
- Node rec_c;
- indent("sygus-pbe-dt", ind);
- Trace("sygus-pbe-dt") << "construct PBE child #" << sc << "..." << std::endl;
- std::map< unsigned, Node >::iterator itla = look_ahead_solved_children.find( sc );
- if( itla!=look_ahead_solved_children.end() ){
- rec_c = itla->second;
- indent("sygus-pbe-dt-debug", ind+1);
- Trace("sygus-pbe-dt-debug") << "ConstructPBE: look ahead solved : " << d_tds->sygusToBuiltin( rec_c ) << std::endl;
- }else{
- // 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; k<itnc->second.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; k<itpc->second.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; k<itpc->second.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<Node, NodeRole>& te_pair = etis->d_cenum[i];
+ Node te = te_pair.first;
+ std::map<Node, EnumInfo>::iterator itnt = d_einfo.find(te);
+ Assert(itnt != d_einfo.end());
+ bool branch_pol = (i == 1);
+ // for each condition, get terms that satisfy it in this
+ // branch
+ for (unsigned k = 0, size = einfo_child.d_enum_vals.size();
+ k < size;
+ k++)
+ {
+ Node cond = einfo_child.d_enum_vals[k];
+ std::vector<Node> solved;
+ itnt->second.d_term_trie.getSubsumedBy(
+ 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<int, std::vector<Node> > possible_cond;
+ std::map<Node, int> solved_cond; // stores branch
+ einfo_child.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())
+ {
+ 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; i<itsc->second.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<int, std::vector<Node> > solved_cond;
+ if (!x.isReturnValueModified())
+ {
+ Assert(x.d_uinfo.find(ce) != x.d_uinfo.end());
+ int solve_max = 0;
+ for (Node& cond : itpc->second)
+ {
+ std::map<Node, std::map<unsigned, Node> >::iterator itla =
+ x.d_uinfo[ce].d_look_ahead_sols.find(cond);
+ if (itla != x.d_uinfo[ce].d_look_ahead_sols.end())
+ {
+ int nsolved = itla->second.size();
+ solve_max = nsolved > solve_max ? nsolved : solve_max;
+ solved_cond[nsolved].push_back(cond);
}
- }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<Node, std::map<unsigned, Node> >::iterator itla =
+ x.d_uinfo[ce].d_look_ahead_sols.find(rec_c);
+ Assert(itla != x.d_uinfo[ce].d_look_ahead_sols.end());
+ for (std::pair<const unsigned, Node>& las : itla->second)
+ {
+ look_ahead_solved_children[las.first] = las.second;
+ }
+ break;
}
+ n--;
}
}
+
+ // otherwise, guess a conditional
+ if (rec_c.isNull())
+ {
+ rec_c = constructBestConditional(itpc->second, x);
+ Assert(!rec_c.isNull());
+ indent("sygus-pbe-dt", ind);
+ Trace("sygus-pbe-dt")
+ << "PBE: ITE strategy : choose random conditional "
+ << d_tds->sygusToBuiltin(rec_c) << std::endl;
+ }
+ }
+ else
+ {
+ // TODO (#1250) : degenerate case where children have different
+ // types?
+ indent("sygus-pbe-dt", ind);
+ Trace("sygus-pbe-dt") << "return PBE: failed ITE strategy, "
+ "cannot find a distinguishable condition"
+ << std::endl;
}
if( !rec_c.isNull() ){
- 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; sc<itts->second.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() );
}
}
}
}
+ if (changed)
+ {
+ d_visit_role.clear();
+ }
return changed;
}
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() );
}
}
}
+ 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<Node>& vals,
+ std::vector<String>& ex_vals)
+{
+ bool isPrefix = d_has_string_pos == role_string_prefix;
+ String dummy;
for( unsigned i=0; i<vals.size(); i++ ){
if( d_vals[i]==pbe->d_true ){
Assert( vals[i].isConst() );
unsigned pos_value = d_str_pos[i];
if( pos_value>0 ){
- Assert( d_has_string_pos!=0 );
- CVC4::String s = vals[i].getConst<String>();
+ Assert(d_has_string_pos != role_invalid);
+ String s = vals[i].getConst<String>();
Assert( pos_value<=s.size() );
ex_vals.push_back( isPrefix ? s.suffix( s.size()-pos_value ) :
s.prefix( s.size()-pos_value ) );
}
}
-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<String>& ex_vals,
+ const std::vector<Node>& vals,
+ std::vector<unsigned>& inc,
+ unsigned& tot)
+{
for( unsigned j=0; j<vals.size(); j++ ){
unsigned ival = 0;
if( d_vals[j]==pbe->d_true ){
// example is active in this context
Assert( vals[j].isConst() );
- CVC4::String mystr = vals[j].getConst<String>();
+ String mystr = vals[j].getConst<String>();
ival = mystr.size();
if( mystr.size()<=ex_vals[j].size() ){
if( !( isPrefix ? ex_vals[j].strncmp(mystr, ival) : ex_vals[j].rstrncmp(mystr, ival) ) ){
}
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<String>& ex_vals,
+ const std::vector<Node>& vals)
+{
for( unsigned j=0; j<vals.size(); j++ ){
if( d_vals[j]==pbe->d_true ){
// example is active in this context
Assert( vals[j].isConst() );
- CVC4::String mystr = vals[j].getConst<String>();
+ String mystr = vals[j].getConst<String>();
if( ex_vals[j]!=mystr ){
return false;
}
}
}
+CegConjecturePbe::StrategyNode::~StrategyNode()
+{
+ for (unsigned j = 0, size = d_strats.size(); j < size; j++)
+ {
+ delete d_strats[j];
+ }
+ d_strats.clear();
+}
+}
+}
}
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
//------------------------------ 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 ){}
* 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,
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;
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;
* 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<std::pair<Node, NodeRole> > d_cenum;
+ /** the arguments for the (templated) solution */
+ std::vector<Node> d_sol_templ_args;
+ /** the template for the solution */
+ Node d_sol_templ;
+ };
+
+ /** represents a node in the strategy graph
+ *
+ * It contains a list of possible strategies which are tried during calls
+ * to constructSolution.
+ */
+ class StrategyNode
+ {
+ public:
+ StrategyNode() {}
+ ~StrategyNode();
+ /** the set of strategies to try at this node in the strategy graph */
+ std::vector<EnumTypeInfoStrat*> d_strats;
};
/** stores enumerators and strategies for a SyGuS datatype type */
class EnumTypeInfo {
public:
EnumTypeInfo() : d_parent( NULL ){}
+ /** the parent candidate info (see below) */
CandidateInfo * d_parent;
- // 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<EnumRole, Node> d_enum;
+ /** map from node roles to strategy nodes */
+ std::map<NodeRole, StrategyNode> d_snodes;
};
/** stores strategy and enumeration information for a function-to-synthesize
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;
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<Node>& lemmas);
- void staticLearnRedundantOps(Node c,
- Node e,
- std::map<Node, bool>& visited,
- std::vector<Node>& redundant,
- std::vector<Node>& 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<Node, unsigned>& templ_var_index,
std::map<unsigned, unsigned>& templ_injection);
+ /** static learn redundant operators
+ *
+ * This learns static lemmas for pruning enumerative space based on the
+ * strategy for the function-to-synthesize c, and stores these into lemmas.
+ */
+ void staticLearnRedundantOps(Node c, std::vector<Node>& lemmas);
+ /** helper for static learn redundant operators
+ *
+ * (e, nrole) specify the strategy node in the graph we are currently
+ * analyzing, visited stores the nodes we have already visited.
+ *
+ * This method builds the mapping needs_cons, which maps (master) enumerators
+ * to a map from the constructors that it needs.
+ *
+ * ind is the depth in the strategy graph we are at (for debugging).
+ */
+ void staticLearnRedundantOps(
+ Node c,
+ Node e,
+ NodeRole nrole,
+ std::map<Node, std::map<NodeRole, bool> >& visited,
+ std::map<Node, std::map<unsigned, bool> >& needs_cons,
+ int ind);
//------------------------------ 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<Node> d_vals;
+ /** update the examples
+ *
+ * if pol=true, this method updates d_vals to d_vals & vals
+ * if pol=false, this method updates d_vals to d_vals & ( ~vals )
+ */
+ bool updateContext(CegConjecturePbe* pbe, std::vector<Node>& vals, bool pol);
+ //----------end for ITE strategy
+
+ //----------for CONCAT strategies
+ /** the position in the strings
+ *
+ * For each i/o example pair, this stores the length of the current solution
+ * for the input of the pair, where the solution for that input is a prefix
+ * or
+ * suffix of the output of the pair. For example, if our i/o pairs are:
+ * f( "abcd" ) = "abcdcd"
+ * f( "aa" ) = "aacd"
+ * If the solution we have currently constructed is str.++( x1, "c", ... ),
+ * then d_str_pos = ( 5, 3 ), where notice that
+ * str.++( "abc", "c" ) is a prefix of "abcdcd" and
+ * str.++( "aa", "c" ) is a prefix of "aacd".
+ */
+ std::vector<unsigned> d_str_pos;
+ /** has string position
+ *
+ * Whether the solution positions indicate a prefix or suffix of the output
+ * examples. If this is role_invalid, then we have not updated the string
+ * position.
+ */
+ NodeRole d_has_string_pos;
+ /** update the string examples
+ *
+ * This method updates d_str_pos to d_str_pos + pos.
+ */
+ bool updateStringPosition(CegConjecturePbe* pbe, std::vector<unsigned>& pos);
+ /** get current strings
+ *
+ * This returns the prefix/suffix of the string constants stored in vals
+ * of size d_str_pos, and stores the result in ex_vals. For example, if vals
+ * is (abcdcd", "aacde") and d_str_pos = ( 5, 3 ), then we add
+ * "d" and "de" to ex_vals.
+ */
+ void getCurrentStrings(CegConjecturePbe* pbe,
+ const std::vector<Node>& vals,
+ std::vector<String>& ex_vals);
+ /** get string increment
+ *
+ * If this method returns true, then inc and tot are updated such that
+ * for all active indices i,
+ * vals[i] is a prefix (or suffix if isPrefix=false) of ex_vals[i], and
+ * inc[i] = str.len(vals[i])
+ * for all inactive indices i, inc[i] = 0
+ * We set tot to the sum of inc[i] for i=1,...,n. This indicates the total
+ * number of characters incremented across all examples.
+ */
+ bool getStringIncrement(CegConjecturePbe* pbe,
+ bool isPrefix,
+ const std::vector<String>& ex_vals,
+ const std::vector<Node>& vals,
+ std::vector<unsigned>& inc,
+ unsigned& tot);
+ /** returns true if ex_vals[i] = vals[i] for all active indices i. */
+ bool isStringSolved(CegConjecturePbe* pbe,
+ const std::vector<String>& ex_vals,
+ const std::vector<Node>& vals);
+ //----------end for CONCAT strategies
+
+ /** is return value modified?
+ *
+ * This returns true if we are currently in a state where the return value
+ * of the solution has been modified, e.g. by a previous node that solved
+ * for a prefix.
+ */
+ bool isReturnValueModified();
+ /** 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<Node, std::map<NodeRole, bool> > 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<Node, std::map<unsigned, Node> > 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.
//------------------------------ 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 */
projects / cvc5.git / commitdiff