Minor fixes for trigger selection max.

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 );
+      }
     }
   }
 }