diff options
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/trigger.cpp | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 39063942d..b13e76afb 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -342,7 +342,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 ){ if( patMap.find( n )==patMap.end() ){ patMap[ n ] = false; - bool newHasPol = (n.getKind()==IFF || n.getKind()==XOR) ? false : hasPol; + bool newHasPol = n.getKind()==IFF ? false : hasPol; bool newPol = n.getKind()==NOT ? !pol : pol; if( tstrt==TS_MIN_TRIGGER ){ if( n.getKind()==FORALL ){ @@ -350,9 +350,8 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< }else{ bool retVal = false; for( int i=0; i<(int)n.getNumChildren(); i++ ){ - bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol; bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; - if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){ + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol, newHasPol2 ) ){ retVal = true; } } @@ -381,9 +380,8 @@ 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 newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol; bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; - if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){ + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol, newHasPol2 ) ){ retVal = true; } } |