summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ce_guided_pbe.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/ce_guided_pbe.cpp')
-rw-r--r--src/theory/quantifiers/ce_guided_pbe.cpp104
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 ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback