diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-23 15:34:03 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-23 15:34:03 +0200 |
commit | ff216dc63edd0e9dc50bc38010ea50fa565e7e97 (patch) | |
tree | 1a61660f8ae118519a40805b98cb945d80e59825 /src/theory/quantifiers/trigger.cpp | |
parent | 2064e455674aab26e3632da31998bda8b3fff5f9 (diff) |
Support :no-pattern.
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 11ec0210d..b2b8e7197 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -325,7 +325,7 @@ bool Trigger::isSimpleTrigger( Node n ){ } -bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ){ +bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){ if( patMap.find( n )==patMap.end() ){ patMap[ n ] = false; bool newHasPol = n.getKind()==IFF ? false : hasPol; @@ -337,14 +337,17 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< bool retVal = false; for( int i=0; i<(int)n.getNumChildren(); i++ ){ bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; - if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol, newHasPol2 ) ){ + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){ retVal = true; } } if( retVal ){ return true; }else{ - Node nu = getIsUsableTrigger( n, f, pol, hasPol ); + Node nu; + if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){ + nu = getIsUsableTrigger( n, f, pol, hasPol ); + } if( !nu.isNull() ){ patMap[ nu ] = true; return true; @@ -355,7 +358,10 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< } }else{ bool retVal = false; - Node nu = getIsUsableTrigger( n, f, pol, hasPol ); + Node nu; + if( std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){ + nu = getIsUsableTrigger( n, f, pol, hasPol ); + } if( !nu.isNull() ){ patMap[ nu ] = true; if( tstrt==TS_MAX_TRIGGER ){ @@ -367,7 +373,7 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< if( n.getKind()!=FORALL ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; - if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol, newHasPol2 ) ){ + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){ retVal = true; } } @@ -408,12 +414,12 @@ bool Trigger::isPureTheoryTrigger( Node n ) { } } -void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, bool filterInst ){ +void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst ){ std::map< Node, bool > patMap; if( filterInst ){ //immediately do not consider any term t for which another term is an instance of t std::vector< Node > patTerms2; - collectPatTerms( qe, f, n, patTerms2, TS_ALL, false ); + collectPatTerms( qe, f, n, patTerms2, TS_ALL, exclude, false ); std::vector< Node > temp; temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); qe->getTermDatabase()->filterInstances( temp ); @@ -441,7 +447,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } } - collectPatTerms2( qe, f, n, patMap, tstrt, true, true ); + collectPatTerms2( qe, f, n, patMap, tstrt, exclude, true, true ); for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){ if( it->second ){ patTerms.push_back( it->first ); |