diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-30 09:11:52 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-30 09:11:52 -0500 |
commit | 100037d531ff1fd30ed3dd5bed91076c383ad55c (patch) | |
tree | f31d60fd4a902efa45e2db109632c607aee5c575 /src/theory/quantifiers/trigger.cpp | |
parent | fa5df1aad69f8ad62686b9418070a1baf74b4a77 (diff) |
Minor fixes for trigger selection max.
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 85 |
1 files changed, 43 insertions, 42 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 1bfc53b41..7072d0499 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -398,16 +398,14 @@ bool Trigger::isSimpleTrigger( Node n ){ } //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula -bool Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, +void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added, bool pol, bool hasPol, bool epol, bool hasEPol ){ std::map< Node, Node >::iterator itv = visited.find( n ); if( itv==visited.end() ){ visited[ n ] = Node::null(); Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl; - bool retVal = false; if( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){ - bool rec = true; Node nu; bool nu_single = false; if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){ @@ -426,11 +424,11 @@ bool Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, } Assert( reqEq.isNull() || !quantifiers::TermDb::hasInstConstAttr( reqEq ) ); Assert( isUsableTrigger( nu, q ) ); - //do not add if already excluded + //do not add if already visited bool add = true; if( n!=nu ){ std::map< Node, Node >::iterator itvu = visited.find( nu ); - if( itvu!=visited.end() && itvu->second.isNull() ){ + if( itvu!=visited.end() ){ add = false; } } @@ -439,55 +437,58 @@ bool Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, visited[ nu ] = nu; tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq ); nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren(); - retVal = true; - if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){ - rec = false; - } + }else{ + nu = Node::null(); } } } - if( rec ){ - Node nrec = nu.isNull() ? n : nu; - std::vector< Node > added2; - for( unsigned i=0; i<nrec.getNumChildren(); i++ ){ - bool newHasPol, newPol; - bool newHasEPol, newEPol; - QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol ); - QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol ); - if( collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol ) ){ - retVal = true; - } - } - if( !nu.isNull() ){ - bool rm_nu = false; - //discard if we added a subterm as a trigger with all variables that nu has - for( unsigned i=0; i<added2.size(); i++ ){ - Assert( tinfo.find( added2[i] )!=tinfo.end() ); - if( added2[i]!=nu ){ + Node nrec = nu.isNull() ? n : nu; + std::vector< Node > added2; + for( unsigned i=0; i<nrec.getNumChildren(); i++ ){ + bool newHasPol, newPol; + bool newHasEPol, newEPol; + QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol ); + QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol ); + collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol ); + } + if( !nu.isNull() ){ + bool rm_nu = false; + for( unsigned i=0; i<added2.size(); i++ ){ + Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i << " : " << added2[i] << std::endl; + Assert( added2[i]!=nu ); + // if child was not already removed + if( tinfo.find( added2[i] )!=tinfo.end() ){ + if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){ + //discard all subterms + Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl; + visited[added2[i]] = Node::null(); + tinfo.erase( added2[i] ); + }else{ if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){ + //discard if we added a subterm as a trigger with all variables that nu has + Trace("auto-gen-trigger-debug2") << "......subsumes parent." << std::endl; rm_nu = true; } - added.push_back( added2[i] ); - }else{ - Assert( false ); + if( std::find( added.begin(), added.end(), added2[i] )==added.end() ){ + added.push_back( added2[i] ); + } } } - if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){ - visited[nu] = Node::null(); - tinfo.erase( nu ); - }else{ - added.push_back( nu ); - } + } + if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){ + visited[nu] = Node::null(); + tinfo.erase( nu ); + }else{ + Assert( std::find( added.begin(), added.end(), nu )==added.end() ); + added.push_back( nu ); } } } - return retVal; }else{ - if( itv->second.isNull() ){ - return false; - }else{ - added.push_back( itv->second ); - return true; + if( !itv->second.isNull() ){ + if( std::find( added.begin(), added.end(), itv->second )==added.end() ){ + added.push_back( itv->second ); + } } } } |