diff options
Diffstat (limited to 'src/theory/quantifiers/ce_guided_pbe.cpp')
-rw-r--r-- | src/theory/quantifiers/ce_guided_pbe.cpp | 104 |
1 files changed, 55 insertions, 49 deletions
diff --git a/src/theory/quantifiers/ce_guided_pbe.cpp b/src/theory/quantifiers/ce_guided_pbe.cpp index ac09a31d0..e4bf43963 100644 --- a/src/theory/quantifiers/ce_guided_pbe.cpp +++ b/src/theory/quantifiers/ce_guided_pbe.cpp @@ -35,6 +35,7 @@ void indent( const char * c, int ind ) { } } } + void print_val( const char * c, std::vector< Node >& vals, bool pol = true ){ if( Trace.isOn(c) ){ for( unsigned i=0; i<vals.size(); i++ ){ @@ -43,15 +44,8 @@ void print_val( const char * c, std::vector< Node >& vals, bool pol = true ){ } } } -void print_strat( const char * c, unsigned s ){ - switch(s){ - 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; - } -} -void print_role( const char * c, unsigned r ){ + +void CegConjecturePbe::print_role( const char * c, unsigned r ){ switch(r){ case CegConjecturePbe::enum_io:Trace(c) << "IO";break; case CegConjecturePbe::enum_ite_condition:Trace(c) << "CONDITION";break; @@ -61,6 +55,15 @@ void print_role( const char * c, unsigned r ){ } } +void CegConjecturePbe::print_strat( const char * c, unsigned s ){ + switch(s){ + 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; + } +} + CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p) : d_qe(qe), d_parent(p){ @@ -250,7 +253,7 @@ Node CegConjecturePbe::PbeTrie::addPbeExampleEval(TypeNode etn, Node e, Node b, bool CegConjecturePbe::hasExamples(Node e) { if (isPbe()) { - e = getCandidateForEnumerator(e); + e = getSynthFunctionForEnumerator(e); std::map<Node, bool>::iterator itx = d_examples_invalid.find(e); if (itx == d_examples_invalid.end()) { return d_examples.find(e) != d_examples.end(); @@ -260,7 +263,7 @@ bool CegConjecturePbe::hasExamples(Node e) { } unsigned CegConjecturePbe::getNumExamples(Node e) { - e = getCandidateForEnumerator(e); + e = getSynthFunctionForEnumerator(e); std::map<Node, std::vector<std::vector<Node> > >::iterator it = d_examples.find(e); if (it != d_examples.end()) { @@ -271,7 +274,7 @@ unsigned CegConjecturePbe::getNumExamples(Node e) { } void CegConjecturePbe::getExample(Node e, unsigned i, std::vector<Node>& ex) { - e = getCandidateForEnumerator(e); + e = getSynthFunctionForEnumerator(e); std::map<Node, std::vector<std::vector<Node> > >::iterator it = d_examples.find(e); if (it != d_examples.end()) { @@ -283,7 +286,7 @@ void CegConjecturePbe::getExample(Node e, unsigned i, std::vector<Node>& ex) { } Node CegConjecturePbe::getExampleOut(Node e, unsigned i) { - e = getCandidateForEnumerator(e); + e = getSynthFunctionForEnumerator(e); std::map<Node, std::vector<Node> >::iterator it = d_examples_out.find(e); if (it != d_examples_out.end()) { Assert(i < it->second.size()); @@ -297,7 +300,7 @@ Node CegConjecturePbe::getExampleOut(Node e, unsigned i) { Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) { Assert(isPbe()); Assert(!e.isNull()); - e = getCandidateForEnumerator(e); + e = getSynthFunctionForEnumerator(e); std::map<Node, bool>::iterator itx = d_examples_invalid.find(e); if (itx == d_examples_invalid.end()) { unsigned nex = d_examples[e].size(); @@ -310,7 +313,7 @@ Node CegConjecturePbe::addSearchVal(TypeNode tn, Node e, Node bvr) { Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, unsigned i) { - e = getCandidateForEnumerator(e); + e = getSynthFunctionForEnumerator(e); std::map<Node, bool>::iterator itx = d_examples_invalid.find(e); if (itx == d_examples_invalid.end()) { std::map<Node, std::vector<std::vector<Node> > >::iterator it = @@ -323,7 +326,7 @@ Node CegConjecturePbe::evaluateBuiltin(TypeNode tn, Node bn, Node e, return Rewriter::rewrite(bn); } -Node CegConjecturePbe::getCandidateForEnumerator(Node e) { +Node CegConjecturePbe::getSynthFunctionForEnumerator(Node e) { std::map<Node, Node>::const_iterator it = d_enum_to_candidate.find(e); if (it != d_enum_to_candidate.end()) { return it->second; @@ -340,8 +343,7 @@ void CegConjecturePbe::registerEnumerator( Node et, Node c, TypeNode tn, unsigne Trace("sygus-unif-debug") << ", role = "; print_role( "sygus-unif-debug", enum_role ); Trace("sygus-unif-debug") << ", in search = " << inSearch << std::endl; - d_einfo[et].d_parent_candidate = c; - d_einfo[et].d_role = enum_role; + 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 ); @@ -387,9 +389,9 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu 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++ ){ - bool success = false; Node cop = Node::fromExpr( dt[j].getConstructor() ); Node op = Node::fromExpr( dt[j].getSygusOp() ); if( r==0 ){ @@ -397,7 +399,6 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu if( op.getKind() == kind::BUILTIN ){ Kind sk = NodeManager::operatorToKind( op ); if( sk==kind::ITE ){ - Trace("sygus-unif") << "...type " << dt.getName() << " has ITE, enumerate child types..." << std::endl; // we can do unification Assert( dt[j].getNumArgs()==3 ); cop_to_strat[cop] = strat_ITE; @@ -405,9 +406,11 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu if( dt[j].getNumArgs()==2 ) { cop_to_strat[cop] = strat_CONCAT; } - Trace("sygus-unif") << "...type " << dt.getName() << " has CONCAT, child types successful = " << success << std::endl; } 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() ); @@ -417,7 +420,7 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu } } }else if( cop_to_strat.find( cop )==cop_to_strat.end() ){ - // could be a defined function (this is a hack for ICFP benchmarks) + // could be a defined function (this handles the ICFP benchmarks) std::vector< Node > utchildren; utchildren.push_back( cop ); std::vector< Node > sks; @@ -449,7 +452,7 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu cop_to_strat[cop] = strat_ITE; } }else if( eut.getKind()==kind::STRING_CONCAT ){ - if( dt[j].getNumArgs()>=eut.getNumChildren() ){ + if( dt[j].getNumArgs()>=eut.getNumChildren() && eut.getNumChildren()==2 ){ cop_to_strat[cop] = strat_CONCAT; } }else if( eut.getKind()==kind::APPLY_UF ){ @@ -505,7 +508,8 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu } if( cop_to_strat.find( cop )!=cop_to_strat.end() ){ Trace("sygus-unif") << "...type " << dt.getName() << " has defined constructor matching strategy "; - Trace("sygus-unif") << cop_to_strat[cop] << ", enumerate child types..." << std::endl; + 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]; @@ -602,7 +606,7 @@ void CegConjecturePbe::collectEnumeratorTypes( Node e, TypeNode tn, unsigned enu Assert( !et.isNull() ); d_cinfo[e].d_tinfo[tn].d_strat[cop].d_cenum.push_back( et ); // need to make this take into account template - //Assert( et.getType()==e.getType() || d_einfo[et].d_role!=enum_io ); + //Assert( et.getType()==e.getType() || d_einfo[et].getRole()!=enum_io ); } Trace("sygus-unif") << "Initialized strategy "; print_strat( "sygus-unif", strat ); @@ -655,7 +659,7 @@ void CegConjecturePbe::staticLearnRedundantOps( Node c, std::vector< Node >& lem 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.d_role ); + print_role( "sygus-unif", itns->second.getRole() ); Trace("sygus-unif") << std::endl; } } @@ -679,7 +683,7 @@ void CegConjecturePbe::staticLearnRedundantOps( Node c, Node e, std::map< Node, indent("sygus-unif", ind); Trace("sygus-unif") << e << " : role : "; - print_role("sygus-unif", itn->second.d_role); + print_role("sygus-unif", itn->second.getRole()); Trace("sygus-unif") << " : "; if( itn->second.isTemplated() ){ @@ -847,7 +851,7 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& Assert( itv!=d_einfo.end() ); Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl; //bool prevIsCover = false; - if( itv->second.d_role==enum_io ){ + if( itv->second.getRole()==enum_io ){ Trace("sygus-pbe-enum") << " IO-Eval of "; //prevIsCover = itv->second.isFeasible(); }else{ @@ -870,7 +874,7 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& Assert( res.isConst() ); } Node resb; - if( itv->second.d_role==enum_io ){ + if( itv->second.getRole()==enum_io ){ Node out = itxo->second[j]; Assert( out.isConst() ); resb = res==out ? d_true : d_false; @@ -888,7 +892,7 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& } } bool keep = false; - if( itv->second.d_role==enum_io ){ + if( itv->second.getRole()==enum_io ){ if( cond_vals.find( d_true )!=cond_vals.end() || cond_vals.empty() ){ // latter is the degenerate case of no examples //check subsumbed/subsuming std::vector< Node > subsume; @@ -950,7 +954,7 @@ void CegConjecturePbe::addEnumeratedValue( Node x, Node v, std::vector< Node >& itv->second.addEnumValue( this, v, results ); /* if( Trace.isOn("sygus-pbe-enum") ){ - if( itv->second.d_role==enum_io ){ + if( itv->second.getRole()==enum_io ){ if( !prevIsCover && itv->second.isFeasible() ){ Trace("sygus-pbe-enum") << "...PBE : success : Evaluation of " << xs << " now covers all examples." << std::endl; } @@ -1038,7 +1042,7 @@ bool CegConjecturePbe::getExplanationForEnumeratorExclude( Node c, Node x, Node if( ei.d_enum_slave.size()==1 ){ // this check whether the example evaluates to something that is larger than the output // if so, then this term is never useful when using a concatenation strategy - if( ei.d_role==enum_concat_term ){ + if( ei.getRole()==enum_concat_term ){ if( Trace.isOn("sygus-pbe-cterm-debug") ){ Trace("sygus-pbe-enum") << std::endl; } @@ -1091,7 +1095,7 @@ void CegConjecturePbe::EnumInfo::addEnumValue( CegConjecturePbe * pbe, Node v, s d_enum_vals.push_back( v ); d_enum_vals_res.push_back( results ); /* - if( d_role==enum_io ){ + if( getRole()==enum_io ){ // compute if( d_enum_total.empty() ){ d_enum_total = results; @@ -1460,12 +1464,12 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in std::map< Node, EnumInfo >::iterator itn = d_einfo.find( e ); Assert( itn!=d_einfo.end() ); Node ret_dt; - if( itn->second.d_role==enum_any ){ + 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.d_role==enum_io && !x.isReturnValueModified() && itn->second.isSolved() ){ + }else if( itn->second.getRole()==enum_io && !x.isReturnValueModified() && itn->second.isSolved() ){ // this type has a complete solution ret_dt = itn->second.getSolved(); indent("sygus-pbe-dt", ind); @@ -1481,7 +1485,7 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in // get the term enumerator for this type bool success = true; std::map< Node, EnumInfo >::iterator itet; - if( itn->second.d_role==enum_concat_term ){ + if( itn->second.getRole()==enum_concat_term ){ itet = itn; }else{ std::map< unsigned, Node >::iterator itnt = itt->second.d_enum.find( enum_concat_term ); @@ -1518,7 +1522,7 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in Trace("sygus-pbe-dt-debug") << " ...not currently string solved." << std::endl; } } - }else if( itn->second.d_role==enum_io && !x.isReturnValueModified() ){ + }else if( itn->second.getRole()==enum_io && !x.isReturnValueModified() ){ // 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 ); @@ -1552,31 +1556,33 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in int incr_type = 0; std::map< Node, std::vector< unsigned > > incr; - // construct the child order + // 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].d_role==enum_concat_term ); + Assert( d_einfo[ce].getRole()==enum_concat_term ); corder.push_back( sc ); - unsigned inc = r==0 ? 1 : -1; - unsigned scc = sc + inc; - while( scc>=0 && scc<itts->second.d_cenum.size() ){ - corder.push_back( scc ); - scc = scc + inc; - } + cused.insert( sc ); break; } } - }else{ - for( unsigned sc=0; sc<itts->second.d_cenum.size(); sc++ ){ + } + // fill remaining children for which there is no preference + for( unsigned sc=0; sc<itts->second.d_cenum.size(); sc++ ){ + if( cused.find( sc )==cused.end() ){ corder.push_back( sc ); } - } + } Assert( corder.size()==itts->second.d_cenum.size() ); @@ -1703,7 +1709,7 @@ Node CegConjecturePbe::constructSolution( Node c, Node e, UnifContext& x, int in 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.d_role==enum_concat_term ); + 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 ){ |